Theory Orbit_Stabiliser

chapter "Orbit-Stabiliser Theorem"
text ‹
In this Theory we will prove the orbit-stabiliser theorem, a basic result in the algebra of groups.

›

theory Orbit_Stabiliser
  imports
    "HOL-Algebra.Left_Coset"

begin

section "Imports"
text ‹
  /HOL/Algebra/Group.thy is used for the definitions of groups and subgroups
›

text ‹
  Left\_Coset.thy is a copy of /HOL/Algebra/Coset.thy that includes additional theorems about left cosets.

  The version of Coset.thy in the Isabelle library is missing some theorems about left cosets
  that are available for right cosets, so these had to be added by simply replacing the definitions
  of right cosets with those of left cosets.

  Coset.thy is used for definitions of group order, quotient groups (operator LMod), and Lagranges theorem.
›

text ‹
  /HOL/Fun.thy is used for function composition and the identity function.
›


section "Group Actions"

text ‹
  We begin by augmenting the existing definition of a group with a group action.

  The group action was defined according to \<^cite>‹groupaction›.
›

locale orbit_stabiliser = group +
  fixes action :: "'a ⇒ 'b ⇒ 'b" (infixl ‹⊙› 51)
  assumes id_act [simp]: "𝟭 ⊙ x = x"
    and compat_act:
    "g ∈ carrier G ∧ h ∈ carrier G ⟶ g ⊙ (h ⊙ x) = (g ⊗ h) ⊙ x"

section "Orbit and stabiliser"

text ‹
Next, we define orbit and stabiliser, according to the same Wikipedia article.
›

context orbit_stabiliser
begin

definition orbit :: "'b ⇒ 'b set" where
  "orbit x = {y. (∃ g ∈ carrier G. y = g ⊙ x)}"

definition stabiliser :: "'b ⇒ 'a set"
  where "stabiliser x = {g ∈ carrier G. g ⊙ x = x}"


section "Stabiliser Theorems"

text ‹
We begin our proofs by showing that the stabiliser forms a subgroup.

This proof follows the template from  \<^cite>‹stabsub›.
›

theorem stabiliser_subgroup: "subgroup (stabiliser x) G"
proof(rule subgroupI)
  show "stabiliser x ⊆ carrier G" using stabiliser_def by auto
next
  fix x
  from id_act have "𝟭 ⊙ x = x" by simp
  then have "𝟭 ∈ stabiliser x" using stabiliser_def by auto
  then show "stabiliser x ≠ {}" by auto
next
  fix g x
  assume gStab:"g ∈ stabiliser x"
  then have g_car:"g ∈ carrier G" using stabiliser_def by simp
  then have invg_car:"inv g ∈ carrier G" using inv_closed by simp
  have "g ⊙ x = x" using stabiliser_def gStab by simp
  then have "inv g ⊙ (g ⊙ x) = inv g ⊙ x" by simp
  then have "(inv g ⊗ g) ⊙ x = inv g ⊙ x" using compat_act g_car invg_car by simp
  then have "x = (inv g) ⊙ x" using g_car l_inv by simp
  then show "inv g ∈ stabiliser x" using invg_car stabiliser_def by simp
next
  fix g h x
  assume g_stab: "g ∈ stabiliser x" and h_stab: "h ∈ stabiliser x"
  then have g_car: "g ∈ carrier G" and h_car: "h ∈ carrier G" using stabiliser_def by auto
  then have "g ⊙ x = x" "h ⊙ x = x"
    using stabiliser_def g_stab h_stab by auto
  then have "g ⊙ (h ⊙ x) = x" by simp
  then have "(g ⊗ h) ⊙ x = x" using compat_act g_car h_car by simp
  then show "(g ⊗ h) ∈ stabiliser x"
    using g_stab h_stab stabiliser_def by auto
qed

text ‹
As an intermediate step we formulate a lemma about the relationship between the group action
and the stabiliser.

This proof follows the template from \<^cite>‹stabsubcor›.
›

corollary stabiliser_subgroup_corollary:
  assumes g_car: "g ∈ carrier G" and
    h_car: "h ∈ carrier G"
  shows "(g ⊙ x) = (h ⊙ x) ⟷ ((inv g) ⊗ h) ∈ stabiliser x"
