comapOfInjective — Mathlib

English

The preimage of a Sylow p-subgroup along an injective homomorphism is again a Sylow p-subgroup.

Русский

Предобраз подпогруппы Силова p по инъективному гомоморфизму снова является подпогруппой Силова p.

LaTeX

$$$ (h\\varphi : Function.Injective \\varphi) \\Rightarrow \\exists Q: Sylow p K, Q.toSubgroup = P.toSubgroup .comap \\varphi $$$

Lean4

/-- The preimage of a Sylow subgroup under an injective homomorphism is a Sylow subgroup. -/
def comapOfInjective (hϕ : Function.Injective ϕ) (h : P ≤ ϕ.range) : Sylow p K :=
  P.comapOfKerIsPGroup ϕ (IsPGroup.ker_isPGroup_of_injective hϕ) h

Похожие утверждения