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