# Theory SubgroupConjugation

```(*  Title:      Subgroup Conjugation
Author:     Jakob von Raumer, Karlsruhe Institute of Technology
Maintainer: Jakob von Raumer <jakob.raumer at student.kit.edu>
*)

theory SubgroupConjugation
imports GroupAction
begin

section ‹Conjugation of Subgroups and Cosets›

text ‹This theory examines properties of the conjugation of subgroups
of a fixed group as a group action›

subsection ‹Definitions and Preliminaries›

text ‹We define the set of all subgroups of @{term G} which have a certain
cardinality. @{term G} will act on those sets. Afterwards some theorems which
left cosets.›

lemma (in subgroup) subgroup_of_subset:
assumes G:"group G"
assumes PH:"H ⊆ K"
assumes KG:"subgroup K G"
shows "subgroup H (G⦇carrier := K⦈)"
using assms subgroup_def group.m_inv_consistent m_inv_closed by fastforce

context group
begin

definition subgroups_of_size ::"nat ⇒ _"
where "subgroups_of_size p = {H. subgroup H G ∧ card H = p}"

lemma lcosI: "[| h ∈ H; H ⊆ carrier G; x ∈ carrier G|] ==> x ⊗ h ∈ x <# H"

lemma lcoset_join2:
assumes H:"subgroup H G"
assumes g:"g ∈ H"
shows "g <# H = H"
proof auto
fix x
assume x:"x ∈ g <# H"
then obtain h where h:"h ∈ H" "x = g ⊗ h" unfolding l_coset_def by auto
with g H show "x ∈ H" by (metis subgroup.m_closed)
next
fix x
assume x:"x ∈ H"
with g H have "inv g ⊗ x ∈ H" by (metis subgroup.m_closed subgroup.m_inv_closed)
with x g H show "x ∈ g <# H" by (metis is_group subgroup.lcos_module_rev subgroup.mem_carrier)
qed

lemma cardeq_rcoset:
assumes "finite (carrier G)"
assumes "M ⊆ carrier G"
assumes "g ∈ carrier G"
shows "card (M #> g) = card  M"
proof -
have "M #> g ∈ rcosets M" by (metis assms(2) assms(3) rcosetsI)
thus "card (M #> g) = card M"
using assms(2) card_rcosets_equal by auto
qed

lemma cardeq_lcoset:
assumes "finite (carrier G)"
assumes M:"M ⊆ carrier G"
assumes g:"g ∈ carrier G"
shows "card (g <# M) = card  M"
proof -
have "bij_betw (λm. g ⊗ m) M (g <# M)"
show "inj_on ((⊗) g) M"
proof(rule inj_onI)
from g have invg:"inv g ∈ carrier G" by (rule inv_closed)
fix x y
assume x:"x ∈ M" and y:"y ∈ M"
with M have xG:"x ∈ carrier G" and yG:"y ∈ carrier G" by auto
assume "g ⊗ x = g ⊗ y"
hence "(inv g) ⊗ (g ⊗ x) = (inv g) ⊗ (g ⊗ y)" by simp
with g invg xG yG have "(inv g ⊗ g) ⊗ x = (inv g ⊗ g) ⊗ y" by (metis m_assoc)
with g invg xG yG show  "x = y" by simp
qed
next
fix x
assume "x ∈ M"
thus "g ⊗ x ∈ g <# M" unfolding l_coset_def by auto
next
fix x
assume x:"x ∈ g <# M"
then obtain m where "x = g ⊗ m" "m ∈ M" unfolding l_coset_def by auto
thus "x ∈ (⊗) g ` M" by simp
qed
thus "card (g <# M) = card M" by (metis bij_betw_same_card)
qed

subsection ‹Conjugation is a group action›

text ‹We will now prove that conjugation acts on the subgroups
of a certain group. A large part of this proof consists of showing that
the conjugation of a subgroup with a group element is, again, a subgroup.›

