English
The natural isomorphism between the left-hand construction ιFunctorObj and the right-hand SmallObject construction holds at level j, via the map induced by the iteration functor and its succ app arrow iso.
Русский
Сохранено естественное изоморфизмное соответствие между двумя конструированными слева и справа объектами, связанное с итератором и сопряжённым отображением.
LaTeX
$$$ιFunctorObj\ I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom \cong (relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)) \circ (relativeCellComplexιObjFObjSuccIso I κ f j).hom$$
Lean4
theorem ιFunctorObj_eq (j : κ.ord.toType) :
letI := hasColimitsOfShape_discrete I κ
letI := hasPushouts I κ
ιFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
(relativeCellComplexιObj I κ f).F.map (homOfLE (Order.le_succ j)) ≫
(relativeCellComplexιObjFObjSuccIso I κ f j).hom :=
by simpa using Arrow.leftFunc.congr_map (iterationFunctorMapSuccAppArrowIso I κ f j).hom.w
