hom_ext — Mathlib

English

Two morphisms into a universal arrow are equal if their postcomposition with f.hom agree after applying S.

Русский

Два морфизмa в универсальную стрелу равны, если их композиции через f.hom с равными образами после применения S совпадают.

LaTeX

$$$ \forall h : \text{IsUniversal } f, \forall c, \forall \eta, \eta' : c \to f.left,\; S.map \eta ≫ f.hom = S.map \eta' ≫ f.hom \Rightarrow \eta = \eta'. $$$

Lean4

/-- Two morphisms into a universal `S`-costructured arrow are equal if their image under `S` are
equal after postcomposing the universal arrow. -/
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : c ⟶ f.left} (w : S.map η ≫ f.hom = S.map η' ≫ f.hom) : η = η' := by
  rw [h.hom_desc η, h.hom_desc η', w]

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