lemma conjugation_subgroup:
assumes HG:"subgroup H G"
assumes gG:"g ∈ carrier G"
shows "subgroup (g <# (H #> inv g)) G"
proof
from gG have "inv g ∈ carrier G" by (rule inv_closed)
with HG have "(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset)
with gG show "g <# (H #> inv g) ⊆ carrier G" by (metis l_coset_subset_G)
next
from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed)
with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset)
fix x y
assume x:"x ∈ g <# (H #> inv g)" and y:"y ∈ g <# (H #> inv g)"
then obtain x' y' where x':"x' ∈ H #> inv g" "x = g ⊗ x'" and y':"y' ∈ H #> inv g" "y = g ⊗ y'" unfolding l_coset_def by auto
then obtain hx hy where hx:"hx ∈ H" "x' = hx ⊗ inv g" and hy:"hy ∈ H" "y' = hy ⊗ inv g" unfolding r_coset_def by auto
with x' y' have x2:"x = g ⊗ (hx ⊗ inv g)" and y2:"y = g ⊗ (hy ⊗ inv g)" by auto
hence "x ⊗ y = (g ⊗ (hx ⊗ inv g)) ⊗ (g ⊗ (hy ⊗ inv g))" by simp
also from hx hy HG have hxG:"hx ∈ carrier G" and hyG:"hy ∈ carrier G" by (metis subgroup.mem_carrier)+
with gG hy x2 invgG have "(g ⊗ (hx ⊗ inv g)) ⊗ (g ⊗ (hy ⊗ inv g)) = g ⊗ hx ⊗ (inv g ⊗ g) ⊗ hy ⊗ inv g" by (metis m_assoc m_closed)
also from invgG gG have "... = g ⊗ hx ⊗ 𝟭 ⊗ hy ⊗ inv g" by simp
also from gG hxG have "... = g ⊗ hx ⊗ hy ⊗ inv g" by (metis m_closed r_one)
also from gG hxG invgG have "... = g ⊗ ((hx ⊗ hy) ⊗ inv g)" by (metis gG hxG hyG invgG m_assoc m_closed)
finally have xy:"x ⊗ y = g ⊗ (hx ⊗ hy ⊗ inv g)".
from hx hy HG have "hx ⊗ hy ∈ H" by (metis subgroup.m_closed)
with invgG HG have "(hx ⊗ hy) ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset)
with gG lcosSubset have "g ⊗ (hx ⊗ hy ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI)
with xy show "x ⊗ y ∈ g <# (H #> inv g)" by simp
next
from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed)
with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset)
from HG have "𝟭 ∈ H" by (rule subgroup.one_closed)
with invgG HG have  "𝟭 ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset)
with gG lcosSubset have "g ⊗ (𝟭 ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI)
with gG invgG show "𝟭 ∈ g <# (H #> inv g)" by simp
next
from gG have invgG:"inv g ∈ carrier G" by (metis inv_closed)
with HG have lcosSubset:"(H #> inv g) ⊆ carrier G" by (metis r_coset_subset_G subgroup.subset)
fix x
assume "x ∈ g <# (H #> inv g)"
then obtain x' where x':"x' ∈ H #> inv g" "x = g ⊗ x'" unfolding l_coset_def by auto
then obtain hx where hx:"hx ∈ H" "x' = hx ⊗ inv g"  unfolding r_coset_def by auto
with HG have invhx:"inv hx ∈ H" by (metis subgroup.m_inv_closed)
from x' hx have "inv x = inv (g ⊗ (hx ⊗ inv g))" by simp
also from x' hx HG gG invgG have "... = inv (inv g) ⊗ inv hx ⊗ inv g" by (metis calculation in_mono inv_mult_group lcosSubset subgroup.mem_carrier)
also from gG have "... = g ⊗ inv hx ⊗ inv g" by simp
also from gG invgG invhx HG have "... = g ⊗ (inv hx ⊗ inv g)" by (metis m_assoc subgroup.mem_carrier)
finally have invx:"inv x = g ⊗ (inv hx ⊗ inv g)".
with invhx invgG HG have "(inv hx) ⊗ inv g ∈ H #> inv g" by (metis rcosI subgroup.subset)
with gG lcosSubset have "g ⊗ (inv hx ⊗ inv g) ∈ g <# (H #> inv g)" by (metis lcosI)
with invx show "inv x ∈ g <# (H #> inv g)" by simp
qed

definition conjugation_action::"nat ⇒ _"
where "conjugation_action p = (λg∈carrier G. λP∈subgroups_of_size p. g <# (P #> inv g))"

