English
A technical identity expressing how opEquiv' interacts with opShiftFunctorEquivalence counitInv, with composing op-shift and unop,'s.
Русский
Техническое тождество, описывающее взаимодействие opEquiv' с counitInv опShiftFunctorEquivalence и с композициями против(op).
LaTeX
$$$$ \\text{opEquiv'}\\_symm\\_op\\_opShiftFunctorEquivalence\\_counitIso\\_inv\\_app = \\text{...} $$$$
Lean4
theorem opEquiv_symm_comp {a b : ℤ} (f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a)
(g : ShiftedHom (Opposite.op Y) (Opposite.op X) b) {c : ℤ} (h : b + a = c) :
(opEquiv _).symm (f.comp g h) = ((opEquiv _).symm g).comp ((opEquiv _).symm f) (by cutsat) :=
by
rw [opEquiv_symm_apply, opEquiv_symm_apply,
opShiftFunctorEquivalence_unitIso_inv_app_eq _ _ _ _ (show a + b = c by cutsat), comp, comp]
dsimp
rw [assoc, assoc, assoc, assoc, ← Functor.map_comp, ← unop_comp_assoc, Iso.inv_hom_id_app]
dsimp
rw [assoc, id_comp, Functor.map_comp, ← NatTrans.naturality_assoc, ← NatTrans.naturality, opEquiv_symm_apply]
dsimp
rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, ← Functor.map_comp_assoc]
rw [← unop_comp_assoc]
erw [← NatTrans.naturality]
rfl
