strict_hom_ext — Mathlib

English

In a category with strict terminal objects, any two morphisms f,g: I ⟶ A from the terminal object I to A are equal.

Русский

В категории со строгими терминальными объектами любые два морфизма I → A равны.

LaTeX

$$$\\forall A, f,g: I \\to A, f=g$$$

Lean4

theorem strict_hom_ext (hI : IsTerminal I) {A : C} (f g : I ⟶ A) : f = g :=
  by
  haveI := hI.isIso_from f
  haveI := hI.isIso_from g
  exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

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