lemma conjugation_is_size_invariant:
assumes fin:"finite (carrier G)"
assumes P:"P ∈ subgroups_of_size p"
assumes g:"g ∈ carrier G"
shows "conjugation_action p g P ∈ subgroups_of_size p"
proof -
from g have invg:"inv g ∈ carrier G" by (metis inv_closed)
from P have PG:"subgroup P G" and card:"card P = p" unfolding subgroups_of_size_def by simp+
hence PsubG:"P ⊆ carrier G" by (metis subgroup.subset)
hence PinvgsubG:"P #> inv g ⊆ carrier G" by (metis invg r_coset_subset_G)
have " g <# (P #> inv g) ∈ subgroups_of_size p"
show "subgroup (g <# (P #> inv g)) G" by (metis g PG conjugation_subgroup)
next
from card PsubG fin invg have "card (P #> inv g) = p" by (metis cardeq_rcoset)
with g PinvgsubG fin show "card (g <# (P #> inv g)) = p" by (metis cardeq_lcoset)
qed
with P g show ?thesis unfolding conjugation_action_def by simp
qed

lemma conjugation_is_Bij:
assumes fin:"finite (carrier G)"
assumes g:"g ∈ carrier G"
shows "conjugation_action p g ∈ Bij (subgroups_of_size p)"
proof -
from g have invg:"inv g ∈ carrier G" by (rule inv_closed)
from g have "conjugation_action p g ∈ extensional (subgroups_of_size p)" unfolding conjugation_action_def by simp
moreover have "bij_betw (conjugation_action p g) (subgroups_of_size p) (subgroups_of_size p)"
show "inj_on (conjugation_action p g) (subgroups_of_size p)"
proof(rule inj_onI)
fix U V
assume U:"U ∈ subgroups_of_size p" and V:"V ∈ subgroups_of_size p"
hence subsetG:"U ⊆ carrier G" "V ⊆ carrier G" unfolding subgroups_of_size_def by (metis (lifting) mem_Collect_eq subgroup.subset)+
hence subsetL:"U #> inv g ⊆ carrier G" "V #> inv g ⊆ carrier G" by (metis invg r_coset_subset_G)+
assume "conjugation_action p g U = conjugation_action p g V"
with g U V have "g <# (U #> inv g) = g <# (V #> inv g)" unfolding conjugation_action_def by simp
hence "(inv g) <# (g <# (U #> inv g)) = (inv g) <# (g <# (V #> inv g))" by simp
hence "(inv g ⊗ g) <# (U #> inv g) = (inv g ⊗ g) <# (V #> inv g)" by (metis g invg lcos_m_assoc r_coset_subset_G subsetG)
hence "𝟭 <# (U #> inv g) = 𝟭 <# (V #> inv g)" by (metis g l_inv)
hence "U #> inv g = V #> inv g" by (metis subsetL lcos_mult_one)
hence "(U #> inv g) #> g = (V #> inv g) #> g" by simp
hence "U #> (inv g ⊗ g) = V #> (inv g ⊗ g)" by (metis coset_mult_assoc g inv_closed subsetG)
hence "U #> 𝟭 = V #> 𝟭" by (metis g l_inv)
thus "U = V" by (metis coset_mult_one subsetG)
qed
next
fix P
assume "P ∈ subgroups_of_size p"
thus "conjugation_action p g P ∈ subgroups_of_size p" by (metis fin g conjugation_is_size_invariant)
next
fix P
assume P:"P ∈ subgroups_of_size p"
with invg have "conjugation_action p (inv g) P ∈ subgroups_of_size p" by (metis fin invg conjugation_is_size_invariant)
with invg P have "(inv g) <# (P #> (inv (inv g))) ∈ subgroups_of_size p" unfolding conjugation_action_def by simp
hence 1:"(inv g) <# (P #> g) ∈ subgroups_of_size p" by (metis g inv_inv)
have "g <# (((inv g) <# (P #> g)) #> inv g) = (⋃p ∈ P. {g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g)})" unfolding r_coset_def l_coset_def by (simp add:m_assoc)
also from P have PG:"P ⊆ carrier G" unfolding subgroups_of_size_def by (auto simp add:subgroup.subset)
have "∀p ∈ P.  g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = p"
proof(auto)
fix p
assume "p ∈ P"
with PG have p:"p ∈ carrier G"..
with g invg have "g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = (g ⊗ inv g) ⊗ p ⊗ (g ⊗ inv g)" by (metis m_assoc m_closed)
also with g invg g p have "... = p" by (metis l_one r_inv r_one)
finally show "g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g) = p".
qed
hence "(⋃p ∈ P. {g ⊗ (inv g ⊗ (p ⊗ g) ⊗ inv g)}) = P" by simp
finally have "g <# (((inv g) <# (P #> g)) #> inv g) = P".
with 1 have "P ∈ (λP. g <# (P #> inv g)) ` subgroups_of_size p" by auto
with P g show "P ∈ conjugation_action p g ` subgroups_of_size p" unfolding conjugation_action_def by simp
qed
ultimately show ?thesis unfolding BijGroup_def Bij_def by simp
qed

