English
The preimage of a Sylow p-subgroup under a p-group-kernel homomorphism is again a Sylow p-subgroup; the construction ensures the required maximal property and subgroup containment.
Русский
Предобраз подпогруппы Силова p-подгруппы под гомоморфизмом с p-групким ядром вновь является подпогруппой Силова p; конструкция сохраняет максимальность и включение подгрупп.
LaTeX
$$$ (h\\varphi : IsPGroup p (\\varphi.\\ker)) \\land (h : P \\leq \\varphi.range) \\Rightarrow \\exists Q: Sylow p K, Q.toSubgroup = P.1.comap \\varphi $$$
Lean4
/-- The preimage of a Sylow subgroup under a p-group-kernel homomorphism is a Sylow subgroup. -/
def comapOfKerIsPGroup (hϕ : IsPGroup p ϕ.ker) (h : P ≤ ϕ.range) : Sylow p K :=
{ P.1.comap ϕ with
isPGroup' := P.2.comap_of_ker_isPGroup ϕ hϕ
is_maximal' := fun {Q} hQ hle => by
show Q = P.1.comap ϕ
rw [← P.3 (hQ.map ϕ) (le_trans (ge_of_eq (map_comap_eq_self h)) (map_mono hle))]
exact (comap_map_eq_self ((P.1.ker_le_comap ϕ).trans hle)).symm }
