English
Burnside's normal p-complement theorem: If N_G(P) ≤ C_G(P) for a Sylow p-subgroup P of a finite group G, then the kernel of the transferSylow map is a normal p-complement of G.
Русский
Теорема Бёрндайна о нормальном p-комплекте: если N_G(P) ≤ C_G(P) для Sylow-p-подгруппы P конечной группы G, тогда ядро переноса Sylow образует нормальный p-комплект группы.
LaTeX
$$IsComplement' (transferSylow P hP).ker P$$
Lean4
/-- **Burnside's normal p-complement theorem**: If `N(P) ≤ C(P)`, then `P` has a normal
complement. -/
theorem ker_transferSylow_isComplement' : IsComplement' (transferSylow P hP).ker P :=
by
have hf : Function.Bijective ((transferSylow P hP).restrict (P : Subgroup G)) :=
(transferSylow_restrict_eq_pow P hP).symm ▸ (P.2.powEquiv' P.not_dvd_index).bijective
rw [Function.Bijective, ← range_eq_top, restrict_range] at hf
have := range_eq_top.mp (top_le_iff.mp (hf.2.ge.trans (map_le_range (transferSylow P hP) P)))
rw [← (comap_injective this).eq_iff, comap_top, comap_map_eq, sup_comm, SetLike.ext'_iff, normal_mul, ←
ker_eq_bot_iff, ← (map_injective (P : Subgroup G).subtype_injective).eq_iff, ker_restrict, subgroupOf_map_subtype,
Subgroup.map_bot, coe_top] at hf
exact isComplement'_of_disjoint_and_mul_eq_univ (disjoint_iff.2 hf.1) hf.2
