English
If N is a normal subgroup of G and P is a Sylow p-subgroup of N, then the normalizer of P in G together with N generates G, i.e., N_G(P)·N = G.
Русский
Если N нормальная в G и P — Sylow p-подгруппа N, тогда нормализатор P в G вместе с N порождает G: N_G(P)N = G.
LaTeX
$$N_G(P) ⊔ N = G$$
Lean4
/-- **Frattini's Argument**: If `N` is a normal subgroup of `G`, and if `P` is a Sylow `p`-subgroup
of `N`, then `N_G(P) ⊔ N = G`. -/
theorem normalizer_sup_eq_top {p : ℕ} [Fact p.Prime] {N : Subgroup G} [N.Normal] [Finite (Sylow p N)] (P : Sylow p N) :
(P.map N.subtype).normalizer ⊔ N = ⊤ :=
by
refine top_le_iff.mp fun g _ => ?_
obtain ⟨n, hn⟩ := exists_smul_eq N ((MulAut.conjNormal g : MulAut N) • P) P
rw [← inv_mul_cancel_left (↑n) g, sup_comm]
apply mul_mem_sup (N.inv_mem n.2)
rw [smul_def, ← mul_smul, ← MulAut.conjNormal_val, ← MulAut.conjNormal.map_mul, Sylow.ext_iff, pointwise_smul_def,
Subgroup.pointwise_smul_def] at hn
have : Function.Injective (MulAut.conj (n * g)).toMonoidHom := (MulAut.conj (n * g)).injective
refine fun x ↦ (mem_map_iff_mem this).symm.trans ?_
rw [map_map, ← congr_arg (map N.subtype) hn, map_map]
rfl
