eq_lift_comp_mkRingHom — Mathlib

English

For any f and w as above, f equals Lift ⟨f ∘ mkRingHom r, w⟩, i.e., every quotient hom factors uniquely through Lift.

Русский

Для любого f и w выше, f равно Lift ⟨f ∘ mkRingHom r, w⟩, то есть каждая гомоморфизм-квота уникально факторизуется через Lift.

LaTeX

$$$f = \\mathrm{lift}(\\langle f \\circ mkRingHom r, w \\rangle)$$$

Lean4

theorem eq_lift_comp_mkRingHom {r : R → R → Prop} (f : RingQuot r →+* T) :
    f = lift ⟨f.comp (mkRingHom r), fun _ _ h ↦ congr_arg f (mkRingHom_rel h)⟩ :=
  lift_unique (f.comp (mkRingHom r)) (fun _ _ h ↦ congr_arg (⇑f) (mkRingHom_rel h)) f rfl

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