to_product_injective_of_isLimit — Mathlib

English

For a diagram F with a colimit D in a concrete category, equality of colimit projections implies equality of elements.

Русский

Для диаграммы F с колимитом D в конкретной категории равенство проекций колимита в точке означает равенство самих точек.

LaTeX

$$$\\forall F:\\, J\\to C,\\; [HasColimit\ F] \\Rightarrow \\forall x,y:\\, ToType(\\mathrm{colimit}\ F),\\; (\\forall j:\\, J,\\; \\mathrm{colimit}.\\iota_{F,j}(x)=\\mathrm{colimit}.\\iota_{F,j}(y))\\Rightarrow x=y$$$

Lean4

theorem to_product_injective_of_isLimit {D : Cone F} (hD : IsLimit D) :
    Function.Injective fun (x : ToType D.pt) (j : J) => D.π.app j x :=
  by
  let E := (forget C).mapCone D
  intro (x : E.pt) y H
  apply (Types.isLimitEquivSections (isLimitOfPreserves _ hD)).injective
  ext j
  exact funext_iff.mp H j

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