English
There is a canonical isomorphism between ((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f and ε I.homFamily .app (((iterationFunctor I κ).obj j).obj f).
Русский
Существует каноническое изоморфизм между ((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f и ε I.homFamily .app(((iterationFunctor I κ).obj j).obj f).
LaTeX
$$$((\\text{iterationFunctor} \\, I \\, \\kappa).map (\\text{homOfLE}(\\text{Order.le\_succ } j))).app f \\cong (\\epsilon I.homFamily).app(((\\text{iterationFunctor} \\, I \\, \\kappa).\\mathrm{obj} j).\\mathrm{obj} f)$$$
Lean4
/-- For any `f : Arrow C` and `j : κ.ord.toType`, the morphism
`((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f` identifies
to a morphism given by `SmallObject.ε I.homFamily`. -/
noncomputable def iterationFunctorMapSuccAppArrowIso (f : Arrow C) (j : κ.ord.toType) :
letI := hasColimitsOfShape_discrete I κ
letI := hasPushouts I κ
Arrow.mk (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f) ≅
(ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f) :=
have := hasIterationOfShape I κ
have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
Arrow.isoMk (Iso.refl _)
(((evaluation _ _).obj f).mapIso ((succStruct I κ).iterationFunctorObjSuccIso j (not_isMax j)))
(by
have this := NatTrans.congr_app ((succStruct I κ).iterationFunctor_map_succ j (not_isMax j)) f
dsimp at this
dsimp [iterationFunctor]
rw [id_comp, this, assoc, Iso.inv_hom_id_app, comp_id]
dsimp [succStruct])
