English
The inverse of the pullback-shift addition functor decomposes via the appropriate pullback-shift isomorphisms and the base shift inverse.
Русский
Обратный компонент сложения черезpullbackShift распадается через соответствующие изоморфизмы pullbackShift и обратный компонент базового сдвига.
LaTeX
$$$ (shiftFunctorAdd' \; (PullbackShift C \; \varphi) \; a_1 \ a_2 \ a_3 \ h).inv.app X = (shiftFunctor (PullbackShift C \varphi) a_2).map ( (pullbackShiftIso C \varphi a_1 b_1 h_1).hom.app X) \\; ∘ (pullbackShiftIso C \varphi a_2 b_2 h_2).hom.app _ \\; ∘ (shiftFunctorAdd' C b_1 b_2 b_3 (by rw[ h_1, h_2, h_3, \ left, \ φ.map_add ] )).inv.app X \\; ∘ (pullbackShiftIso C \varphi a_3 b_3 h_3).inv.app X $$$
Lean4
theorem pullbackShiftFunctorAdd'_inv_app :
(shiftFunctorAdd' _ a₁ a₂ a₃ h).inv.app X =
(shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X) ≫
(pullbackShiftIso C φ a₂ b₂ h₂).hom.app _ ≫
(shiftFunctorAdd' C b₁ b₂ b₃ (by rw [h₁, h₂, h₃, ← h, φ.map_add])).inv.app X ≫
(pullbackShiftIso C φ a₃ b₃ h₃).inv.app X :=
by
subst h₁ h₂ h
obtain rfl : b₃ = φ a₁ + φ a₂ := by rw [h₃, φ.map_add]
simp only [Functor.comp_obj, NatTrans.naturality_assoc]
erw [Functor.map_id, id_comp, id_comp, shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq_shiftFunctorAdd]
change _ ≫ _ = _
congr 1
rw [Discrete.addMonoidalFunctor_μ]
dsimp [Discrete.eqToHom]
congr 2
apply eqToHom_map
