Theory Secondary_Sylow.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 (Gcarrier := 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 = (λgcarrier G. λPsubgroups_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
    = (λgBij (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 "... = (λPsubgroups_of_size p. conjx (conjy P))" by (metis compose_def)
  also have "... = (λPsubgroups_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 = (λPsubgroups_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 (Gcarrier := 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 (Gcarrier := 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 "Gcarrier := 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