kerLift — Mathlib

English

If there exists a right inverse g of a ring hom f: R →+* S, then R/ker f ≃+* S.

Русский

Если существует правый обратный g к кольцу-гомоморфизму f: R →+* S, тогда R/ker f эквивариантно S.

LaTeX

$$$$R/\ker f \cong+* S \quad\text{if } \exists g: S \to R\text{ with } f\circ g = \mathrm{id}_S.$$$$

Lean4

/-- The induced map from the quotient by the kernel to the codomain.

This is an isomorphism if `f` has a right inverse (`quotientKerEquivOfRightInverse`) /
is surjective (`quotientKerEquivOfSurjective`).
-/
def kerLift : R ⧸ ker f →+* S :=
  Ideal.Quotient.lift _ f fun _ => mem_ker.mp

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