quotientKerEquivOfRightInverse — Mathlib

English

If there exists a right inverse g for f, then R/ker f ≃+* S.

Русский

Если существует правый обратный г для f, тогда R/ker f ≃+* S.

LaTeX

$$$$R/\ker f \cong+* S$$$$

Lean4

/-- The **first isomorphism theorem for commutative rings**, computable version. -/
def quotientKerEquivOfRightInverse {g : S → R} (hf : Function.RightInverse g f) : R ⧸ ker f ≃+* S :=
  { kerLift f with
    toFun := kerLift f
    invFun := Ideal.Quotient.mk (ker f) ∘ g
    left_inv := by
      rintro ⟨x⟩
      apply kerLift_injective
      simp only [Submodule.Quotient.quot_mk_eq_mk, Ideal.Quotient.mk_eq_mk, kerLift_mk, Function.comp_apply, hf (f x)]
    right_inv := hf }

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