iterationFunctor — Mathlib

English

The iteration cocone is isomorphic to the colimit cocone of the iteration functor, i.e., iteration J identifies with the colimit of iterationFunctor J.

Русский

Кокон итерации идентичен колимитному кокону итерационного функторa: итерация J эквивалентна колимиту iterationFunctor J.

LaTeX

$$$$ \text{IsColimit}(\text{iterationCocone}(J)) $$$$

Lean4

/-- Given `Φ : SuccStruct C` and a well-ordered type `J`, this
is the functor `J ⥤ C` which gives the iterations of `Φ` indexed by `J`. -/
noncomputable def iterationFunctor : J ⥤ C
    where
  obj j := (Φ.iter j).F.obj ⟨j, by simp⟩
  map f := Iteration.mapObj _ _ (leOfHom f) _ _ (leOfHom f)

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