lemma lr_coset_assoc:
assumes g:"g ∈ carrier G"
assumes h:"h ∈ carrier G"
assumes P:"P ⊆ carrier G"
shows "g <# (P #> h) = (g <# P) #> h"
proof(auto)
fix x
assume "x ∈ g <# (P #> h)"
then obtain p where "p ∈ P" and p:"x = g ⊗ (p ⊗ h)" unfolding l_coset_def r_coset_def by auto
with P have "p ∈ carrier G" by auto
with g h p have "x = (g ⊗ p) ⊗ h" by (metis m_assoc)
with ‹p ∈ P› show "x ∈ (g <# P) #> h" unfolding l_coset_def r_coset_def by auto
next
fix x
assume "x ∈ (g <# P) #> h"
then obtain p where "p ∈ P" and p:"x = (g ⊗ p) ⊗ h" unfolding l_coset_def r_coset_def by auto
with P have "p ∈ carrier G" by auto
with g h p have "x = g ⊗ (p ⊗ h)" by (metis m_assoc)
with ‹p ∈ P› show "x ∈ g <# (P #> h)" unfolding l_coset_def r_coset_def by auto
qed

theorem acts_on_subsets:
assumes fin:"finite (carrier G)"
shows "group_action G (conjugation_action p) (subgroups_of_size p)"
unfolding group_action_def group_action_axioms_def group_hom_def group_hom_axioms_def hom_def
proof -
fix g
assume g:"g ∈ carrier G"
with fin show "conjugation_action p g ∈ carrier (BijGroup (subgroups_of_size p))"
unfolding BijGroup_def by (metis conjugation_is_Bij partial_object.select_convs(1))
next
fix x y
assume x:"x ∈ carrier G" and y:"y ∈ carrier G"
hence invx:"inv x ∈ carrier G" and invy:"inv y ∈ carrier G" by (metis inv_closed)+
from x y have xyG:"x ⊗ y ∈ carrier G" by (metis m_closed)
define conjx where "conjx = conjugation_action p x"
define conjy where "conjy = conjugation_action p y"
from fin x have xBij:"conjx ∈ Bij (subgroups_of_size p)" unfolding conjx_def by (metis conjugation_is_Bij)
from fin y have yBij:"conjy ∈ Bij (subgroups_of_size p)" unfolding conjy_def by (metis conjugation_is_Bij)
have "conjx ⊗⇘BijGroup (subgroups_of_size p)⇙ conjy
= (λg∈Bij (subgroups_of_size p). restrict (compose (subgroups_of_size p) g) (Bij (subgroups_of_size p))) conjx conjy" unfolding BijGroup_def by simp
also from xBij yBij have "... = compose (subgroups_of_size p) conjx conjy" by simp
also have "... = (λP∈subgroups_of_size p. conjx (conjy P))" by (metis compose_def)
also have "... = (λP∈subgroups_of_size p. x ⊗ y <# (P #> inv (x ⊗ y)))"
proof(rule restrict_ext)
fix P
assume P:"P ∈ subgroups_of_size p"
hence PG:"P ⊆ carrier G" unfolding subgroups_of_size_def by (auto simp:subgroup.subset)
with y have yPG:"y <# P ⊆ carrier G" by (metis l_coset_subset_G)
from x y have invxyG:"inv (x ⊗ y) ∈ carrier G" and xyG:"x ⊗ y ∈ carrier G" using inv_closed m_closed by auto
from yBij have "conjy ` subgroups_of_size p = subgroups_of_size p" unfolding Bij_def bij_betw_def by simp
with P have conjyP:"conjy P ∈ subgroups_of_size p" unfolding Bij_def bij_betw_def by (metis (full_types) imageI)
with x y P have "conjx (conjy P) = x <# ((y <# (P #> inv y)) #> inv x)" unfolding conjy_def conjx_def conjugation_action_def by simp
also from y invy PG have "... = x <# (((y <# P) #> inv y) #> inv x)" by (metis lr_coset_assoc)
also from PG invx invy y have "... = x <# ((y <# P) #> (inv y ⊗ inv x))" by (metis coset_mult_assoc yPG)
also from x y have "... = x <# ((y <# P) #> inv (x ⊗ y))" by (metis inv_mult_group)
also from invxyG x yPG have "... = (x <# (y <# P)) #> inv (x ⊗ y)" by (metis lr_coset_assoc)
also from x y PG have "... = ((x ⊗ y) <# P) #> inv (x ⊗ y)" by (metis lcos_m_assoc)
also from xyG invxyG PG have "... = (x ⊗ y) <# (P #> inv (x ⊗ y))" by (metis lr_coset_assoc)
finally show "conjx (conjy P) = x ⊗ y <# (P #> inv (x ⊗ y))".
qed
finally have "conjx ⊗⇘BijGroup (subgroups_of_size p)⇙ conjy = (λP∈subgroups_of_size p. x ⊗ y <# (P #> inv (x ⊗ y)))".
with xyG show "conjugation_action p (x ⊗ y)
= conjugation_action p x ⊗⇘BijGroup (subgroups_of_size p)⇙ conjugation_action p y"
unfolding conjx_def conjy_def conjugation_action_def by simp
qed

