English
There is a natural bijection between Sylow_p(G) and the quotient G / N_G(P) given by sending Q to g with Q = g P g^{-1}.
Русский
Существуют естественные биекции между Sylow_p(G) и фактор-группой G / N_G(P); Q ↦ g с Q = g P g^{-1}.
LaTeX
$$$\\mathrm{Sylow}_p(G) \\simeq G / N_G(P).$$$
Lean4
/-- Sylow `p`-subgroups are in bijection with cosets of the normalizer of a Sylow `p`-subgroup -/
noncomputable def equivQuotientNormalizer [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) :
Sylow p G ≃ G ⧸ P.normalizer :=
calc
Sylow p G ≃ (⊤ : Set (Sylow p G)) := (Equiv.Set.univ (Sylow p G)).symm
_ ≃ orbit G P := (Equiv.setCongr P.orbit_eq_top.symm)
_ ≃ G ⧸ stabilizer G P := (orbitEquivQuotientStabilizer G P)
_ ≃ G ⧸ P.normalizer := by rw [P.stabilizer_eq_normalizer]
