isColimitCofanMapObj — Mathlib

English

For a fixed j and X, with a given HasMap p, the cofan X.cofanMapObj p j is the coproduct of the family of objects X i with p i = j; it satisfies the colimit property.

Русский

Для заданного j и X, имеющего HasMap p, когран X.cofanMapObj p j является копрокон-образом семейства объектов X_i с p i = j и обладает свойством кколимита.

LaTeX

$$$ IsColimit (X.cofanMapObj p j) $$$

Lean4

/-- Given `X : GradedObject I C`, `p : I → J` and `j : J`, `X.mapObj p j` satisfies
the universal property of the coproduct of those `X i` such that `p i = j`. -/
noncomputable def isColimitCofanMapObj (j : J) : IsColimit (X.cofanMapObj p j) :=
  colimit.isColimit _

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