hom_ext — Mathlib

English

If c is a limit for F : β → C, and f,g : A ⟶ c.pt are two morphisms that become equal after composing with every projection c.proj i, then f = g.

Русский

Пусть c есть предел диаграммы F: β → C. Если две стрелки f,g: A → c(pt) совпадают после композиции с каждой проекцией c.proj_i, то они равны.

LaTeX

$$$\\forall i, f \\circ c.proj_i = g \\circ c.proj_i \\Rightarrow f = g$$$

Lean4

theorem hom_ext {I : Type*} {F : I → C} {c : Fan F} (hc : IsLimit c) {A : C} (f g : A ⟶ c.pt)
    (h : ∀ i, f ≫ c.proj i = g ≫ c.proj i) : f = g :=
  hc.hom_ext (fun ⟨i⟩ => h i)

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