English
Analogous to the inverse case, the forward (hom) component of the pullback-shift addition functor factors through the relevant isomorphisms and base shift morphisms.
Русский
Аналогично обратному случаю, прямой компонент гом через pullbackShiftAdd' факторизуется через соответствующие изоморфизмы и базовые морфизмы сдвига.
LaTeX
$$$ (shiftFunctorAdd' \; (PullbackShift C φ) \; a_1 a_2 a_3 h).hom.app X = (pullbackShiftIso C φ a_3 b_3 h_3).hom.app X \\; ∘ (shiftFunctorAdd' C b_1 b_2 b_3 (by rw[ h_1, h_2, h_3, ← h, φ.map_add])).hom.app X \\; ∘ (pullbackShiftIso C φ a_2 b_2 h_2).inv.app _ \\; ∘ (shiftFunctor (PullbackShift C φ) a_2).map ((pullbackShiftIso C φ a_1 b_1 h_1).inv.app X) $$$
Lean4
theorem pullbackShiftFunctorAdd'_hom_app :
(shiftFunctorAdd' _ a₁ a₂ a₃ h).hom.app X =
(pullbackShiftIso C φ a₃ b₃ h₃).hom.app X ≫
(shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).hom.app X ≫
(pullbackShiftIso C φ a₂ b₂ h₂).inv.app _ ≫
(shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X) :=
by
rw [← cancel_epi ((shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X), Iso.inv_hom_id_app,
pullbackShiftFunctorAdd'_inv_app φ X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc, Iso.inv_hom_id_app_assoc,
Iso.inv_hom_id_app_assoc, Iso.hom_inv_id_app_assoc, ← Functor.map_comp, Iso.hom_inv_id_app, Functor.map_id]
rfl
