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
are already available for right cosets are dualized into statements about
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"
  by (auto simp add: l_coset_def)

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)"
  proof(auto simp add: bij_betw_def)
    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"
  proof(auto simp add:subgroups_of_size_def)
    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)"
  proof(auto simp add:bij_betw_def)
    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
apply(auto simp add:is_group group_BijGroup)
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