Theory Sylow_Theorems
theory Sylow_Theorems
imports Group_Theory Group_Operations "HOL-Computational_Algebra.Primes"
begin
section ‹The First Sylow Theorem›
context Group
begin
interpretation left: left_translations_of_group G "(⋅)" 𝟭 ..
text ‹The set of @{term n}-element subsets of @{term G}.›
definition Ω :: "nat ⇒ 'a set set"
where "Ω n = {B. B ⊆ G ∧ card B = n}"
text ‹The left-translation action on @{term "Ω n"}: each @{term "g ∈ G"} acts by mapping
a subset @{term B} to @{term "(⋅) g ` B = {g ⋅ b | b. b ∈ B}"}. We make the map
extensional on @{term "Ω n"} so it lies in @{term "Ω n →⇩E Ω n"}.›
definition φ_left :: "nat ⇒ 'a ⇒ 'a set ⇒ 'a set"
where "φ_left n g = restrict (λB. (⋅) g ` B) (Ω n)"
text ‹Membership in @{term "Ω n"}.›
lemma Ω_memI [intro]: "⟦B ⊆ G; card B = n⟧ ⟹ B ∈ Ω n"
unfolding Ω_def by simp
lemma Ω_memD [dest]: "B ∈ Ω n ⟹ B ⊆ G ∧ card B = n"
unfolding Ω_def by simp
text ‹The cardinality of @{term "Ω n"} is the binomial coefficient @{term "card G choose n"}.›
lemma card_Ω:
assumes "finite G"
shows "card (Ω n) = card G choose n"
using assms by (simp add: Ω_def n_subsets)
text ‹Left multiplication by @{term "g ∈ G"} is injective on the carrier.›
lemma left_mult_inj_on:
assumes "g ∈ G"
shows "inj_on ((⋅) g) G"
by (simp add: assms inj_on_def)
text ‹Left multiplication maps subsets of @{term G} to subsets of @{term G}.›
lemma left_mult_image_subset:
assumes "g ∈ G" "B ⊆ G"
shows "(⋅) g ` B ⊆ G"
using assms by auto
text ‹Left multiplication preserves cardinality of subsets of @{term G}.›
lemma left_mult_image_card:
assumes "g ∈ G" "B ⊆ G"
shows "card ((⋅) g ` B) = card B"
by (meson assms left_mult_inj_on card_image inj_on_subset)
text ‹The action @{term "φ_left n g"} maps @{term "Ω n"} to itself.›
lemma φ_left_closed:
assumes "g ∈ G" "B ∈ Ω n"
shows "(⋅) g ` B ∈ Ω n"
using assms left_mult_image_subset left_mult_image_card by (fastforce simp: Ω_def)
text ‹The action applied to an element of @{term "Ω n"}.›
lemma φ_left_apply [simp]:
assumes "B ∈ Ω n"
shows "φ_left n g B = (⋅) g ` B"
using assms unfolding φ_left_def by simp
text ‹Outside @{term "Ω n"}, the action is undefined.›
lemma φ_left_undefined:
assumes "B ∉ Ω n"
shows "φ_left n g B = undefined"
using assms unfolding φ_left_def by simp
text ‹The action is extensional on @{term "Ω n"}.›
lemma φ_left_extensional: "φ_left n g ∈ extensional (Ω n)"
unfolding φ_left_def by (rule restrict_extensional)
text ‹The action maps @{term "Ω n"} into itself.›
lemma φ_left_mapsto:
assumes "g ∈ G"
shows "φ_left n g ∈ Ω n →⇩E Ω n"
using assms φ_left_closed φ_left_extensional
by (auto simp: PiE_def Pi_def extensional_def φ_left_def restrict_def Ω_def)
text ‹Left multiplication by @{term "g ∈ G"} followed by @{term "inverse g"} is the identity
on subsets of @{term G}.›
lemma left_mult_image_inverse:
assumes "g ∈ G" "B ⊆ G"
shows "(⋅) (inverse g) ` ((⋅) g ` B) = B"
proof (intro iffI set_eqI)
fix x
assume "x ∈ (⋅) (inverse g) ` ((⋅) g ` B)"
then obtain b where "b ∈ B" "x = inverse g ⋅ (g ⋅ b)" by blast
then show "x ∈ B"
by (metis assms invertible invertible_left_inverse2 subsetD)
next
fix x
assume "x ∈ B" then show "x ∈ (⋅) (inverse g) ` ((⋅) g ` B)"
by (metis assms imageI in_mono invertible invertible_left_inverse2)
qed
text ‹The action @{term "φ_left n g"} is a bijection on @{term "Ω n"}.›
lemma φ_left_bij:
assumes "g ∈ G"
shows "bij_betw (φ_left n g) (Ω n) (Ω n)"
proof (intro bij_betw_byWitness strip)
fix B assume B: "B ∈ Ω n"
then have BG: "B ⊆ G" and gB: "(⋅) g ` B ∈ Ω n"
using assms B φ_left_closed by auto
with B show "φ_left n (inverse g) (φ_left n g B) = B"
using assms BG φ_left_apply left_mult_image_inverse
by presburger
next
fix B assume B: "B ∈ Ω n"
then have BG: "B ⊆ G" by auto
have gB: "(⋅) (inverse g) ` B ∈ Ω n"
using B φ_left_closed assms invertible invertible_inverse_closed by meson
have "φ_left n g (φ_left n (inverse g) B) = (⋅) g ` ((⋅) (inverse g) ` B)"
using B gB φ_left_apply by presburger
also have "… = B"
using BG assms invertible invertible_inverse_closed invertible_inverse_inverse
left_mult_image_inverse by metis
finally show "φ_left n g (φ_left n (inverse g) B) = B" .
next
show "φ_left n g ` Ω n ⊆ Ω n"
using assms φ_left_closed by auto
show "φ_left n (inverse g) ` Ω n ⊆ Ω n"
by (simp add: φ_left_closed assms image_iff image_subset_iff)
qed
text ‹The action satisfies the unit law.›
lemma φ_left_unit: "φ_left n 𝟭 = identity (Ω n)"
by (force simp: image_def left_unit φ_left_def subsetD)
text ‹The action satisfies the composition law.›
lemma φ_left_compose:
assumes "g ∈ G" "h ∈ G"
shows "φ_left n (g ⋅ h) = compose (Ω n) (φ_left n g) (φ_left n h)"
proof (rule ext)
fix B
show "φ_left n (g ⋅ h) B = compose (Ω n) (φ_left n g) (φ_left n h) B"
proof (cases "B ∈ Ω n")
case True
then have "compose (Ω n) (φ_left n g) (φ_left n h) B = φ_left n g ((⋅) h ` B)"
by (simp add: compose_eq)
also have "… = (⋅) g ` ((⋅) h ` B)"
using assms True φ_left_closed by simp
also have "… = (⋅) (g ⋅ h) ` B"
proof -
have "B ⊆ G" using True by auto
then show ?thesis
using associative [OF assms]
by (smt (cvc5, best) compose_eq image_cong in_mono surj_compose)
qed
also have "… = φ_left n (g ⋅ h) B" using True by simp
finally show ?thesis by simp
next
case False
then show ?thesis by (simp add: φ_left_def compose_def)
qed
qed
text ‹The left-translation action on @{term "Ω n"} is a @{locale Group_Action}.›
theorem subset_action:
"Group_Action G (⋅) 𝟭 (φ_left n) (Ω n)"
proof
fix g assume "g ∈ G"
then show "φ_left n g ∈ Monoid.Units (Ω n →⇩E Ω n) (compose (Ω n)) (identity (Ω n))"
by (simp add: φ_left_bij φ_left_mapsto transformations.Units_bij_betwD)
qed (auto simp: φ_left_unit φ_left_compose)
end
lemma (in Group) Sylow_abelian:
assumes grp: "Abelian_Group G (⋅) 𝟭" "finite G"
and prime: "prime p" and dvd: "p dvd card G"
shows "∃g∈G. element_order g = p"
using dvd grp
proof (induction "card G" arbitrary: G "(⋅)" "𝟭" rule: less_induct)
case less
then interpret G: Abelian_Group G composition unit by simp
have "card G ≠ 1"
using less.prems prime by force
with less obtain a where a: "a∈G" "a ≠ unit"
using G.unit_closed by (metis empty_iff is_singletonI' is_singleton_altdef)
let ?r = "G.element_order a"
show ?case
proof (cases "p dvd ?r")
case True
then obtain r' where r': "?r = p * r'" and pow_eq: "G.power (G.power a r') p = unit"
using G.power_element_order G.power_mult ‹a∈G› less.prems(3) by (metis dvdE mult.commute)
have fin: "finite G" using less by simp
have aG: "G.power a r' ∈ G" using a by simp
have dvd_p: "G.element_order (G.power a r') dvd p"
using G.element_order_dvd[OF fin aG] pow_eq by blast
have False if "G.element_order (G.power a r') = 1"
proof -
have "G.element_order a dvd r'"
using G.element_order_dvd G.power_1 G.power_element_order ‹a∈G› aG fin that by metis
then show False
using G.element_order_pos[OF fin ‹a∈G›] r' prime by simp
qed
with dvd_p show ?thesis using aG
using prime prime_nat_iff by blast
next
case not_dvd: False
have fin: "finite G" using less by simp
define C where "C ≡ G.cyclic_subgroup a"
have C_sub: "C ⊆ G" unfolding C_def using G.cyclic_subgroup_subset a by simp
have card_C: "card C = ?r" unfolding C_def using G.card_cyclic_subgroup[OF fin ‹a∈G›] .
interpret sub_C: Subgroup C G composition unit
unfolding C_def using G.cyclic_subgroup_is_subgroup[OF fin ‹a∈G›] .
interpret CG: subgroup_of_abelian_group C G composition unit ..
have card_quotient: "card CG.Factor_Group = CG.index"
using CG.card_Factor_Group less by simp
then have ‹card C < card G›
by (metis C_sub card_C card_mono fin le_neq_implies_less less.prems(1) not_dvd)
define FactG where "FactG ≡ some_elem ` CG.Factor_Group"
define comp where "comp ≡ class_representatives.rep_comp G CG.Factor_Group CG.quotient_composition"
interpret iso: group_isomorphism "restrict some_elem CG.Factor_Group"
CG.Factor_Group CG.quotient_composition "CG.Class unit"
FactG comp "some_elem (CG.Class unit)"
using CG.group_isomorphism_Factor_Group_class_reps
by (force simp: FactG_def local.comp_def)
have *: "card C * card FactG = card G"
using CG.card_class_reps CG.lagrange FactG_def card_quotient fin by presburger
then have "card FactG > 1"
by (metis ‹card C < card G› mult.commute nat_mult_1 nat_mult_less_cancel_disj)
have "finite FactG"
using CG.class_reps_subset FactG_def fin finite_subset by blast
have ‹p dvd card FactG›
by (metis "*" card_C less.prems(1) not_dvd prime prime_dvd_multD)
have abel_FactG: "Abelian_Group FactG comp (some_elem (CG.Class unit))"
using CG.abelian_class_reps[OF CG.quotient_abelian] by (simp add: FactG_def local.comp_def)
have "card C > 1"
using G.element_order_pos G.power_1 G.power_element_order a(1,2) card_C fin
by (metis One_nat_def antisym_conv3 not_less_eq)
then have "card FactG < card G"
using "*" ‹1 < card FactG›
by (metis One_nat_def bot_nat_0.not_eq_extremum n_less_m_mult_n not_less_iff_gr_or_eq)
then obtain g where g: "g ∈ FactG" "Monoid.element_order comp (some_elem (CG.Class unit)) g = p"
using less(1) ‹p dvd card FactG› abel_FactG ‹finite FactG› ‹1 < card FactG› by blast
then obtain X where X: "X ∈ CG.Factor_Group" "some_elem X = g" by (auto simp: FactG_def)
obtain g' where g': "g' ∈ G" "X = CG.Class g'"
using CG.representant_exists[OF X(1)] by auto
have finFG: "finite CG.Factor_Group"
using CG.Partition_def fin finite_imageI by auto
then have nat_dvd: "CG.quotient.element_order (CG.Class g') dvd G.element_order g'"
by (metis CG.natural.commutes_with_power CG.quotient.element_order_dvd G.power_element_order
X(1) fin g')
have "iso.image.sub.element_order (restrict some_elem CG.Factor_Group X)
dvd CG.quotient.element_order X"
using iso.element_order_image_dvd[OF finFG ‹finite FactG› X(1)] by simp
then have "p dvd CG.quotient.element_order (CG.Class g')"
using X g g' by auto
then show ?thesis
using G.element_order_power_prime fin g'(1) gcd_nat.trans nat_dvd prime by blast
qed
qed
subsection ‹Conjugation, Center, and Centralizer›
context Group begin
text ‹The conjugation action: @{term g} acts on @{term x} by @{text "g x g⇧-⇧1"}.
We use @{text "g x g⇧-⇧1"} rather than @{text "g⇧-⇧1 x g"} so that the map
@{text "g ↦ (x ↦ g x g⇧-⇧1)"} is a group homomorphism (not anti-homomorphism).›
definition conjugation :: "'a ⇒ 'a ⇒ 'a"
where "conjugation g x ≡ (if g ∈ G ∧ x ∈ G then g ⋅ x ⋅ inverse g else x)"
lemma conjugation_closed:
assumes "g ∈ G" "x ∈ G"
shows "conjugation g x ∈ G"
using assms by (simp add: conjugation_def)
lemma conjugation_unit:
assumes "x ∈ G"
shows "conjugation 𝟭 x = x"
using assms by (simp add: conjugation_def)
lemma conjugation_compose:
assumes "g ∈ G" "h ∈ G"
shows "conjugation (g ⋅ h) x = conjugation g (conjugation h x)"
by (simp add: assms associative conjugation_def inverse_composition_commute)
lemma conjugation_outside [simp]:
"x ∉ G ⟹ conjugation g x = x"
by (simp add: conjugation_def)
lemma conjugation_bij:
assumes "g ∈ G"
shows "bij_betw (conjugation g) G G"
proof (rule bij_betwI)
show "⋀x. x ∈ G ⟹ conjugation (inverse g) (conjugation g x) = x"
using assms by (simp add: conjugation_def associative invertible_left_inverse2)
show "⋀y. y ∈ G ⟹ conjugation g (conjugation (inverse g) y) = y"
using assms by (simp add: conjugation_def associative invertible_right_inverse2)
qed (auto simp: conjugation_closed assms)
text ‹The restricted conjugation map, suitable for the @{locale Group_Action} locale.›
definition φ_conj :: "'a ⇒ 'a ⇒ 'a"
where "φ_conj g = restrict (conjugation g) G"
lemma φ_conj_apply [simp]:
assumes "g ∈ G" "x ∈ G"
shows "φ_conj g x = g ⋅ x ⋅ inverse g"
using assms by (simp add: φ_conj_def conjugation_def)
lemma φ_conj_outside [simp]:
"x ∉ G ⟹ φ_conj g x = undefined"
by (simp add: φ_conj_def)
lemma φ_conj_extensional: "φ_conj g ∈ extensional G"
unfolding φ_conj_def by (rule restrict_extensional)
lemma φ_conj_mapsto:
assumes "g ∈ G"
shows "φ_conj g ∈ G →⇩E G"
using assms by (auto simp: PiE_def Pi_def φ_conj_def conjugation_closed)
lemma φ_conj_bij:
assumes "g ∈ G"
shows "bij_betw (φ_conj g) G G"
by (simp add: φ_conj_def assms conjugation_bij)
lemma φ_conj_unit: "φ_conj 𝟭 = identity G"
by auto
lemma φ_conj_compose:
assumes "g ∈ G" "h ∈ G"
shows "φ_conj (g ⋅ h) = compose G (φ_conj g) (φ_conj h)"
by (force simp: conjugation_closed φ_conj_def assms compose_def conjugation_compose)
theorem conjugation_action: "Group_Action G (⋅) 𝟭 φ_conj G"
proof
fix g assume "g ∈ G"
then show "φ_conj g ∈ Monoid.Units (G →⇩E G) (compose G) (identity G)"
by (simp add: φ_conj_bij φ_conj_mapsto transformations.Units_bijective)
qed (auto simp: φ_conj_unit φ_conj_compose)
text ‹The center of @{term G}: elements that commute with everything.›
definition center :: "'a set"
where "center = {z ∈ G. ∀g ∈ G. z ⋅ g = g ⋅ z}"
text ‹The centralizer of an element @{term y}: elements that commute with @{term y}.›
definition centralizer :: "'a ⇒ 'a set"
where "centralizer y = {g ∈ G. g ⋅ y = y ⋅ g}"
lemma center_subset: "center ⊆ G"
by (auto simp: center_def)
lemma center_mem_iff:
assumes "z ∈ G"
shows "z ∈ center ⟷ (∀g ∈ G. z ⋅ g = g ⋅ z)"
using assms by (simp add: center_def)
lemma centralizer_subset: "centralizer y ⊆ G"
by (auto simp: centralizer_def)
lemma centralizer_mem_iff:
assumes "g ∈ G" "y ∈ G"
shows "g ∈ centralizer y ⟷ g ⋅ y = y ⋅ g"
using assms by (simp add: centralizer_def)
text ‹Interpret the conjugation action to access orbits, stabilizers, and fixed points.›
interpretation conj: Group_Action G "(⋅)" 𝟭 φ_conj G
by (rule conjugation_action)
lemma center_eq_fixed_points: "center = conj.fixed_points"
unfolding center_def conj.fixed_points_def conj.stabilizer_def
by (force simp: subset_iff simp flip: commute_iff_inverse)
text ‹The class equation separates the singleton conjugacy classes, which are exactly the
center, from the nontrivial conjugacy classes.›
theorem class_equation:
assumes "finite G"
shows "card G = card center + (∑X ∈ conj.nontrivial_orbits. card X)"
using conj.fixed_point_class_equation[OF assms]
by (simp add: center_eq_fixed_points)
lemma centralizer_eq_stabilizer:
assumes "y ∈ G"
shows "centralizer y = conj.stabilizer y"
using assms
by (auto simp: centralizer_def commute_iff_inverse conj.stabilizer_def)
text ‹The center is a subgroup of @{term G}.›
lemma inverse_commutes:
assumes "x ∈ G" "∀g ∈ G. x ⋅ g = g ⋅ x"
shows "∀g ∈ G. inverse x ⋅ g = g ⋅ inverse x"
proof
fix g assume gG: "g ∈ G"
have "x ⋅ (inverse x ⋅ g) = g"
using assms(1) gG by (simp add: associative [symmetric])
moreover have "x ⋅ (g ⋅ inverse x) = g"
by (simp add: assms associative gG)
ultimately show "inverse x ⋅ g = g ⋅ inverse x"
using assms(1) gG
by (metis composition_closed invertible invertible_inverse_closed
invertible_left_inverse2)
qed
lemma center_subgroup: "Subgroup center G (⋅) 𝟭"
proof (rule subgroupI)
fix x y assume "x ∈ center" "y ∈ center"
then show "x ⋅ y ∈ center"
unfolding center_def mem_Collect_eq
by (metis associative composition_closed)
next
fix x assume x: "x ∈ center"
then show "invertible x" using center_subset by auto
show "inverse x ∈ center"
using x center_subset inverse_commutes by (auto simp: center_def)
qed (auto simp add: center_def)
text ‹The center is an abelian group.›
lemma center_abelian: "Abelian_Group center (⋅) 𝟭"
proof -
interpret CG: subgroup_of_group center G "(⋅)" 𝟭
by (simp add: Group_axioms center_subgroup subgroup_of_group_def)
show ?thesis
proof qed (use center_subset center_def in blast)
qed
text ‹The centralizer of @{term "y ∈ G"} is a subgroup of @{term G}.›
lemma centralizer_subgroup:
assumes "y ∈ G"
shows "Subgroup (centralizer y) G (⋅) 𝟭"
using conj.stabilizer_subgroup[OF assms] centralizer_eq_stabilizer[OF assms] by simp
text ‹If @{term y} is not in the center, then its centralizer is a proper subgroup.›
lemma centralizer_proper:
assumes "y ∈ G" "y ∉ center" "finite G"
shows "card (centralizer y) < card G"
proof -
have "centralizer y ⊆ G" by (rule centralizer_subset)
moreover have "centralizer y ≠ G"
by (metis assms center_mem_iff centralizer_mem_iff)
ultimately show ?thesis using assms(3) by (simp add: psubsetI psubset_card_mono)
qed
end
text ‹Preimage of a subgroup under a group homomorphism is a subgroup.›
lemma (in group_homomorphism) preimage_subgroup:
assumes sub: "Subgroup S G' (⋅') 𝟭'"
defines "H ≡ {g ∈ G. η g ∈ S}"
shows "Subgroup H G (⋅) 𝟭"
proof (rule source.subgroupI)
show "H ⊆ G" "𝟭 ∈ H"
using commutes_with_unit sub Submonoid.sub_unit_closed by (fastforce simp: H_def Subgroup_def)+
next
fix x y assume "x ∈ H" "y ∈ H"
then have xG: "x ∈ G" and yG: "y ∈ G" and xS: "η x ∈ S" and yS: "η y ∈ S"
unfolding H_def by auto
have "η (x ⋅ y) = η x ⋅' η y" using commutes_with_composition xG yG by auto
also have "… ∈ S" using sub xS yS
by (meson Group_def Monoid.composition_closed Subgroup_def)
finally show "x ⋅ y ∈ H" unfolding H_def using xG yG by auto
next
fix x assume "x ∈ H"
then have xG: "x ∈ G" and xS: "η x ∈ S" unfolding H_def by auto
show "source.invertible x" using xG by auto
have "η (source.inverse x) = target.inverse (η x)"
using invertible_commutes_with_inverse xG by blast
also have "… ∈ S"
using sub target.Gen_def target.Gen_subgroup_eq target.generate.inv xS by blast
finally show "source.inverse x ∈ H"
by (auto simp: H_def xG)
qed
text ‹Cardinality of the preimage: each coset in the subgroup contributes @{term "card (Ker)"} elements.›
lemma (in group_homomorphism) preimage_card:
assumes sub: "Subgroup S G' (⋅') 𝟭'" and fin: "finite G" and fin': "finite G'"
and img: "S ⊆ η ` G"
defines "H ≡ {g ∈ G. η g ∈ S}"
shows "card H = card S * card Ker"
proof -
define fiber where "fiber s ≡ {g ∈ G. η g = s}" for s
have H_eq: "H = (⋃s ∈ S. fiber s)"
unfolding H_def fiber_def by auto
have fib_class: "∃g ∈ G. fiber s = kernel.Class g" if "s ∈ S" for s
proof -
obtain g where gG: "g ∈ G" and sg: "η g = s"
using ‹s ∈ S› img by auto
have "fiber s = kernel.Class g"
proof (intro set_eqI iffI)
fix x assume "x ∈ fiber s"
then have xG: "x ∈ G" and "η x = s" "η x = η g"
unfolding fiber_def using sg by auto
then have "η (inverse x ⋅ g) = 𝟭'"
using invertible_image_lemma sg xG ‹g ∈ G› by (auto simp add: commutes_with_composition)
then have "inverse x ⋅ g ∈ Ker"
using Ker_memI gG xG by blast
then have "(x, g) ∈ kernel.Congruence"
by (metis gG kernel.CongruenceI kernel.symmetric source.invertible
source.invertible_right_inverse2 xG)
then show "x ∈ kernel.Class g"
by (rule kernel.ClassI)
next
fix x assume "x ∈ kernel.Class g"
then have "(x, g) ∈ kernel.Congruence"
using kernel.ClassD gG by blast
then have xG: "x ∈ G" using kernel.left_closed by auto
from ‹(x, g) ∈ kernel.Congruence› obtain k where kK: "k ∈ Ker" and xgk: "x = g ⋅ k"
using kernel.CongruenceD by auto
then have "η x = η g ⋅' η k"
using commutes_with_composition gG Ker_closed[OF kK] by auto
then show "x ∈ fiber s" unfolding fiber_def using xG
using Ker_image gG kK sg by force
qed
then show "∃g ∈ G. fiber s = kernel.Class g" using gG by auto
qed
have fib_card: "⋀s. s ∈ S ⟹ card (fiber s) = card Ker"
by (metis fib_class kernel.Class_cardinality)
have fib_disj: "disjoint_family_on fiber S"
unfolding disjoint_family_on_def fiber_def by auto
have fib_fin: "⋀s. s ∈ S ⟹ finite (fiber s)"
unfolding fiber_def using fin by auto
have "finite S"
using fin' sub by (meson finite_subset Subgroup_def Submonoid.subset)
then show ?thesis
using card_UN_disjoint'[OF fib_disj fib_fin] by (simp add: H_eq fib_card)
qed
subsection ‹First Sylow Theorem›
theorem (in Group) Sylow_I:
fixes p :: nat and m :: nat
assumes "prime p"
and "finite G"
and "p ^ m dvd card G"
shows "∃H. Subgroup H G (⋅) 𝟭 ∧ card H = p ^ m"
using assms(3,2) Group_axioms
proof (induction "card G" arbitrary: G "(⋅)" "𝟭" m rule: less_induct)
case less
then interpret G: Group G composition unit
by meson
show ?case
proof (cases "m = 0")
case True
then have "Subgroup {unit} G composition unit ∧ card {unit} = p ^ m"
by (auto intro: G.subgroupI)
then show ?thesis by blast
next
case False
have fin: "finite G" using less.prems by simp
have pa_dvd: "p ^ m dvd card G" using less.prems by simp
have p_dvd_G: "p dvd card G"
using False pa_dvd by auto
show ?thesis
proof (cases "p dvd card G.center")
case True
have center_fin: "finite G.center"
using fin G.center_subset finite_subset by blast
interpret Z: Group G.center composition unit
using G.center_subgroup Subgroup.axioms(2) by force
obtain z where zZ: "z ∈ G.center" and z_ord: "Z.element_order z = p"
using Z.Sylow_abelian[OF G.center_abelian center_fin ‹prime p› True]
by auto
have zG: "z ∈ G" using zZ G.center_subset by auto
have z_comm: "⋀g. g ∈ G ⟹ composition z g = composition g z"
using zZ G.center_def by auto
have "Z.power z n = G.power z n" for n
by (induction n) auto
then have z_ord_G: "G.element_order z = p" using z_ord
unfolding Z.element_order_def G.element_order_def by simp
have p_pos: "p > 0" using ‹prime p› prime_gt_0_nat by blast
define N where "N = G.power z ` {..<p}"
have N_alt: "N = range (G.power z)"
using G.power_mod_order[OF fin zG] p_pos z_ord_G
by (fastforce simp: N_def)
have N_sub: "N ⊆ G" unfolding N_def using zG by auto
have card_N: "card N = p"
using G.power_inj_on_order[OF fin zG] z_ord_G
by (simp add: N_def card_image)
have unit_N: "unit ∈ N" unfolding N_alt
by (metis G.power_0 rangeI)
have comp_N: "composition x y ∈ N" if "x ∈ N" "y ∈ N" for x y
using that zG by (force simp: N_alt simp flip: G.power_add)
have inv_N: "G.inverse x ∈ N" if "x ∈ N" for x
proof -
obtain i where xi: "x = G.power z i"
using that N_alt ‹x ∈ N› by blast
have xG: "x ∈ G" using that N_sub by auto
define y where "y ≡ G.power z ((p - 1) * i)"
have yN: "y ∈ N" unfolding y_def N_alt by auto
have yG: "y ∈ G" using yN N_sub by auto
have "composition x y = G.power z (i + (p - 1) * i)"
unfolding xi y_def using zG G.power_add by auto
also have "i + (p - 1) * i = p * i" using p_pos by (simp add: algebra_simps)
also have "G.power z (p * i) = G.power (G.power z p) i"
using zG G.power_mult by simp
also have "G.power (G.power z p) i = unit"
using G.power_element_order[OF fin zG] z_ord_G by simp
finally have xy: "composition x y = unit" .
then show ?thesis
by (metis G.center_mem_iff G.inverse_equality Z.power_closed xG xi yG yN zZ)
qed
have sub_N: "Subgroup N G composition unit"
using G.subgroupI N_sub comp_N inv_N unit_N by blast
interpret NG: subgroup_of_group N G composition unit
by (simp add: G.Group_axioms sub_N subgroup_of_group_def)
have N_normal: "normal_subgroup N G composition unit"
proof (rule NG.Left_equals_Right_coset_implies_normality)
fix g assume gG: "g ∈ G"
show "NG.Left_Coset g N = NG.Right_Coset N g"
proof -
have power_comm: "composition g (G.power z i) = composition (G.power z i) g" for i
proof (induction i)
case 0
then show ?case by (simp add: gG)
next
case (Suc i) then show ?case
by (metis G.center_mem_iff G.power_closed Z.power_closed gG zG zZ)
qed
show ?thesis
proof (intro set_eqI iffI)
fix x
assume "x ∈ NG.Left_Coset g N"
then obtain n where nN: "n ∈ N" and xeq: "x = composition g n"
by (auto simp: NG.Left_Coset_def)
from nN obtain i where ni: "n = G.power z i"
using N_alt by blast
then show "x ∈ NG.Right_Coset N g"
using nN power_comm xeq by auto
next
fix x
assume "x ∈ NG.Right_Coset N g"
then obtain n i where "n ∈ N" "x = composition n g" "n = G.power z i"
using N_alt by blast
then show "x ∈ NG.Left_Coset g N"
using NG.Left_Coset_memI power_comm by metis
qed
qed
qed
interpret NG: normal_subgroup N G composition unit
using N_normal .
have card_FG: "card NG.Factor_Group = NG.index"
using NG.card_Factor_Group fin by simp
have card_G_eq: "card G = card N * NG.index"
using NG.lagrange fin by simp
then have card_G_eq': "card G = p * card NG.Factor_Group"
using card_N card_FG by simp
have FG_lt: "card NG.Factor_Group < card G"
using assms(1) card_G_eq' fin prime_nat_iff zG by fastforce
show ?thesis
proof -
have fin_FG: "finite NG.Factor_Group"
using fin NG.partition partition_on_def by (metis finite_UnionD)
have "p ^ m dvd p * card NG.Factor_Group"
using pa_dvd card_G_eq' by simp
then have pa1_dvd: "p ^ (m - 1) dvd card NG.Factor_Group"
by (metis False dvd_mult_cancel p_pos power_eq_if)
define FactG where "FactG ≡ some_elem ` NG.Factor_Group"
define fcomp where "fcomp ≡ class_representatives.rep_comp G NG.Factor_Group NG.quotient_composition"
interpret iso: group_isomorphism "restrict some_elem NG.Factor_Group"
NG.Factor_Group NG.quotient_composition "NG.Class unit"
FactG fcomp "some_elem (NG.Class unit)"
using NG.group_isomorphism_Factor_Group_class_reps
by (force simp: FactG_def fcomp_def)
interpret Group_FactG: Group FactG fcomp "some_elem (NG.Class unit)"
using iso.target.Group_axioms .
have fin_FactG: "finite FactG"
using NG.class_reps_subset FactG_def fin finite_subset by blast
have card_FactG: "card FactG = card NG.Factor_Group"
using NG.card_class_reps FactG_def by simp
have FG_lt': "card FactG < card G"
using FG_lt card_FactG by simp
obtain K' where K'_sub: "Subgroup K' FactG fcomp (some_elem (NG.Class unit))"
and K'_card: "card K' = p ^ (m - 1)"
by (metis FG_lt' card_FactG fin_FactG iso.target.Group_axioms less.hyps pa1_dvd)
define inv_η where "inv_η ≡ restrict (inv_into NG.Factor_Group (restrict some_elem NG.Factor_Group)) FactG"
interpret inv_iso: group_isomorphism inv_η FactG fcomp "some_elem (NG.Class unit)"
NG.Factor_Group NG.quotient_composition "NG.Class unit"
using iso.inverse_group_isomorphism by (simp add: inv_η_def)
define K where "K ≡ inv_η ` K'"
have K_sub: "Subgroup K NG.Factor_Group NG.quotient_composition (NG.Class unit)"
unfolding K_def using inv_iso.image_subgroup[OF K'_sub] .
have "inj_on inv_η K'"
using inv_iso.injective K'_sub
by (meson inj_on_subset Subgroup_def Submonoid.subset)
then have K_card: "card K = p ^ (m - 1)"
unfolding K_def using K'_card card_image by metis
define H where "H ≡ {g ∈ G. NG.Class g ∈ K}"
interpret NG_hom: group_homomorphism NG.Class G composition unit
NG.Factor_Group NG.quotient_composition "NG.Class unit"
by (simp add: G.Group_axioms NG.natural.Monoid_homomorphism_axioms NG.quotient.Group_axioms
group_homomorphism_def)
have H_sub: "Subgroup H G composition unit"
unfolding H_def using K_sub NG_hom.preimage_subgroup by blast
have K_in_image: "K ⊆ NG.Class ` G"
using K_sub NG.natural.surjective by (metis Subgroup_def Submonoid.subset)
have "card H = card K * card NG_hom.Ker"
unfolding H_def
using NG_hom.preimage_card[OF K_sub fin fin_FG K_in_image] .
moreover have "NG_hom.Ker = N"
proof
show "NG_hom.Ker ⊆ N"
using NG.Normal_def NG_hom.Ker_image subsetI by blast
show "N ⊆ NG_hom.Ker"
using G.left_unit G.unit_closed NG.Class_eq NG.CongruenceI NG.sub NG_hom.Ker_memI
by (metis subsetI)
qed
moreover have "card K * card N = p ^ m"
by (simp add: False power_eq_if K_card card_N)
ultimately have "card H = p ^ m" by simp
with H_sub show ?thesis by blast
qed
next
case False
interpret conj: Group_Action G composition unit G.φ_conj G
by (rule G.conjugation_action)
have False if "∀y ∈ G. y ∉ G.center ⟶ p dvd card (conj.orbit y)"
proof -
have "p dvd card (G - G.center)"
using conj.dvd_card_nonfixed_points[OF fin]
by (simp add: G.center_eq_fixed_points that)
with False show False
by (metis G.center_subset card_Diff_subset card_mono dvd_diffD1 fin finite_subset p_dvd_G)
qed
then obtain y where yG: "y ∈ G" and y_not_center: "y ∉ G.center"
and not_dvd_orbit: "¬ p dvd card (conj.orbit y)"
by blast
define X where "X ≡ conj.orbit y"
have orbit_stab: "card G = card X * card (conj.stabilizer y)"
using conj.orbit_stabilizer_card[OF yG fin] X_def by simp
have stab_eq: "conj.stabilizer y = G.centralizer y"
using G.centralizer_eq_stabilizer[OF yG] by simp
have "coprime (card X) (p ^ m)"
using X_def assms(1) not_dvd_orbit prime_imp_power_coprime by blast
then have pa_dvd_cent: "p ^ m dvd card (G.centralizer y)"
by (metis pa_dvd orbit_stab stab_eq coprime_dvd_mult_right_iff coprime_commute)
have cent_grp: "Group (G.centralizer y) composition unit"
using G.centralizer_subgroup yG Subgroup_def by meson
have cent_fin: "finite (G.centralizer y)"
using fin G.centralizer_subset by (rule rev_finite_subset)
have "card (G.centralizer y) < card G"
using G.centralizer_proper[OF yG y_not_center fin] .
then obtain H where H_sub: "Subgroup H (G.centralizer y) composition unit"
and H_card: "card H = p ^ m"
using cent_fin cent_grp less.hyps pa_dvd_cent by blast
then show ?thesis
using subgroup_transitive[OF H_sub] G.centralizer_subgroup[OF yG] by auto
qed
qed
qed
text ‹Cauchy's theorem for arbitrary finite groups is now an immediate corollary of the
first Sylow theorem: taking @{term "m = 1"} yields a subgroup of order @{term p}, and a
group of prime order is cyclic, so any of its non-unit elements has order exactly @{term p}.)›
corollary (in Group) Cauchy:
fixes p :: nat
assumes prime: "prime p" and fin: "finite G" and dvd: "p dvd card G"
shows "∃g∈G. element_order g = p"
proof -
have "p ^ 1 dvd card G" using dvd by simp
then obtain H where H: "Subgroup H G (⋅) 𝟭" and cardH: "card H = p"
using Sylow_I[OF prime fin, of 1] by auto
interpret H: Subgroup H G "(⋅)" 𝟭 by (rule H)
have finH: "finite H" using fin H.subset by (rule rev_finite_subset)
have "card H ≠ 1"
using cardH prime by force
then obtain g where gH: "g ∈ H" and gne: "g ≠ 𝟭"
using is_singleton_altdef is_singleton_iff_ex1[of H] by blast
have dvdp: "H.sub.element_order g dvd p"
using H.sub.element_order_dvd_card[OF finH gH] cardH by simp
have "H.sub.element_order g ≠ 1"
using fin gH gne power_element_order by force
with gH H.subset show ?thesis
using dvdp prime by (auto simp: prime_nat_iff)
qed
section ‹The Second Sylow Theorem›
text ‹If H is a subgroup of a group G and g is in G, then the conjugate
@{text "g H g⇧-⇧1"} is again a subgroup of G.›
context Group begin
definition conjugate_subgroup :: "'a ⇒ 'a set ⇒ 'a set"
where "conjugate_subgroup g H = conjugation g ` H"
lemma conjugate_subgroup_mem_iff:
assumes "g ∈ G" "H ⊆ G" "x ∈ G"
shows "x ∈ conjugate_subgroup g H ⟷ (∃h ∈ H. x = g ⋅ h ⋅ inverse g)"
unfolding conjugate_subgroup_def using assms
by (auto simp: conjugation_def)
lemma conjugate_subgroup_subset:
assumes "H ⊆ G"
shows "conjugate_subgroup g H ⊆ G"
using assms by (auto simp: conjugate_subgroup_def conjugation_def)
lemma conjugate_subgroup_card:
assumes "H ⊆ G" "finite H"
shows "card (conjugate_subgroup g H) = card H"
using card_image[of "conjugation g" H] inj_on_subset[OF bij_betw_imp_inj_on[OF conjugation_bij] ‹H⊆G›]
by (metis conjugation_def conjugate_subgroup_def conjugation_unit ext unit_closed)
text ‹Conjugation is a homomorphism: it distributes over products and inverses.›
lemma conjugation_hom:
assumes "h1 ∈ G" "h2 ∈ G"
shows "conjugation g h1 ⋅ conjugation g h2 = conjugation g (h1 ⋅ h2)"
using assms by (simp add: conjugation_def associative invertible_left_inverse2)
lemma conjugation_inverse:
assumes "h ∈ G"
shows "conjugation g (inverse h) = inverse (conjugation g h)"
using conjugation_def assms inverse_composition_commute by auto
lemma conjugate_subgroup_is_subgroup:
assumes sub: "Subgroup H G (⋅) 𝟭" and g: "g ∈ G"
shows "Subgroup (conjugate_subgroup g H) G (⋅) 𝟭"
proof -
interpret H: Subgroup H G "(⋅)" 𝟭 using sub .
show ?thesis
proof (rule subgroupI)
show "conjugate_subgroup g H ⊆ G"
by (simp add: H.subset conjugate_subgroup_subset g)
next
have "conjugation g 𝟭 = 𝟭" using g by (simp add: conjugation_def)
then show "𝟭 ∈ conjugate_subgroup g H"
using H.subset conjugate_subgroup_mem_iff g by force
next
fix x y assume "x ∈ conjugate_subgroup g H" "y ∈ conjugate_subgroup g H"
then obtain hx hy where "hx ∈ H" "x = conjugation g hx"
and "hy ∈ H" "y = conjugation g hy" and "x ⋅ y = conjugation g (hx ⋅ hy)"
using conjugate_subgroup_def conjugation_hom by auto
then show "x ⋅ y ∈ conjugate_subgroup g H"
using conjugate_subgroup_def by blast
next
fix x assume "x ∈ conjugate_subgroup g H"
then obtain h where h: "h ∈ H" "x = conjugation g h"
unfolding conjugate_subgroup_def by auto
have hG: "h ∈ G" using h(1) H.subset by auto
show "invertible x" using h(2) conjugation_closed[OF g hG] by auto
show "inverse x ∈ conjugate_subgroup g H"
using h conjugation_inverse[OF hG]
by (metis H.sub.invertible H.submonoid_inverse_closed conjugate_subgroup_def imageI)
qed
qed
lemma conjugate_subgroup_self:
assumes sub: "Subgroup H G (⋅) 𝟭" and gH: "g ∈ H" and fin: "finite G"
shows "conjugate_subgroup g H = H"
proof -
interpret H: Subgroup H G "(⋅)" 𝟭 using sub .
have finH: "finite H" using fin H.subset finite_subset by auto
have "conjugate_subgroup g H ⊆ H"
using gH by (auto simp: conjugate_subgroup_def conjugation_def)
then show ?thesis
by (simp add: H.subset card_subset_eq conjugate_subgroup_card finH gH)
qed
lemma conjugate_subgroup_unit:
assumes "H ⊆ G"
shows "conjugate_subgroup 𝟭 H = H"
using assms by (force simp: conjugate_subgroup_def conjugation_unit)
lemma conjugate_subgroup_compose:
assumes "g ∈ G" "h ∈ G" "H ⊆ G"
shows "conjugate_subgroup (g ⋅ h) H = conjugate_subgroup g (conjugate_subgroup h H)"
unfolding conjugate_subgroup_def
using assms by (auto simp: conjugation_compose intro: imageI)
text ‹If @{term H} normalises @{term K} (i.e.\ every element of @{term H} conjugates @{term K}
to itself), then the set product @{term "HK = H × K"} is a subgroup of @{term G}.›
definition subgroup_product :: "'a set ⇒ 'a set ⇒ 'a set"
where "subgroup_product H K = (λ(h,k). h ⋅ k) ` (H × K)"
lemma subgroup_product_mem_iff:
"x ∈ subgroup_product H K ⟷ (∃h ∈ H. ∃k ∈ K. x = h ⋅ k)"
unfolding subgroup_product_def by auto
lemma subgroup_product_subset:
assumes "H ⊆ G" "K ⊆ G"
shows "subgroup_product H K ⊆ G"
unfolding subgroup_product_def using assms by auto
lemma
assumes "Subgroup K G (⋅) 𝟭" "H ⊆ G"
shows subgroup_product_superset_left: "H ⊆ subgroup_product H K"
and subgroup_product_superset_right: "H ⊆ subgroup_product K H"
proof -
interpret K: Subgroup K G "(⋅)" 𝟭 using assms(1) .
show "H ⊆ subgroup_product H K" "H ⊆ subgroup_product K H"
using assms(2) subgroup_product_mem_iff by force+
qed
lemma normalizes_subgroup_product_is_subgroup:
assumes Hsub: "Subgroup H G (⋅) 𝟭"
and Ksub: "Subgroup K G (⋅) 𝟭"
and norm: "∀h ∈ H. conjugate_subgroup h K = K"
shows "Subgroup (subgroup_product H K) G (⋅) 𝟭"
proof -
interpret H: Subgroup H G "(⋅)" 𝟭 using Hsub .
interpret K: Subgroup K G "(⋅)" 𝟭 using Ksub .
have swap: "∃k' ∈ K. k ⋅ h = h ⋅ k'" if "k ∈ K" "h ∈ H" for k h
proof -
have "conjugation (inverse h) k ∈ K"
by (metis H.image_of_inverse_iff conjugate_subgroup_def image_eqI norm that)
moreover have "conjugation (inverse h) k = inverse h ⋅ k ⋅ h"
by (simp add: conjugation_def that)
moreover have "k ⋅ h = h ⋅ (inverse h ⋅ k ⋅ h)"
by (simp add: that flip: associative)
ultimately show ?thesis by auto
qed
show ?thesis
proof (rule subgroupI)
show "subgroup_product H K ⊆ G"
by (simp add: H.subset K.subset subgroup_product_subset)
show "𝟭 ∈ subgroup_product H K"
using subgroup_product_mem_iff by force
next
fix x y
assume xHK: "x ∈ subgroup_product H K" and yHK: "y ∈ subgroup_product H K"
obtain h1 k1 where h1H: "h1 ∈ H" and k1K: "k1 ∈ K" and xeq: "x = h1 ⋅ k1"
using xHK unfolding subgroup_product_mem_iff by auto
obtain h2 k2 where h2H: "h2 ∈ H" and k2K: "k2 ∈ K" and yeq: "y = h2 ⋅ k2"
using yHK unfolding subgroup_product_mem_iff by auto
obtain k' where k'K: "k' ∈ K" and k'eq: "k1 ⋅ h2 = h2 ⋅ k'"
using swap[OF k1K h2H] by auto
have "x ⋅ y = h1 ⋅ k1 ⋅ (h2 ⋅ k2)" using xeq yeq by simp
also have "… = (h1 ⋅ h2) ⋅ (k' ⋅ k2)"
by (metis H.sub K.sub associative composition_closed h1H h2H k'K k'eq k1K k2K)
finally have "x ⋅ y = (h1 ⋅ h2) ⋅ (k' ⋅ k2)" .
then show "x ⋅ y ∈ subgroup_product H K"
using h1H h2H k'K k2K subgroup_product_mem_iff by auto
next
fix g assume "g ∈ subgroup_product H K"
then obtain h k where hH: "h ∈ H" and kK: "k ∈ K" and geq: "g = h ⋅ k"
unfolding subgroup_product_mem_iff by auto
show "invertible g"
by (simp add: geq hH kK)
have "inverse g = inverse k ⋅ inverse h"
by (simp add: geq hH inverse_composition_commute kK)
moreover obtain ikK: "inverse k ∈ K" and ihH: "inverse h ∈ H"
using hH kK by blast
ultimately show "inverse g ∈ subgroup_product H K"
using local.swap subgroup_product_mem_iff by metis
qed
qed
text ‹The normalizer of a subgroup @{term H} in @{term G}: the set of elements
that normalize @{term H} under conjugation.›
definition normalizer :: "'a set ⇒ 'a set"
where "normalizer H ≡ {g ∈ G. conjugate_subgroup g H = H}"
lemma normalizer_subset: "normalizer H ⊆ G"
unfolding normalizer_def by auto
lemma normalizer_mem_iff:
"g ∈ normalizer H ⟷ g ∈ G ∧ conjugate_subgroup g H = H"
unfolding normalizer_def by auto
lemma normalizer_subgroup:
assumes sub: "Subgroup H G (⋅) 𝟭" and fin: "finite G"
shows "Subgroup (normalizer H) G (⋅) 𝟭"
proof (rule subgroupI)
interpret H: Subgroup H G "(⋅)" 𝟭 using sub .
show "𝟭 ∈ normalizer H"
by (simp add: H.subset conjugate_subgroup_unit normalizer_mem_iff)
fix g h assume gN: "g ∈ normalizer H" and hN: "h ∈ normalizer H"
then show "g ⋅ h ∈ normalizer H"
using H.subset conjugate_subgroup_compose normalizer_mem_iff by force
fix g assume gN: "g ∈ normalizer H"
then have gG: "g ∈ G" and gH: "conjugate_subgroup g H = H"
unfolding normalizer_mem_iff by auto
have "conjugate_subgroup (inverse g) H = conjugate_subgroup (inverse g ⋅ g) H"
using H.subset conjugate_subgroup_compose gG gH invertible invertible_inverse_closed
by presburger
also have "… = H"
by (simp add: conjugate_subgroup_self fin gG sub)
finally show "inverse g ∈ normalizer H"
by (simp add: normalizer_mem_iff gG)
qed (auto simp: normalizer_subset normalizer_mem_iff)
lemma subgroup_subset_normalizer:
assumes sub: "Subgroup H G (⋅) 𝟭" and "finite G"
shows "H ⊆ normalizer H"
proof
fix h assume hH: "h ∈ H"
interpret H: Subgroup H G "(⋅)" 𝟭 using sub .
show "h ∈ normalizer H"
by (simp add: conjugate_subgroup_self hH normalizer_mem_iff assms)
qed
lemma normal_in_normalizer:
assumes sub: "Subgroup H G (⋅) 𝟭" and fin: "finite G"
shows "normal_subgroup H (normalizer H) (⋅) 𝟭"
proof -
interpret H: Subgroup H G "(⋅)" 𝟭 using sub .
interpret N: Subgroup "normalizer H" G "(⋅)" 𝟭
using normalizer_subgroup[OF sub fin] .
have sub_H_N: "Subgroup H (normalizer H) (⋅) 𝟭"
proof
qed (auto simp: subgroup_subset_normalizer[OF sub fin])
show ?thesis
proof (intro normal_subgroup.intro subgroup_of_group.intro sub_H_N N.sub.Group_axioms)
show "normal_subgroup_axioms H (normalizer H) (⋅) 𝟭"
proof
fix g k assume gN: "g ∈ normalizer H" and kH: "k ∈ H"
have igH: "conjugate_subgroup (inverse g) H = H"
using normalizer_subgroup[OF sub fin] gN normalizer_mem_iff by blast
have "conjugation (inverse g) k ∈ conjugate_subgroup (inverse g) H"
unfolding conjugate_subgroup_def using kH by auto
then show "N.sub.inverse g ⋅ k ⋅ g ∈ H"
using conjugation_def gN igH kH H.subset by fastforce
qed
qed
qed
text ‹The order formula for a product whose factors normalize one another in the
relevant direction. The second isomorphism theorem supplies the quotient
cardinalities, so this bridge remains entirely within the native set-based API.›
lemma normalizes_subgroup_product_card:
assumes Hsub: "Subgroup H G (⋅) 𝟭"
and Ksub: "Subgroup K G (⋅) 𝟭"
and norm: "∀h ∈ H. conjugate_subgroup h K = K"
and fin: "finite G"
shows "card (subgroup_product H K) * card (H ∩ K) = card H * card K"
proof -
interpret H: Subgroup H G "(⋅)" 𝟭 using Hsub .
interpret K: Subgroup K G "(⋅)" 𝟭 using Ksub .
have product_sub: "Subgroup (subgroup_product H K) G (⋅) 𝟭"
by (rule normalizes_subgroup_product_is_subgroup[OF Hsub Ksub norm])
then interpret product: Subgroup "subgroup_product H K" G "(⋅)" 𝟭 .
interpret N: Subgroup "normalizer K" G "(⋅)" 𝟭
by (rule normalizer_subgroup[OF Ksub fin])
have product_subset_N: "subgroup_product H K ⊆ normalizer K"
proof
fix x
assume x: "x ∈ subgroup_product H K"
obtain h k where hH: "h ∈ H" and kK: "k ∈ K" and xeq: "x = h ⋅ k"
using x unfolding subgroup_product_mem_iff by auto
obtain "h ∈ normalizer K" and "k ∈ normalizer K"
using Ksub conjugate_subgroup_self fin hH kK norm normalizer_mem_iff by auto
then show "x ∈ normalizer K"
using xeq N.sub_composition_closed by simp
qed
have product_N_sub: "Subgroup (subgroup_product H K) (normalizer K) (⋅) 𝟭"
by (meson N.Subgroup_axioms product_sub product_subset_N subgroup_restrict)
interpret KN: normal_subgroup K "normalizer K" "(⋅)" 𝟭
by (simp add: Ksub fin normal_in_normalizer)
have K_product: "K ⊆ subgroup_product H K"
by (rule subgroup_product_superset_right[OF Hsub K.subset])
have K_product_sub: "Subgroup K (subgroup_product H K) (⋅) 𝟭"
by (meson K_product Ksub product_sub subgroup_restrict)
have K_normal_product: "normal_subgroup K (subgroup_product H K) (⋅) 𝟭"
proof (intro normal_subgroup.intro subgroup_of_group.intro K_product_sub product.sub.Group_axioms)
show "normal_subgroup_axioms K (subgroup_product H K) (⋅) 𝟭"
proof
fix g k
assume gP: "g ∈ subgroup_product H K" and kK: "k ∈ K"
have inverse_eq: "product.sub.inverse g = N.sub.inverse g"
using gP product_N_sub by (metis Subgroup.subgroup_inverse_equality)
show "product.sub.inverse g ⋅ k ⋅ g ∈ K"
using KN.normal gP inverse_eq kK product_subset_N by auto
qed
qed
then interpret KP: normal_subgroup K "subgroup_product H K" "(⋅)" 𝟭 .
have H_product_sub: "Subgroup H (subgroup_product H K) (⋅) 𝟭"
by (meson H.subset Hsub Ksub product_sub subgroup_product_superset_left subgroup_restrict)
have HIntK_product_sub:
"Subgroup (H ∩ K) (subgroup_product H K) (⋅) 𝟭"
by (rule product.sub.subgroup_intersection[OF H_product_sub K_product_sub])
have HIntK_H_sub: "Subgroup (H ∩ K) H (⋅) 𝟭"
using HIntK_product_sub H_product_sub subgroup_restrict by fastforce
interpret HIntK: normal_subgroup "H ∩ K" H "(⋅)" 𝟭
proof (intro normal_subgroup.intro subgroup_of_group.intro HIntK_H_sub H.sub.Group_axioms)
show "normal_subgroup_axioms (H ∩ K) H (⋅) 𝟭"
by (simp add: H_product_sub K_normal_product normal_subgroup.axioms(2)
product.sub.normal_subgroup_intersection)
qed
have H_product_group: "subgroup_of_group H (subgroup_product H K) (⋅) 𝟭"
by (rule subgroup_of_groupI[OF H_product_sub product.sub.Group_axioms])
have product_locale:
"normal_subgroup_product K H (subgroup_product H K) (⋅) 𝟭"
by (rule normal_subgroup_product.intro[OF K_normal_product H_product_group])
interpret iso: second_iso_theorem K H "subgroup_product H K" "(⋅)" 𝟭
by (rule second_iso_theorem.intro[OF product_locale])
have iso_product: "iso.HK = subgroup_product H K"
by (simp add: iso.HK_def subgroup_product_def)
have fract_left: "iso.Fract_HK_K = KP.Partition"
unfolding iso.Fract_HK_K_def iso_product KP.Partition_def by rule
have fract_right: "iso.Fract_H_HIntK = HIntK.Partition"
unfolding iso.Fract_H_HIntK_def HIntK.Partition_def by rule
have finH: "finite H" using finite_subset[OF H.subset fin] .
have fin_product: "finite (subgroup_product H K)"
using finite_subset[OF subgroup_product_subset[OF H.subset K.subset] fin] .
have card_left: "card iso.Fract_HK_K = KP.index"
using KP.card_Factor_Group[OF fin_product] fract_left by simp
have card_right: "card iso.Fract_H_HIntK = HIntK.index"
using HIntK.card_Factor_Group[OF finH] fract_right by simp
have iso_card: "card iso.Fract_HK_K = card iso.Fract_H_HIntK"
proof -
obtain f composition unit composition' unit' where f:
"group_isomorphism f iso.Fract_HK_K composition unit
iso.Fract_H_HIntK composition' unit'"
using iso.second_isomorphism unfolding isomorphic_as_groups_def by auto
interpret f: group_isomorphism f iso.Fract_HK_K composition unit
iso.Fract_H_HIntK composition' unit' using f .
show ?thesis using f.bijective by (rule bij_betw_same_card)
qed
have card_product: "card (subgroup_product H K) = card K * card iso.Fract_HK_K"
using KP.lagrange[OF fin_product] card_left iso_product by simp
have card_H: "card H = card (H ∩ K) * card iso.Fract_H_HIntK"
using HIntK.lagrange[OF finH] card_right fract_right by simp
have "card (subgroup_product H K) * card (H ∩ K)
= card K * (card (H ∩ K) * card iso.Fract_H_HIntK)"
by (simp add: card_product iso_card)
also have "… = card H * card K"
by (simp add: card_H)
finally show ?thesis .
qed
text ‹Sylow @{term p}-subgroups: subgroups whose order is the largest power of @{term p}
dividing @{term "card G"}.›
definition Sylow_subgroups :: "nat ⇒ 'a set set"
where "Sylow_subgroups p =
{H. Subgroup H G (⋅) 𝟭 ∧ card H = p ^ multiplicity p (card G)}"
text ‹Sylow @{term p}-subgroups exist by the first Sylow theorem.›
lemma Sylow_subgroups_nonempty:
assumes "prime p" "finite G"
shows "Sylow_subgroups p ≠ {}"
using Sylow_I[OF assms] multiplicity_dvd by (auto simp: Sylow_subgroups_def)
text ‹Conjugation preserves Sylow @{term p}-subgroups.›
lemma conjugate_Sylow_is_Sylow:
assumes "P ∈ Sylow_subgroups p" "g ∈ G" "finite G"
shows "conjugate_subgroup g P ∈ Sylow_subgroups p"
proof -
interpret Subgroup P G "(⋅)" 𝟭
using Sylow_subgroups_def assms by blast
show ?thesis
using assms conjugate_subgroup_card
by (simp add: Sylow_subgroups_def conjugate_subgroup_is_subgroup finite_subset subset)
qed
text ‹The conjugation action on subsets of @{term G}: each @{term "g ∈ G"} maps a subset
@{term H} to @{term "conjugation g ` H"}. We restrict to @{term "Sylow_subgroups p"}
to obtain a group action.›
definition φ_Sylow :: "nat ⇒ 'a ⇒ 'a set ⇒ 'a set"
where "φ_Sylow p g = restrict (conjugate_subgroup g) (Sylow_subgroups p)"
lemma Sylow_subgroups_subgroup:
"P ∈ Sylow_subgroups p ⟹ Subgroup P G (⋅) 𝟭"
unfolding Sylow_subgroups_def by auto
lemma Sylow_subgroups_subset:
"P ∈ Sylow_subgroups p ⟹ P ⊆ G"
unfolding Sylow_subgroups_def using Submonoid.subset Subgroup_def by fastforce
lemma Sylow_subgroups_card:
"P ∈ Sylow_subgroups p ⟹ card P = p ^ multiplicity p (card G)"
unfolding Sylow_subgroups_def by auto
lemma φ_Sylow_mapsto:
assumes "g ∈ G" "prime p" "finite G"
shows "φ_Sylow p g ∈ Sylow_subgroups p →⇩E Sylow_subgroups p"
unfolding φ_Sylow_def PiE_def Pi_def
using conjugate_Sylow_is_Sylow assms by auto
lemma φ_Sylow_bij:
assumes g: "g ∈ G" and p: "prime p" and fin: "finite G"
shows "bij_betw (φ_Sylow p g) (Sylow_subgroups p) (Sylow_subgroups p)"
proof (intro bij_betw_byWitness strip)
show "φ_Sylow p (inverse g) (φ_Sylow p g P) = P" if P: "P ∈ Sylow_subgroups p" for P
proof -
have Psub: "P ⊆ G" using Sylow_subgroups_subset[OF P] .
have gP: "conjugate_subgroup g P ∈ Sylow_subgroups p"
using conjugate_Sylow_is_Sylow[OF P g fin] .
show "φ_Sylow p (inverse g) (φ_Sylow p g P) = P"
unfolding φ_Sylow_def using P gP
by (metis conjugate_subgroup_unit Psub conjugate_subgroup_compose g
invertible invertible_inverse_closed invertible_left_inverse restrict_apply)
qed
show "φ_Sylow p g (φ_Sylow p (inverse g) Q) = Q" if Q: "Q ∈ Sylow_subgroups p" for Q
proof -
have igQ: "conjugate_subgroup (inverse g) Q ∈ Sylow_subgroups p"
using conjugate_Sylow_is_Sylow[OF Q _ fin] g by auto
show "φ_Sylow p g (φ_Sylow p (inverse g) Q) = Q"
unfolding φ_Sylow_def using Q igQ Sylow_subgroups_subset[OF Q]
by (metis conjugate_subgroup_unit conjugate_subgroup_compose g
invertible invertible_inverse_closed invertible_right_inverse restrict_apply)
qed
qed (use φ_Sylow_mapsto[OF _ p fin] g in ‹auto simp: PiE_def Pi_def›)
lemma φ_Sylow_unit:
assumes "prime p" "finite G"
shows "φ_Sylow p 𝟭 = identity (Sylow_subgroups p)"
using Sylow_subgroups_subset φ_Sylow_def conjugate_subgroup_unit by fastforce
lemma φ_Sylow_compose:
assumes g: "g ∈ G" "h ∈ G" "prime p" "finite G"
shows "φ_Sylow p (g ⋅ h) = compose (Sylow_subgroups p) (φ_Sylow p g) (φ_Sylow p h)"
unfolding φ_Sylow_def compose_def
by (force simp: Sylow_subgroups_subset conjugate_Sylow_is_Sylow conjugate_subgroup_compose assms)
lemma φ_Sylow_action:
assumes "prime p" "finite G"
shows "Group_Action G (⋅) 𝟭 (φ_Sylow p) (Sylow_subgroups p)"
proof
fix g assume "g ∈ G"
then show "φ_Sylow p g ∈ Monoid.Units (Sylow_subgroups p →⇩E Sylow_subgroups p)
(compose (Sylow_subgroups p)) (identity (Sylow_subgroups p))"
using φ_Sylow_mapsto φ_Sylow_bij assms
by (intro transformations.Units_bij_betwD) auto
qed (use φ_Sylow_unit φ_Sylow_compose assms in auto)
lemma prime_power_dvd_not_prime_dvd:
fixes p d :: nat and k :: nat
assumes "prime p" "d dvd p ^ k" "¬ p dvd d"
shows "d = 1"
by (metis assms dvd_trans prime_dvd_power prime_factor_nat primes_dvd_imp_eq)
text ‹The second Sylow theorem: any two Sylow @{term p}-subgroups of @{term G} are conjugate.
That is, the conjugation action of @{term G} on @{term "Sylow_subgroups p"} is transitive.›
theorem Sylow_II:
assumes "prime p" "finite G"
and "P ∈ Sylow_subgroups p" "Q ∈ Sylow_subgroups p"
shows "∃g ∈ G. conjugate_subgroup g P = Q"
proof -
interpret act: Group_Action G "(⋅)" 𝟭 "φ_Sylow p" "Sylow_subgroups p"
using φ_Sylow_action[OF assms(1,2)] .
text ‹Let @{term P} act on @{term "Sylow_subgroups p"} by conjugation.
Consider the orbits of this restricted action. The key combinatorial
argument shows that @{term Q} must lie in the orbit of @{term P}.›
have P_self_orbit: "∀g ∈ P. conjugate_subgroup g P = P"
using Sylow_subgroups_subgroup assms conjugate_subgroup_self by blast
text ‹Transitivity of the conjugation action via the left-coset counting
argument. @{term P} acts on the left cosets of @{term Q} by left multiplication.
Since the number of cosets is coprime to @{term p}, there must be a fixed coset,
which yields the conjugating element.›
interpret Psub: Subgroup P G "(⋅)" 𝟭
using Sylow_subgroups_subgroup[OF assms(3)] .
interpret Qsub: Subgroup Q G "(⋅)" 𝟭
using Sylow_subgroups_subgroup[OF assms(4)] .
interpret QG: subgroup_of_group Q G "(⋅)" 𝟭
by (simp add: Qsub.Subgroup_axioms Group_axioms subgroup_of_group_def)
have finP: "finite P" using assms(2) Psub.subset finite_subset by auto
have finQ: "finite Q" using assms(2) Qsub.subset finite_subset by auto
define k where "k ≡ multiplicity p (card G)"
have cardP': "card P = p ^ k" and cardQ': "card Q = p ^ k"
using Sylow_subgroups_card assms k_def by blast+
have p_pos: "p > 0"
by (simp add: assms(1) prime_gt_0_nat)
have cardG_pos: "card G > 0"
using Psub.subset assms(2) card_0_eq by blast
then have "QG.index = card G div (p ^ k)"
using QG.lagrange assms(2) cardQ' by auto
then have not_p_dvd_index: "¬ p dvd QG.index"
using multiplicity_decompose[of concl: p]
using assms(1) cardG_pos k_def not_prime_unit by auto
define L where "L = (λg. g ⋅| Q) ` G"
have finL: "finite L"
using L_def assms(2) by blast
have L_sub_Omega: "L ⊆ Ω (p ^ k)"
by (auto simp: L_def Qsub.subset Ω_memI φ_left_closed act.Left_Coset_def cardQ')
interpret P_act: Group_Action P "(⋅)" 𝟭 "φ_left (p ^ k)" "Ω (p ^ k)"
proof
fix g assume gP: "g ∈ P"
then show "φ_left (p ^ k) g
∈ Monoid.Units (Ω (p ^ k) →⇩E Ω (p ^ k)) (compose (Ω (p ^ k))) (identity (Ω (p ^ k)))"
by (simp add: φ_left_bij φ_left_mapsto transformations.Units_bijective)
qed (auto simp add: φ_left_unit φ_left_compose)
have Q_in_Omega: "Q ∈ Ω (p ^ k)"
using Qsub.subset cardQ' by auto
have stab_Q: "P_act.stabilizer Q = P ∩ Q"
proof (intro antisym subsetI)
fix a
assume "a ∈ P_act.stabilizer Q"
then have aP: "a ∈ P" and eq: "φ_left (p ^ k) a Q = Q"
unfolding P_act.stabilizer_def by auto
have "(⋅) a ` Q = Q" using Q_in_Omega eq by simp
with aP show "a ∈ P ∩ Q"
by (metis IntI Psub.sub.right_unit Qsub.sub_unit_closed image_eqI)
next
fix a
assume a: "a ∈ P ∩ Q"
then have "(⋅) a ` Q = Q"
by (simp add: Qsub.sub.left_mult_image_card Qsub.sub.left_mult_image_subset
card_subset_eq finQ)
then show "a ∈ P_act.stabilizer Q"
unfolding P_act.stabilizer_def using a by (simp add: Q_in_Omega)
qed
have orbit_dvd: "card (P_act.orbit Q) dvd p ^ k"
by (metis P_act.orbit_stabilizer_card Q_in_Omega cardP' dvd_triv_left finP)
have orbit_sub_L: "P_act.orbit Q ⊆ L"
using P_act.orbit_mem_iff Q_in_Omega by (auto simp: L_def coset_notation.Left_Coset_def)
have union_L: "⋃L = G"
proof
show "⋃L ⊆ G"
unfolding L_def coset_notation.Left_Coset_def using Qsub.subset by auto
show "G ⊆ ⋃L"
using L_def Qsub.sub_unit_closed act.Left_Coset_memI right_unit by (metis UN_iff subsetI)
qed
have disj_L: "C1 ∩ C2 = {}"
if C1L: "C1 ∈ L" and C2L: "C2 ∈ L" and neq: "C1 ≠ C2" for C1 C2
proof -
obtain g1 g2 where g1G: "g1 ∈ G" and C1eq: "C1 = g1 ⋅| Q"
and g2G: "g2 ∈ G" and C2eq: "C2 = g2 ⋅| Q"
using C1L C2L unfolding L_def by auto
show "C1 ∩ C2 = {}"
proof (rule ccontr)
assume "C1 ∩ C2 ≠ {}"
then obtain x where xC1: "x ∈ C1" and xC2: "x ∈ C2" by auto
obtain q1 q2 where q1Q: "q1 ∈ Q" and xeq1: "x = g1 ⋅ q1"
and q2Q: "q2 ∈ Q" and xeq2: "x = g2 ⋅ q2"
and eq12: "g1 ⋅ q1 = g2 ⋅ q2"
using C1eq C2eq xC1 xC2 by fastforce
have q1G: "q1 ∈ G" and q2G: "q2 ∈ G" using q1Q q2Q Qsub.subset by auto
have "C1 = C2"
proof (intro antisym subsetI)
fix y
assume "y ∈ C1"
then obtain r where rQ: "r ∈ Q" and yeq: "y = g1 ⋅ r"
unfolding C1eq coset_notation.Left_Coset_def by auto
have rG: "r ∈ G" using rQ Qsub.subset by auto
have iq1Q: "inverse q1 ∈ Q"
using q1Q by (intro Qsub.submonoid_inverse_closed) auto
have "q2 ⋅ inverse q1 ⋅ r ∈ Q"
using q2Q iq1Q rQ by (intro Qsub.sub_composition_closed) auto
moreover have "y = g2 ⋅ (q2 ⋅ inverse q1 ⋅ r)"
proof -
have "g2 ⋅ (q2 ⋅ inverse q1 ⋅ r) = g2 ⋅ q2 ⋅ inverse q1 ⋅ r"
using g2G q2G q1G rG by (simp add: associative)
also have "… = g1 ⋅ r"
by (metis Qsub.sub associative eq12 g1G invertible invertible_right_inverse iq1Q q1G right_unit)
finally show ?thesis using yeq by simp
qed
ultimately show "y ∈ C2"
unfolding C2eq coset_notation.Left_Coset_def by auto
next
fix y
assume "y ∈ C2"
then obtain r where rQ: "r ∈ Q" and yeq: "y = g2 ⋅ r"
unfolding C2eq coset_notation.Left_Coset_def by auto
have rG: "r ∈ G" using rQ Qsub.subset by auto
have "q1 ⋅ inverse q2 ⋅ r ∈ Q"
using q1Q rQ q2Q by blast
moreover have "y = g1 ⋅ (q1 ⋅ inverse q2 ⋅ r)"
proof -
have "g1 ⋅ (q1 ⋅ inverse q2 ⋅ r) = g1 ⋅ q1 ⋅ inverse q2 ⋅ r"
using g1G q1G q2G rG by (simp add: associative)
also have "… = g2 ⋅ r"
using eq12 g2G q2G rG by (simp add: associative invertible_right_inverse)
finally show ?thesis using yeq by simp
qed
ultimately show "y ∈ C1"
unfolding C1eq coset_notation.Left_Coset_def by auto
qed
with neq show False by contradiction
qed
qed
have card_coset: "⋀C. C ∈ L ⟹ card C = card Q"
using L_sub_Omega cardQ' by auto
have "card G = (∑C∈L. card C)"
unfolding union_L [symmetric]
proof (intro card_Union_disjoint)
show "disjoint L" using disj_L unfolding disjoint_def by auto
show "⋀A. A ∈ L ⟹ finite A"
using union_L ‹finite G› by (meson Union_upper finite_subset)
qed
also have "… = (∑C∈L. card Q)"
by (simp add: card_coset)
finally have "card G = card Q * card L" by simp
with cardG_pos have card_L: "card L = QG.index"
using QG.lagrange by fastforce
have "∃C ∈ L. ∀a ∈ P. (⋅) a ` C = C"
proof (rule ccontr)
assume nofix: "¬ (∃C∈L. ∀a∈P. (⋅) a ` C = C)"
have orbit_in_L: "P_act.orbit C ⊆ L" if "C ∈ L" for C
proof
fix D assume "D ∈ P_act.orbit C"
then obtain a where aP: "a ∈ P" and aG: "a ∈ G" and Deq: "φ_left (p ^ k) a C = D"
by (auto simp: P_act.orbit_def)
obtain g where gG: "g ∈ G" and Ceq: "C = g ⋅| Q" using ‹C ∈ L› unfolding L_def by auto
have "D = (⋅) a ` C" using Deq that L_sub_Omega by auto
also have "… = (a ⋅ g) ⋅| Q"
unfolding coset_notation.Left_Coset_def using aG gG Qsub.subset by (auto simp: Ceq associative)
finally show "D ∈ L" unfolding L_def using aG gG by auto
qed
have orbit_dvd_gen: "card (P_act.orbit C) dvd p ^ k" if "C ∈ L" for C
unfolding dvd_def
using L_sub_Omega P_act.orbit_stabilizer_card cardP' finP that by auto
have orbit_singleton_fixed: "∀a∈P. (⋅) a ` C = C"
if "C ∈ L" "P_act.orbit C = {C}" for C
proof
fix a assume aP: "a ∈ P"
have COmega: "C ∈ Ω (p ^ k)" using that(1) L_sub_Omega by auto
then show "(⋅) a ` C = C"
by (metis P_act.orbit_memI φ_left_apply aP emptyE insert_iff that(2))
qed
have div_ppow: "p dvd d" if "d dvd p ^ k" "d > 1" for d :: nat
using assms(1) prime_power_dvd_not_prime_dvd that by blast
have orbit_p_dvd: "p dvd card (P_act.orbit C)" if CL: "C ∈ L" for C
proof -
have "C ∈ P_act.orbit C"
using L_sub_Omega P_act.orbit_self that by blast
moreover have "P_act.orbit C ≠ {C}"
by (metis nofix orbit_singleton_fixed that)
ultimately have "card (P_act.orbit C) ≠ 1" using card_1_singletonE by force
then show ?thesis using div_ppow
using assms(1) orbit_dvd_gen prime_power_dvd_not_prime_dvd that by blast
qed
define Lorbs where "Lorbs ≡ P_act.orbit ` L"
have cover: "⋃ Lorbs = L"
using L_sub_Omega P_act.orbit_self orbit_in_L by (auto simp: Lorbs_def)
have disj: "disjoint Lorbs"
using P_act.orbit_disjoint L_sub_Omega
by (intro disjointI) (auto simp: Lorbs_def)
have "⋀A. A ∈ Lorbs ⟹ finite A"
using cover finL by (metis Union_upper rev_finite_subset)
then have cardL_sum: "card L = (∑X∈Lorbs. card X)"
using disj card_Union_disjoint cover by blast
have "p dvd (∑X∈Lorbs. card X)"
using orbit_p_dvd by (intro dvd_sum) (auto simp: Lorbs_def)
with cardL_sum not_p_dvd_index show False
by (simp add: card_L)
qed
then obtain g where gG: "g ∈ G" and fixed: "∀a ∈ P. (⋅) a ` (g ⋅| Q) = g ⋅| Q"
using L_def by blast
have conj_sub: "conjugate_subgroup (inverse g) P ⊆ Q"
proof
fix x assume xconj: "x ∈ conjugate_subgroup (inverse g) P"
then obtain a where aP: "a ∈ P" and xeq: "x = conjugation (inverse g) a"
unfolding conjugate_subgroup_def by auto
then have "a ⋅ (g ⋅ 𝟭) ∈ g ⋅| Q"
by (metis Qsub.sub_unit_closed coset_notation.Left_Coset_def fixed imageI)
then show "x ∈ Q"
using gG aP associative conjugation_def gG invertible_left_inverse2 xeq by auto
qed
have "conjugate_subgroup (inverse g) P = Q"
by (simp add: Psub.subset cardP' cardQ' card_subset_eq conj_sub conjugate_subgroup_card finP finQ gG)
then show ?thesis
using gG by blast
qed
text ‹A Sylow subgroup cannot normalize a distinct Sylow subgroup. The
normalized product is a finite subgroup whose order is forced between the
common Sylow order and the maximal p-power dividing @{term "card G"}.›
lemma normalizes_Sylow_subgroups_eq:
assumes prime: "prime p" and fin: "finite G"
and P: "P ∈ Sylow_subgroups p" and Q: "Q ∈ Sylow_subgroups p"
and norm: "∀g ∈ P. conjugate_subgroup g Q = Q"
shows "Q = P"
proof -
interpret Psub: Subgroup P G "(⋅)" 𝟭
using Sylow_subgroups_subgroup[OF P] .
interpret Qsub: Subgroup Q G "(⋅)" 𝟭
using Sylow_subgroups_subgroup[OF Q] .
have finP: "finite P" using finite_subset[OF Psub.subset fin] .
have finQ: "finite Q" using finite_subset[OF Qsub.subset fin] .
define m where "m ≡ multiplicity p (card G)"
have cardP: "card P = p ^ m" and cardQ: "card Q = p ^ m"
using Sylow_subgroups_card P Q by (simp_all add: m_def)
have product_sub: "Subgroup (subgroup_product P Q) G (⋅) 𝟭"
by (rule normalizes_subgroup_product_is_subgroup[OF Psub.Subgroup_axioms Qsub.Subgroup_axioms norm])
interpret product: Subgroup "subgroup_product P Q" G "(⋅)" 𝟭
using product_sub .
interpret productG: subgroup_of_group "subgroup_product P Q" G "(⋅)" 𝟭 ..
have fin_product: "finite (subgroup_product P Q)"
using finite_subset[OF subgroup_product_subset[OF Psub.subset Qsub.subset] fin] .
have "card (subgroup_product P Q) * card (P ∩ Q) = card P * card Q"
by (rule normalizes_subgroup_product_card[OF Psub.Subgroup_axioms Qsub.Subgroup_axioms norm fin])
then have "card (subgroup_product P Q) * card (P ∩ Q) = p ^ (m + m)"
by (simp add: cardP cardQ monoid_mult_class.power_add)
then have product_dvd_power: "card (subgroup_product P Q) dvd p ^ (m + m)"
by (metis dvd_def)
obtain i where i_le: "i ≤ m + m" and card_product: "card (subgroup_product P Q) = p ^ i"
using divides_primepow_nat[OF prime] product_dvd_power by blast
have p_i_dvd_G: "p ^ i dvd card G"
using card_product by (simp add: productG.lagrange[OF fin])
have "G ≠ {}"
using Psub.subset Psub.sub_unit_closed by blast
then have "card G > 0"
using fin by (simp add: card_gt_0_iff)
then have "multiplicity p (p ^ i) ≤ multiplicity p (card G)"
using dvd_imp_multiplicity_le p_i_dvd_G by blast
then have i_le_m: "i ≤ m" using prime by (simp add: m_def)
have P_product: "P ⊆ subgroup_product P Q"
by (rule subgroup_product_superset_left[OF Qsub.Subgroup_axioms Psub.subset])
have "p ^ m ≤ p ^ i"
using card_mono[OF fin_product P_product] cardP card_product by simp
then have "m ≤ i"
using prime prime_gt_1_nat by force
with i_le_m have exp_eq: "i = m" by auto
have P_eq_product: "P = subgroup_product P Q"
by (simp add: P_product cardP card_product card_subset_eq exp_eq fin_product)
have Q_product: "Q ⊆ subgroup_product P Q"
by (rule subgroup_product_superset_right[OF Psub.Subgroup_axioms Qsub.subset])
show ?thesis
using P_eq_product Q_product cardP cardQ finP by (metis card_subset_eq)
qed
text ‹Conjugation is transitive on the Sylow @{term p}-subgroups.›
lemma Sylow_subgroups_orbit:
assumes prime: "prime p" and fin: "finite G"
and P: "P ∈ Sylow_subgroups p"
shows "(λg. φ_Sylow p g P) ` G = Sylow_subgroups p"
proof -
interpret act: Group_Action G "(⋅)" 𝟭 "φ_Sylow p" "Sylow_subgroups p"
using φ_Sylow_action[OF prime fin] .
show "(λg. φ_Sylow p g P) ` G = Sylow_subgroups p"
proof (rule equalityI)
show "Sylow_subgroups p ⊆ (λg. φ_Sylow p g P) ` G"
proof
fix Q assume Q: "Q ∈ Sylow_subgroups p"
obtain g where gG: "g ∈ G" and gPQ: "conjugate_subgroup g P = Q"
using Sylow_II[OF prime fin P Q] by blast
have "φ_Sylow p g P = Q"
unfolding φ_Sylow_def using P gPQ by simp
then show "Q ∈ (λg. φ_Sylow p g P) ` G"
using gG by blast
qed
qed (use P in blast)
qed
text ‹The number of Sylow @{term p}-subgroups divides the group order and is
congruent to one modulo @{term p}.›
theorem
assumes prime: "prime p" and fin: "finite G"
shows Sylow_subgroups_card_dvd: "card (Sylow_subgroups p) dvd card G"
and Sylow_III: "p dvd card (Sylow_subgroups p) - 1"
proof -
have fin_S: "finite (Sylow_subgroups p)"
using Sylow_subgroups_orbit fin prime by (metis equals0I finite.emptyI finite_imageI)
obtain P where P: "P ∈ Sylow_subgroups p"
using Sylow_subgroups_nonempty fin prime by blast
interpret Psub: Subgroup P G "(⋅)" 𝟭
using Sylow_subgroups_subgroup[OF P] .
interpret act: Group_Action G "(⋅)" 𝟭 "φ_Sylow p" "Sylow_subgroups p"
using φ_Sylow_action[OF prime fin] .
have orbit_S: "act.orbit P = Sylow_subgroups p"
using Sylow_subgroups_orbit[OF prime fin P]
by (simp add: act.orbit_eq)
have stab_normalizer: "act.stabilizer P = normalizer P"
unfolding act.stabilizer_def normalizer_def φ_Sylow_def
using P by simp
have orbit_stab:
"card G = card (Sylow_subgroups p) * card (normalizer P)"
using act.orbit_stabilizer_card[OF P fin] orbit_S stab_normalizer by simp
show "card (Sylow_subgroups p) dvd card G"
using dvd_def orbit_stab by blast
have P_act_map:
"φ_Sylow p g ∈ Monoid.Units
(Sylow_subgroups p →⇩E Sylow_subgroups p)
(compose (Sylow_subgroups p)) (identity (Sylow_subgroups p))"
if "g ∈ P" for g
using that by blast
interpret P_act: Group_Action P "(⋅)" 𝟭 "φ_Sylow p" "Sylow_subgroups p"
proof qed (use act.hom_unit act.hom_compose P_act_map in auto)
have fixed_P: "P ∈ P_act.fixed_points"
by (simp add: Group.conjugate_subgroup_self Group_axioms P P_act.fixed_point_char
Psub.Subgroup_axioms φ_Sylow_def fin)
have "Q = P" if Qfixed: "Q ∈ P_act.fixed_points" for Q
proof -
have Qmem: "Q ∈ Sylow_subgroups p"
using subsetD[OF P_act.fixed_points_subset Qfixed] .
have normQ: "∀g ∈ P. conjugate_subgroup g Q = Q"
using P_act.fixed_point_char Qfixed Qmem φ_Sylow_def by auto
show ?thesis
by (rule normalizes_Sylow_subgroups_eq[OF prime fin P Qmem normQ])
qed
then have "P_act.fixed_points = {P}"
using fixed_P by auto
moreover have "p dvd card (Sylow_subgroups p - P_act.fixed_points)"
proof (rule P_act.dvd_card_nonfixed_points[OF fin_S])
fix Q
assume Q: "Q ∈ Sylow_subgroups p" and Qnot: "Q ∉ P_act.fixed_points"
have orbit_ne: "P_act.orbit Q ≠ {Q}"
using P_act.fixed_point_iff_orbit_singleton Q Qnot by presburger
have orbit_card_ne: "card (P_act.orbit Q) ≠ 1"
using P_act.orbit_self[OF Q] orbit_ne by (metis card_1_singletonE emptyE insert_iff)
have orbit_dvd: "card (P_act.orbit Q) dvd p ^ multiplicity p (card G)"
using P_act.orbit_stabilizer_card Q Sylow_subgroups_card[OF P] by force
show "p dvd card (P_act.orbit Q)"
using orbit_card_ne orbit_dvd prime prime_power_dvd_not_prime_dvd by blast
qed
ultimately show "p dvd card (Sylow_subgroups p) - 1"
using P by auto
qed
end
end