English
A technical compatibility statement describing how the component of the total-shift isomorphism interacts with the shifted total and the X-structure, in terms of the hom components.
Русский
Техническое свойство совместимости компонента изоморфизма totalShift1Iso с сдвинутым общим комплексом и структурой X, в терминах компонент гомома.
LaTeX
$$$((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n = (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫ K.ιTotal (up ℤ) a b' n' ⋯$$$
Lean4
@[reassoc]
theorem ι_totalShift₁Iso_hom_f (a b n : ℤ) (h : a + b = n) (a' : ℤ) (ha' : a' = a + x) (n' : ℤ) (hn' : n' = n + x) :
((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n =
(K.shiftFunctor₁XXIso a x a' ha' b).hom ≫
K.ιTotal (up ℤ) a' b n' (by dsimp; cutsat) ≫
(CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv :=
by
subst ha' hn'
dsimp [totalShift₁Iso, totalShift₁XIso]
simp only [ι_totalDesc, comp_id, id_comp]
