hasColimitsOfShape_discrete — Mathlib

English

For any X, Y and morphism p: X → Y, the shape given by a discrete index of the I.homFamily construction admits colimits in C.

Русский

Для любых X, Y и морфизма p: X → Y форма дискретного индекса для I.homFamily допускает колимиты в C.

LaTeX

$$$\\mathrm{HasColimitsOfShape}\\; (\\mathrm{Discrete}(\\mathrm{FunctorObjIndex}\\ I.homFamily\\ p))\\; C$$$

Lean4

theorem hasColimitsOfShape_discrete (X Y : C) (p : X ⟶ Y) :
    HasColimitsOfShape (Discrete (FunctorObjIndex I.homFamily p)) C :=
  by
  haveI := locallySmall I κ
  haveI := isSmall I κ
  haveI := hasCoproducts I κ
  exact hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{w} _)).symm

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