eq_liftOfRightInverse — Mathlib

English

If h: B → C is another ring hom with h ∘ f = g and ker containment, then h equals the liftOfRightInverse computed from f, f_inv, g.

Русский

Если существует другой гомоморфизм h: B → C с h ∘ f = g и условием ker, то h совпадает с искомым liftOfRightInverse.

LaTeX

$$$$ h = f.liftOfRightInverse f_{inv} hf ⟨g, hg⟩. $$$$

Lean4

theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : A →+* C) (hg : RingHom.ker f ≤ RingHom.ker g)
    (h : B →+* C) (hh : h.comp f = g) : h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩ :=
  by
  simp_rw [← hh]
  exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

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