English
Consider the op-category and the shifted functors with prime indices; the morphism component of shiftFunctorAdd' on Xᵒᵖ is equal to the composition of the corresponding shift iso morphisms and their inverses, expressed via the op-construction and the maps between shifts A, B, and the sum A+B.
Русский
Рассматривая оп-категорию и сдвиги с добавлением в прайм-индексах, компонент морфизма shiftFunctorAdd' на X^{op} равен по смыслу композиции соответствующих морфизмов из изоморфизмов сдвига и их обратных через конструкцию op.
LaTeX
$$$ (\\text{shiftFunctorAdd'} \; C^{op}\\; a_1\\; a_2\\; a_3\\; h).\\mathrm{hom}.\\mathrm{app} X = \\ldots $$$
Lean4
theorem shiftFunctorAdd'_op_hom_app (X : Cᵒᵖ) (a₁ a₂ a₃ : ℤ) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : ℤ) (h₁ : a₁ + b₁ = 0)
(h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0) :
(shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X =
(shiftFunctorOpIso C _ _ h₃).hom.app X ≫
((shiftFunctorAdd' C b₁ b₂ b₃ (by cutsat)).inv.app X.unop).op ≫
(shiftFunctorOpIso C _ _ h₂).inv.app _ ≫ (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C _ _ h₁).inv.app X) :=
by
erw [@pullbackShiftFunctorAdd'_hom_app (OppositeShift C ℤ) _ _ _ _ _ _ _ X a₁ a₂ a₃ h b₁ b₂ b₃ (by dsimp; cutsat)
(by dsimp; cutsat) (by dsimp; cutsat)]
rw [oppositeShiftFunctorAdd'_hom_app]
rfl
