hom_ext — Mathlib

English

If two arrows f, f' from the colimit to X agree after precomposition with all colimit projections, then f = f'.

Русский

Если для всех j отображения colimit.ι F j ≫ f совпадают c соответствующими, то f = f'.

LaTeX

$$$\\forall f,f' : \\operatorname{colimit} F \\to X,\\; (\\forall j, \\iota_F j \\;\\gg\\; f = \\iota_F j \\;\\gg\\; f') \\Rightarrow f = f'$$$

Lean4

@[ext]
theorem hom_ext {F : J ⥤ C} [HasColimit F] {X : C} {f f' : colimit F ⟶ X}
    (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f' :=
  (colimit.isColimit F).hom_ext w

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