English
In the π-construct, the functor πFunctorObj equals the composition of the inverse of relativeCellComplexιObjFObjSuccIso with the inclusion map and the πObj, up to the inverse of the iteration right iso.
Русский
Для операции πFunctorObj выполняется равенство, связанное с инклузией и обратной стороной итератора, аналогично формуле для πObj.
LaTeX
$$$πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom = (relativeCellComplexιObjFObjSuccIso I κ f j).inv \circ (relativeCellComplexιObj I κ f).incl.app (Order.succ j) \circ πObj I κ f \circ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv$$
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ιObjFObjSuccIso I κ f j).inv ≫
(relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv :=
by
have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.w
have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality (homOfLE (Order.le_succ j))
dsimp at h₁ h₂
rw [comp_id] at h₂
rw [← cancel_mono (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom, ←
cancel_mono ((ιIteration I κ).app f).right, assoc, assoc, assoc, assoc, assoc, Iso.inv_hom_id_assoc,
πObj_ιIteration_app_right, iterationFunctorObjObjRightIso_ιIteration_app_right, ←
cancel_epi (relativeCellComplexιObjFObjSuccIso I κ f j).hom, Iso.hom_inv_id_assoc]
dsimp [relativeCellComplexιObjFObjSuccIso, relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]
simp only [reassoc_of% h₁, comp_id, comp_id, Arrow.w_mk_right, ← h₂, NatTrans.comp_app, Arrow.comp_right,
iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc]
