# 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
```