English
The inverse component of shiftFunctorAdd' on Xᵒᵖ is given by composing the map from the inverse of the corresponding op-shift iso and the op of the map from shift functors, mirroring the forward construction with inverses in place.
Русский
Обратный компонент shiftFunctorAdd' на X^{op} задаётся как композиция отображения из инвертированного оп-изоморфизма сдвига и обратного отображения функторов сдвига, аналогично прямому конструированию.
LaTeX
$$$ (\\text{shiftFunctorAdd'} \\, C^{op}\\; a_1 a_2 a_3 h).inv.app X = (\\text{shiftFunctor } C^{op} a_2).map ((\\text{shiftFunctorOpIso } C a_1 b_1 h_1).inv.app X).op \\gg (\\text{shiftFunctorOpIso } C a_2 b_2 h_2) .hom.app _ \\gg ((\\text{shiftFunctorAdd'} \\; C b_1 b_2 b_3 (by cutsat)).inv.app X.unop).op \\gg (\\text{shiftFunctorOpIso } C a_3 b_3 h_3).inv.app X $$$
Lean4
theorem shiftFunctorAdd'_op_inv_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).inv.app X =
(shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C _ _ h₁).hom.app X) ≫
(shiftFunctorOpIso C _ _ h₂).hom.app _ ≫
((shiftFunctorAdd' C b₁ b₂ b₃ (by cutsat)).hom.app X.unop).op ≫ (shiftFunctorOpIso C _ _ h₃).inv.app X :=
by
rw [← cancel_epi ((shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X), Iso.hom_inv_id_app,
shiftFunctorAdd'_op_hom_app X a₁ a₂ a₃ h b₁ b₂ b₃ h₁ h₂ h₃, assoc, assoc, assoc, ← Functor.map_comp_assoc,
Iso.inv_hom_id_app]
erw [Functor.map_id, id_comp, Iso.inv_hom_id_app_assoc]
rw [← op_comp_assoc, Iso.hom_inv_id_app, op_id, id_comp, Iso.hom_inv_id_app]