subsection ‹Properties of the Conjugation Action›

lemma stabilizer_contains_P:
assumes fin:"finite (carrier G)"
assumes P:"P ∈ subgroups_of_size p"
shows "P ⊆ group_action.stabilizer G (conjugation_action p) P"
proof
from P have PG:"subgroup P G" unfolding subgroups_of_size_def by simp
from fin interpret conj:group_action G "(conjugation_action p)" "(subgroups_of_size p)" by (rule acts_on_subsets)
fix x
assume x:"x ∈ P"
with PG have "inv x ∈ P" by (metis subgroup.m_inv_closed)
from x P have xG:"x ∈ carrier G" unfolding subgroups_of_size_def subgroup_def by auto
with P have "conjugation_action p x P = x <# (P #> inv x)" unfolding conjugation_action_def by simp
also from ‹inv x ∈ P› PG have "... = x <# P" by (metis coset_join2 subgroup.mem_carrier)
also from PG x have "... = P" by (rule lcoset_join2)
finally have "conjugation_action p x P = P".
with xG show "x ∈ group_action.stabilizer G (conjugation_action p) P" unfolding conj.stabilizer_def by simp
qed

corollary stabilizer_supergrp_P:
assumes fin:"finite (carrier G)"
assumes P:"P ∈ subgroups_of_size p"
shows "subgroup P (G⦇carrier := group_action.stabilizer G (conjugation_action p) P⦈)"
proof -
from assms have "P ⊆ group_action.stabilizer G (conjugation_action p) P" by (rule stabilizer_contains_P)
moreover from P have "subgroup P G" unfolding subgroups_of_size_def by simp
moreover from P fin have "subgroup (group_action.stabilizer G (conjugation_action p) P) G" by (metis acts_on_subsets group_action.stabilizer_is_subgroup)
ultimately show ?thesis by (metis is_group subgroup.subgroup_of_subset)
qed

lemma (in group) P_fixed_point_of_P_conj:
assumes fin:"finite (carrier G)"
assumes P:"P ∈ subgroups_of_size p"
shows "P ∈ group_action.fixed_points (G⦇carrier := P⦈) (conjugation_action p) (subgroups_of_size p)"
proof -
from fin interpret conjG: group_action G "conjugation_action p" "subgroups_of_size p" by (rule acts_on_subsets)
from P have "subgroup P G" unfolding subgroups_of_size_def by simp
with fin interpret conjP: group_action "G⦇carrier := P⦈" "(conjugation_action p)" "(subgroups_of_size p)" by (metis acts_on_subsets group_action.subgroup_action)
from fin P have "P ⊆ conjG.stabilizer P" by (rule stabilizer_contains_P)
hence "P ⊆ conjP.stabilizer P" using conjG.stabilizer_def conjP.stabilizer_def by auto
with P show "P ∈ conjP.fixed_points" unfolding conjP.fixed_points_def by auto
qed

lemma conj_wo_inv:
assumes QG:"subgroup Q G"
assumes PG:"subgroup P G"
assumes g:"g ∈ carrier G"
assumes conj:"inv g <# (Q #> g) = P"
shows "Q #> g = g <# P"
proof -
from g have invg:"inv g ∈ carrier G" by (metis inv_closed)
from conj have "g <# (inv g <# (Q #> g)) = g <# P" by simp
with QG g invg have "(g ⊗ inv g) <# (Q #> g) = g <# P" by (metis lcos_m_assoc r_coset_subset_G subgroup.subset)
with g invg have "𝟭 <# (Q #> g) = g <# P" by (metis r_inv)
with QG g show "Q #> g = g <# P" by (metis lcos_mult_one r_coset_subset_G subgroup.subset)
qed

end

end
```