English
For a finite group G with a cyclic Sylow p-subgroup P, if K is a subgroup of G, then either [K,P] = ⊥ or [K,P] = P.
Русский
Для конечной группы G с циклической сигмой p, если K ≤ N_G(P), то [K,P] = ⊥ или [K,P] = P.
LaTeX
$$$[K,P] = \\{e\\} \\lor [K,P] = P$$$
Lean4
/-- A cyclic Sylow subgroup is either central in its normalizer or contained in the commutator
subgroup. -/
theorem normalizer_le_centralizer_or_le_commutator : P.normalizer ≤ Subgroup.centralizer P ∨ P ≤ commutator G :=
by
let Q : Sylow p P.normalizer := P.subtype P.le_normalizer
have : Q.Normal := P.normal_in_normalizer
have : IsCyclic Q := isCyclic_of_surjective _ (Subgroup.subgroupOfEquivOfLe P.le_normalizer).symm.surjective
refine (le_center_or_le_commutator Q).imp (fun h ↦ ?_) (fun h ↦ ?_)
· rw [← SetLike.coe_subset_coe, ← Subgroup.centralizer_eq_top_iff_subset, eq_top_iff, ←
Subgroup.map_subtype_le_map_subtype, ← MonoidHom.range_eq_map, P.normalizer.range_subtype] at h
replace h := h.trans (Subgroup.map_centralizer_le_centralizer_image _ _)
rwa [← Subgroup.coe_map, P.coe_subtype, Subgroup.map_subgroupOf_eq_of_le P.le_normalizer] at h
· rw [P.coe_subtype, ← Subgroup.map_subtype_le_map_subtype, Subgroup.map_subgroupOf_eq_of_le P.le_normalizer,
Subgroup.map_subtype_commutator] at h
exact h.trans (Subgroup.commutator_mono le_top le_top)
