English
Let G be a group, N a normal subgroup of G, and M a group. If φ: G →* M is a group homomorphism with N contained in ker φ, then φ factors through the quotient G/N; i.e., there exists a unique group homomorphism φ̂: G/N →* M such that φ̂ ∘ π = φ, where π: G → G/N is the canonical quotient map.
Русский
Пусть G группа, N нормальная подгруппа G, M группа. Если φ: G →* M — гомоморфизм группы и N ⊆ ker φ, то φ факторизуется через фактор-группу G/N; то есть существует единственный гомоморфизм φ̂: G/N →* M такой, что φ̂ ∘ π = φ, где π: G → G/N — естественный отображение на фактор-группу.
LaTeX
$$$N \\le \\ker \\varphi \\;\\Longrightarrow\\; \\exists! \\hat{\\varphi} : G/N \\to^* M \\,\\big(\\hat{\\varphi} \\circ \\pi = \\varphi\\big).$$$
Lean4
/-- A group homomorphism `φ : G →* M` with `N ⊆ ker(φ)` descends (i.e. `lift`s) to a
group homomorphism `G/N →* M`. -/
@[to_additive /-- An `AddGroup` homomorphism `φ : G →+ M` with `N ⊆ ker(φ)` descends (i.e. `lift`s)
to a group homomorphism `G/N →* M`. -/
]
def lift (φ : G →* M) (HN : N ≤ φ.ker) : Q →* M :=
(QuotientGroup.con N).lift φ <| con_ker_eq_conKer φ ▸ con_mono HN
