English
The transfinite composition of shape ιObj attached to f yields a well-defined transfinite composition in the coproduct-pushout setting.
Русский
Трансфинитная композиция формы ιObj, применённая к f, образует корректную трансфинитную композицию в конфигурации coproduct-pushout.
LaTeX
$$$\\text{transfiniteCompositionsOfShape}(I,\\kappa).(\\iotaObj I κ f)$$$
Lean4
@[reassoc (attr := simp)]
theorem iterationFunctorMapSuccAppArrowIso_hom_right_right_comp (f : Arrow C) (j : κ.ord.toType) :
(iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.right ≫
(((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right =
𝟙 _ :=
by
have := Arrow.rightFunc.congr_map ((iterationFunctorMapSuccAppArrowIso I κ f j).hom.w)
dsimp at this ⊢
rw [← cancel_epi (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f).right, ← reassoc_of% this, comp_id]
