English
The hom-component of shiftFunctorAdd' on the opposite category decomposes via op-shift iso factors and the maps associated to a and b components of the shift, in a carefully nested composition.
Русский
Гомоморфизм shiftFunctorAdd' на Opposite распадается через факторы оп-изоморфизма сдвига и отображения, связанных с a,b-компонентами сдвига, в аккуратно вложенной композиции.
LaTeX
$$$ (\\text{shiftFunctorAdd'} \\; C^{op} a_1 a_2 a_3 h).hom.app X = (\\text{shiftFunctorOpIso } C a_3 b_3 h_3).hom.app X ≫ (\\text{something}) ≫ (\\text{shiftFunctorOpIso } C a_2 b_2 h_2).inv.app _ ≫ (\\text{shiftFunctor } C^{op} a_2).map ((\\text{shiftFunctorOpIso } C a_1 b_1 h_1).inv.app X) $$$
Lean4
theorem opShiftFunctorEquivalence_unitIso_hom_app_eq (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) :
(opShiftFunctorEquivalence C p).unitIso.hom.app X =
(opShiftFunctorEquivalence C n).unitIso.hom.app X ≫
(((opShiftFunctorEquivalence C m).unitIso.hom.app (X⟦n⟧)).unop⟦n⟧').op ≫
((shiftFunctorAdd' C m n p h).hom.app _).op ≫
(((shiftFunctorAdd' Cᵒᵖ n m p (by cutsat)).inv.app X).unop⟦p⟧').op :=
by
dsimp [opShiftFunctorEquivalence]
simp only [shiftFunctorAdd'_op_inv_app _ n m p (by cutsat) _ _ _ (add_neg_cancel n) (add_neg_cancel m)
(add_neg_cancel p),
shiftFunctor_op_map _ _ (add_neg_cancel m), Category.assoc, Iso.inv_hom_id_app_assoc]
erw [Functor.map_id, Functor.map_id, Functor.map_id, Functor.map_id, id_comp, id_comp, id_comp, comp_id, comp_id]
dsimp
rw [comp_id,
shiftFunctorCompIsoId_add'_hom_app _ _ _ _ _ _ (neg_add_cancel m) (neg_add_cancel n) (neg_add_cancel p) h]
dsimp
rw [Category.assoc, Category.assoc]
rfl