proof
  from g_car have invg_car: "(inv g) ∈ carrier G" by auto
  show "(g ⊙ x) = (h ⊙ x) ⟹ inv g ⊗ h ∈ stabiliser x"
  proof -
    assume gh: "(g ⊙ x) = (h ⊙ x)"
    have "((inv g) ⊗ h) ⊙ x = (inv g) ⊙ (h ⊙ x)" using assms compat_act by simp
    moreover have "(inv g) ⊙ (h ⊙ x) = (inv g) ⊙ (g ⊙ x)" using gh by simp
    moreover have "(inv g) ⊙ (g ⊙ x) = ((inv g) ⊗ g) ⊙ x" using invg_car g_car compat_act by simp
    moreover have "((inv g) ⊗ g) ⊙ x = x" using g_car by simp
    ultimately have "((inv g) ⊗ h) ⊙ x = x" by simp
    then show ?thesis using stabiliser_def assms by simp
  qed

  show "inv g ⊗ h ∈ stabiliser x ⟹ g ⊙ x = h ⊙ x"
  proof -
    assume gh_stab: "inv g ⊗ h ∈ stabiliser x"
    with stabiliser_def have "x = ((inv g) ⊗ h) ⊙ x" by simp
    then have "𝟭 ⊙ x = ((inv g) ⊗ h) ⊙ x"  by simp
    then have "((inv g) ⊗ g) ⊙ x = ((inv g) ⊗ h) ⊙ x" using invg_car g_car by simp
    then have "x = (inv g) ⊙ (h ⊙ x)" using compat_act g_car h_car by simp
    then have "g ⊙ x = (g ⊗ (inv g)) ⊙ (h ⊙ x)" using compat_act g_car invg_car by metis
    then have "g ⊙ x = h ⊙ x" using compat_act g_car id_act invg_car r_inv by simp
    then show ?thesis by simp
  qed
qed

text ‹
Using the previous lemma and our proof that the stabiliser forms a subgroup, we can now
show that the elements of the orbit map to left cosets of the stabiliser.

This will later form the basis of showing a bijection between the orbit and those cosets.
›

lemma stabiliser_cosets_equivalent:
  assumes g_car: "g ∈ carrier G" and
    h_car: "h ∈ carrier G"
  shows "(g ⊙ x) = (h ⊙ x) ⟷ (g <# stabiliser x) = (h <# stabiliser x)"
proof
  show "g ⊙ x = h ⊙ x ⟹ g <# stabiliser x = h <# stabiliser x"
  proof -
    assume "g ⊙ x = h ⊙ x"
    then have stab_elem: "((inv g) ⊗ h) ∈ stabiliser x"
      using assms stabiliser_subgroup_corollary by simp
    with subgroup.lcos_module_rev[OF stabiliser_subgroup] have "h ∈ g <# (stabiliser x)"
      using assms is_group by simp
    with l_repr_independence have  "g <# (stabiliser x) = h <# (stabiliser x)"
      using assms  stab_elem stabiliser_subgroup by auto
    then show ?thesis by simp
  qed
  show "g <# stabiliser x = h <# stabiliser x ⟹ g ⊙ x = h ⊙ x"
  proof -
    assume "g <# stabiliser x = h <# stabiliser x"
    with subgroup.lcos_module_rev[OF stabiliser_subgroup] have "h ∈ g <# (stabiliser x)"
      using assms is_group l_inv stabiliser_subgroup subgroup_def by metis
    with subgroup.lcos_module_imp[OF stabiliser_subgroup] have "((inv g) ⊗ h) ∈ stabiliser x"
      using assms is_group by blast
    with stabiliser_subgroup_corollary have "g ⊙ x = h ⊙ x" using assms by simp
    then show ?thesis by simp
  qed
qed

section "Picking representatives from cosets"

text ‹
Before we can prove the bijection, we need a few lemmas about representatives from sets.

First we define rep to be an arbitrary element from a left coset of the stabiliser.
›
definition rep :: "'a set ⇒ 'a" where
  "(H ∈ carrier (G LMod (stabiliser x))) ⟹ rep H = (SOME y. y ∈ H)"

text ‹
  The next lemma shows that the representative is always an element of its coset.
›
lemma quotient_rep_ex  : "H ∈ (carrier (G LMod (stabiliser x))) ⟹ rep H ∈ H"
proof -
  fix H
  assume H:"H ∈ carrier (G LMod stabiliser x)"
  then obtain g where "g ∈ carrier G" "H = g <# (stabiliser x)"
    unfolding LFactGroup_def LCOSETS_def by auto
  then have "(SOME x. x ∈ H) ∈ H" using lcos_self stabiliser_subgroup someI_ex by fast
  then show "rep H ∈ H" using H rep_def by auto
qed

text ‹
The final lemma about representatives shows that it does not matter which element of the coset
is picked, i.e. all representatives are equivalent.
›
lemma rep_equivalent:
  assumes H:"H ∈ carrier (G LMod stabiliser x)" and
    gH:"g ∈ H"
  shows "H = g <# (stabiliser x)"
proof -
  fix h
  from H obtain h where hG:"h ∈ carrier G" and H2:"H = h <# (stabiliser x)"
    unfolding LFactGroup_def LCOSETS_def by auto
  with H gH have gh:"g ∈ h <# (stabiliser x)" by simp
  from l_repr_independence have "h <# stabiliser x = g <# stabiliser x"
    using hG gh stabiliser_subgroup by simp
  with H2 have "H = g <# (stabiliser x)" by simp
  then show ?thesis by simp
qed

section "Orbit-Stabiliser Theorem"

