English
Reflexivity of the inverse naturality in the totalShift₂Iso_inv_f relation in trivial index-shift cases.
Русский
Рефлексивность обратной естественности в отношении totalShift₂Iso_inv_f в тривиальных случаях сдвига индексов.
LaTeX
$$$ι\\_totalShift₂Iso\\_inv\\_f (a b n) (hb') (b' n')$$$
Lean4
@[reassoc]
theorem ι_totalShift₂Iso_inv_f (a b n : ℤ) (h : a + b = n) (b' n' : ℤ) (hb' : a + b' = n') (hn' : n' = n + y) :
K.ιTotal (up ℤ) a b' n' hb' ≫
(CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n n' hn').inv ≫ (K.totalShift₂Iso y).inv.f n =
(a * y).negOnePow •
(K.shiftFunctor₂XXIso a b y b' (by cutsat)).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) a b n h :=
by
subst hn'
obtain rfl : b = b' - y := by cutsat
dsimp [totalShift₂Iso, totalShift₂XIso, shiftFunctor₂XXIso, XXIsoOfEq]
simp only [id_comp, ι_totalDesc]
