English
For a fixed prime p, the mapSylowSurjective is surjective, i.e., every Sylow p-subgroup of G' is the image of some Sylow p-subgroup of G under a surjective homomorphism.
Русский
Для фиксированного p отображение Sylow mapSurjective сюръективно: каждая Sylow p-подгруппа G' является образом некоторой Sylow p-подгруппы G.
LaTeX
$$Function.Surjective (Sylow.mapSurjective hf)$$
Lean4
theorem mapSurjective_surjective (p : ℕ) [Fact p.Prime] :
Function.Surjective (Sylow.mapSurjective hf : Sylow p G → Sylow p G') :=
by
have : Finite G' := Finite.of_surjective f hf
intro P
let Q₀ : Sylow p (P.comap f) := Sylow.nonempty.some
let Q : Subgroup G := Q₀.map (P.comap f).subtype
have hPQ : Q.map f ≤ P := Subgroup.map_le_iff_le_comap.mpr (Subgroup.map_subtype_le Q₀.1)
have hpQ : IsPGroup p Q := Q₀.2.map (P.comap f).subtype
have hQ : ¬p ∣ Q.index :=
by
rw [Subgroup.index_map_subtype Q₀.1, P.index_comap_of_surjective hf]
exact Nat.Prime.not_dvd_mul Fact.out Q₀.not_dvd_index P.not_dvd_index
use hpQ.toSylow hQ
rw [Sylow.ext_iff, Sylow.coe_mapSurjective, eq_comm]
exact ((hpQ.map f).toSylow (fun h ↦ hQ (h.trans (Q.index_map_dvd hf)))).3 P.2 hPQ
