strict_hom_ext — Mathlib

English

Let I be a strict initial object in a category C. Then for every object A, there is a unique morphism from A to I; equivalently, any two morphisms A → I are equal.

Русский

Пусть I — строгий начальний объект в категории C. Тогда для каждого объекта A существует единственный морфизм A → I; иначе говоря, любые два морфизма A → I совпадают.

LaTeX

$$$\\forall A,\\ \\exists! f: A \\to I$$$

Lean4

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

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