text ‹
  We can now establish the bijection between orbit(x) and the quotient group G/(stabiliser(x))

  The idea for this bijection is from \<^cite>‹orbitstab›
›
theorem orbit_stabiliser_bij:
  "bij_betw (λH. rep H ⊙ x) (carrier (G LMod (stabiliser x))) (orbit x) "
proof (rule bij_betw_imageI)
  (* show the function is injective *)
  show "inj_on (λH. rep H ⊙ x) (carrier (G LMod stabiliser x))"
  proof(rule inj_onI)
    fix H H'
    assume H:"H ∈ carrier (G LMod (stabiliser x))"
    assume H':"H' ∈ carrier (G LMod (stabiliser x))"
    obtain h h' where  h:"h = rep H" and h': "h' = rep H'" by simp
    assume act_equal: "(rep H) ⊙ x = (rep H') ⊙ x"
    from H h quotient_rep_ex have hH: "h ∈ H" by simp
    from H' h' quotient_rep_ex have hH': "h' ∈ H'" by simp
    from subgroup.lcosets_carrier[OF stabiliser_subgroup is_group] H have "H ⊆ carrier G"
      unfolding LFactGroup_def by simp
    then have hG: "h ∈ carrier G" using hH by auto
    from subgroup.lcosets_carrier[OF stabiliser_subgroup is_group] H' have "H' ⊆ carrier G"
      unfolding LFactGroup_def by simp
    then have h'G: "h' ∈ carrier G" using hH' by auto

        (* Apply lemma about equivalent cosets *)
    have hh'_equiv:"h <# (stabiliser x) = h' <# (stabiliser x)"
      using hG h'G h h' act_equal stabiliser_cosets_equivalent by simp

    from hh'_equiv have H2:"H = h <# (stabiliser x)"
      using H hH rep_equivalent by blast
    moreover from hh'_equiv have H3:"H' = h <# (stabiliser x)"
      using H' hH' rep_equivalent by blast
    then show "H = H'" using H2 H3 by simp
  qed
next
  show "(λH. rep H ⊙ x) ` carrier (G LMod stabiliser x) = orbit x"
  proof(auto)
    show "⋀H. H ∈ carrier (G LMod stabiliser x) ⟹ rep H ⊙ x ∈ orbit x"
    proof -
      fix H
      assume H:"H ∈ carrier (G LMod (stabiliser x))"
      obtain h where h:"h = rep H" by simp
      from H h quotient_rep_ex have hH: "h ∈ H" by simp
      have stab_sub: "(stabiliser x) ⊆ carrier G" using stabiliser_def by auto
      from subgroup.lcosets_carrier[OF stabiliser_subgroup is_group] H have "H ⊆ carrier G"
        unfolding LFactGroup_def by simp
      with hH have "h ∈ carrier G" by auto
      then show "(rep H) ⊙ x ∈ orbit x" using h orbit_def mem_Collect_eq by blast
    qed
    show "⋀y. y ∈ orbit x ⟹ y ∈ (λH. rep H ⊙ x) ` carrier (G LMod stabiliser x)"
    proof -
      fix y
      assume y:"y ∈ orbit x"
      obtain g  where gG:"g ∈ carrier G" and "y = g ⊙ x" using y orbit_def by auto
      obtain H where H:"H = g <# (stabiliser x)" by auto
      with gG have H_carr:"H ∈ carrier (G LMod stabiliser x)"
        unfolding LFactGroup_def LCOSETS_def by auto
      then have "rep H ∈ H" using quotient_rep_ex by auto
      then obtain h where h_stab:"h ∈ stabiliser x" and gh:"rep H = g ⊗ h"
        unfolding H l_coset_def by auto
      have hG:"h ∈ carrier G" using h_stab stabiliser_def by auto
      from stabiliser_def h_stab have "h ⊙ x = x" by auto
      with ‹y = g ⊙ x› have "y = g ⊙ (h ⊙ x)" by simp
      then have "y = (g ⊗ h) ⊙ x" using gG hG compat_act by auto
      then have "y = (rep H) ⊙ x" using gh by simp
      then show "y ∈ (λH. rep H ⊙ x) ` carrier (G LMod stabiliser x)"
        using H_carr by simp
    qed
  qed
qed


text‹
  The actual orbit-stabiliser theorem is a consequence of the bijection
   we established in the previous theorem and of Lagrange's theorem
›
theorem orbit_stabiliser:
  assumes finite: "finite (carrier G)"
  shows "order G = card (orbit x) * card (stabiliser x)"
proof -
  have "card (carrier (G LMod (stabiliser x))) = card (orbit x)"
    using bij_betw_same_card orbit_stabiliser_bij by auto
  moreover have "card (carrier (G LMod (stabiliser x))) * card (stabiliser x)  = order G"
    using finite stabiliser_subgroup l_lagrange unfolding LFactGroup_def by simp
  ultimately show ?thesis by simp
qed
end

end