hom_ext — Mathlib

English

If h is an IsUniversal, then two parallel morphisms out of f are equal whenever their left components agree.

Русский

Если h — IsUniversal, то параллельные морфизмы из f совпадают, когда их левые компоненты совпадают.

LaTeX

$$$\\forall f,g:\\, f.left = g.left \\Rightarrow f = g$$$

Lean4

/-- Two morphisms out of a universal `T`-structured arrow are equal if their image under `T` are
equal after precomposing the universal arrow. -/
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : f.right ⟶ c} (w : f.hom ≫ T.map η = f.hom ≫ T.map η') : η = η' := by
  rw [h.hom_desc η, h.hom_desc η', w]

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