English
A dual compatibility statement for the inverses of the shifted total iso; describes how the inverse components interact with shift XX iso and iotaTotal.
Русский
Двойственная совместимость для обратной стороны изоморфизма totalShift2Iso; описывает взаимодействие обратных компонент с XX-изоморфизмом и iotaTotal.
LaTeX
$$$ι\\_totalShift₂Iso\\_inv\\_f$$$
Lean4
@[reassoc]
theorem ι_totalShift₂Iso_hom_f (a b n : ℤ) (h : a + b = n) (b' : ℤ) (hb' : b' = b + y) (n' : ℤ) (hn' : n' = n + y) :
((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₂Iso y).hom.f n =
(a * y).negOnePow •
(K.shiftFunctor₂XXIso a b y b' hb').hom ≫
K.ιTotal (up ℤ) a b' n' (by dsimp; cutsat) ≫
(CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv :=
by
subst hb' hn'
dsimp [totalShift₂Iso, totalShift₂XIso]
simp only [ι_totalDesc, comp_id, id_comp]
