English
Let G be a finite group. The following conditions are equivalent: G is nilpotent; G satisfies the normalizer condition; every maximal subgroup of G is normal; every Sylow subgroup of G is normal; G is the direct product of its Sylow subgroups.
Русский
Пусть G — конечная группа. Следующие условия эквивалентны: G нильпотентна; G удовлетворяет условию нормализатора; каждая максимальная подгруппа нормальна; каждая подгруппа Сильова нормальна; G является прямым произведением своих подгрупп Сильова.
LaTeX
$$$\\mathrm{IsNilpotent}(G) \\iff \\mathrm{NormalizerCondition}(G) \\iff \\Big( \\forall H \\le G,\\; \\mathrm{IsCoatom}(H) \\rightarrow H \\lhd G \\Big) \\\\ \\iff \\Big( \\forall p \\text{ prime}, \\; \\forall P \\in \\mathrm{Sylow}_p(G), \\; P \\lhd G \\Big) \\\\ \\iff \\; G \\cong \\prod_{p \\text{ prime}} P_p$ where each $P_p$ is a Sylow subgroup of $G$ and hence $G$ is the direct product of its Sylow subgroups.$$
Lean4
/-- A finite group is nilpotent iff the normalizer condition holds, and iff all maximal groups are
normal and iff all Sylow groups are normal and iff the group is the direct product of its Sylow
groups. -/
theorem isNilpotent_of_finite_tfae :
List.TFAE
[IsNilpotent G, NormalizerCondition G, ∀ H : Subgroup G, IsCoatom H → H.Normal,
∀ (p : ℕ) (_hp : Fact p.Prime) (P : Sylow p G), (↑P : Subgroup G).Normal,
Nonempty ((∀ p : (Nat.card G).primeFactors, ∀ P : Sylow p G, (↑P : Subgroup G)) ≃* G)] :=
by
tfae_have 1 → 2 := @normalizerCondition_of_isNilpotent _ _
tfae_have 2 → 3
| h, H => NormalizerCondition.normal_of_coatom H h
tfae_have 3 → 4
| h, p, _, P => Sylow.normal_of_all_max_subgroups_normal h _
tfae_have 4 → 5
| h => Nonempty.intro (Sylow.directProductOfNormal fun {p hp hP} => h p hp hP)
tfae_have 5 → 1
| ⟨e⟩ => isNilpotent_of_product_of_sylow_group e
tfae_finish
