English
If every Sylow p-subgroup of a finite group G is normal, then G is isomorphic to the direct product of these Sylow subgroups indexed by the prime divisors of |G|.
Русский
Пусть все подгруппы Sylow нормальны; тогда G изоморфна прямому произведению этих подгрупп, индексируемому простыми делителями |G|.
LaTeX
$$$[Finite\ G]\ (\forall {p} [Fact (Nat.Prime p)] (P:\ Sylow p G), P.Normal)\Rightarrow \\exists φ: (∀ p, Sylow p G) \to G, φ\text{ является isomorphism onto } G$$
Lean4
/-- If all its Sylow subgroups are normal, then a finite group is isomorphic to the direct product
of these Sylow subgroups.
-/
noncomputable def directProductOfNormal [Finite G] (hn : ∀ {p : ℕ} [Fact p.Prime] (P : Sylow p G), P.Normal) :
(∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, P) ≃* G :=
by
have := Fintype.ofFinite G
set ps := (Nat.card G).primeFactors
let P : ∀ p, Sylow p G := default
have : ∀ p, Fintype (P p) := fun p ↦ Fintype.ofFinite (P p)
have hcomm : Pairwise fun p₁ p₂ : ps => ∀ x y : G, x ∈ P p₁ → y ∈ P p₂ → Commute x y :=
by
rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
have hne' : p₁ ≠ p₂ := by simpa using hne
apply Subgroup.commute_of_normal_of_disjoint _ _ (hn (P p₁)) (hn (P p₂))
apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
refine
MulEquiv.trans (N := ∀ p : ps, P p) ?_
?_
-- There is only one Sylow subgroup for each p, so the inner product is trivial
· -- here we need to help the elaborator with an explicit instantiation
apply @MulEquiv.piCongrRight ps (fun p => ∀ P : Sylow p G, P) (fun p => P p) _ _
rintro ⟨p, hp⟩
haveI hp' := Fact.mk (Nat.prime_of_mem_primeFactors hp)
letI := unique_of_normal _ (hn (P p))
apply MulEquiv.piUnique
apply MulEquiv.ofBijective (Subgroup.noncommPiCoprod hcomm)
apply (Fintype.bijective_iff_injective_and_card _).mpr
constructor
· apply Subgroup.injective_noncommPiCoprod_of_iSupIndep
apply independent_of_coprime_order hcomm
rintro ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩ hne
haveI hp₁' := Fact.mk (Nat.prime_of_mem_primeFactors hp₁)
haveI hp₂' := Fact.mk (Nat.prime_of_mem_primeFactors hp₂)
have hne' : p₁ ≠ p₂ := by simpa using hne
simp only [← Nat.card_eq_fintype_card]
apply IsPGroup.coprime_card_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'
· simp only [← Nat.card_eq_fintype_card]
calc
Nat.card (∀ p : ps, P p) = ∏ p : ps, Nat.card (P p) := Nat.card_pi
_ = ∏ p : ps, p.1 ^ (Nat.card G).factorization p.1 :=
by
congr 1 with ⟨p, hp⟩
exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
_ = ∏ p ∈ ps, p ^ (Nat.card G).factorization p :=
(Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)
_ = (Nat.card G).factorization.prod (· ^ ·) := rfl
_ = Nat.card G := Nat.factorization_prod_pow_eq_self Nat.card_pos.ne'
