English
When interpreting ιObj I κ f as a relative I-cell complex, the j-th step is obtained by applying SmallObject.functorObj to the corresponding iteration step, yielding an isomorphism to the object produced by the functor application.
Русский
При интерпретации ιObj I κ f как относительного I‑клеточного комплекса, на j‑м шаге получаем тождество с объектом, полученным применением functorObj к соответствующему шагу итерации.
LaTeX
$$$ (relativeCellComplexιObj I κ f).F.obj (Order.succ j) \cong \text{functorObj } I.homFamily ((iterationFunctor I κ).obj j).obj (Arrow.mk f).hom$$
Lean4
/-- When `ιObj I κ f` is considered as a relative `I`-cell complex,
the object at the `j`th step is obtained by applying the construction
`SmallObject.functorObj`. -/
noncomputable def relativeCellComplexιObjFObjSuccIso (j : κ.ord.toType) :
letI := hasColimitsOfShape_discrete I κ
letI := hasPushouts I κ
(relativeCellComplexιObj I κ f).F.obj (Order.succ j) ≅
functorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom :=
(Arrow.rightFunc ⋙ Arrow.leftFunc).mapIso (iterationFunctorMapSuccAppArrowIso I κ f j)
