hom_ext — Mathlib

English

If K is a limit for a multifork, then two arrows f,g into K.pt that agree after composing with every leg map K.ι a are equal; i.e., the morphisms into the limit are determined by their composites with the legs.

Русский

Если K является пределом мультфорка, то любые две стрелки f,g: T → K.pt, которые совпадают после композиции с каждым отображением K.ι a, на самом деле совпадают: f = g.

LaTeX

$$$\text{If } h_K:\ IsLimit\ K,\ f,g:\, T \to K.pt,\ \forall a,\; f \circ K.\ι a = g \circ K.\ι a \Rightarrow f = g$$$

Lean4

theorem hom_ext (hK : IsLimit K) {T : C} {f g : T ⟶ K.pt} (h : ∀ a, f ≫ K.ι a = g ≫ K.ι a) : f = g :=
  by
  apply hK.hom_ext
  rintro (_ | b)
  · apply h
  · dsimp
    rw [app_right_eq_ι_comp_fst, reassoc_of% h]

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