iteration — Mathlib

English

For X, Y in C and p: X→Y the shape obtained from the discrete index of FunctorObjIndex I.homFamily p has colimits in C.

Русский

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

LaTeX

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

Lean4

/-- Given `Φ : SuccStruct C` and a well-ordered type `J`,
this is an object of `C` which is the iteration of `Φ` to the power `J`:
it is defined as the colimit of the functor `Φ.iterationFunctor J : J ⥤ C`. -/
noncomputable def iteration : C :=
  colimit (Φ.iterationFunctor J)

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