English
The hom component of the totalShift₁Iso_hom_totalShift₂Iso_hom identity expresses how the first and second shifts interact at the level of morphisms of the total complex, up to the sign (xy).
Русский
Гомоморфизмная часть тотоРы достаточности взаимодействия первого и второго сдвигов на уровне отображений общего комплекса с учетом знака (xy).
LaTeX
$$$(((\text{shift}_2 C y).\obj K).totalShift_1^x).hom \;\circ \; (K.totalShift_2^y).hom\langle x\rangle' = (x y).negOnePow \; \big( \text{total.map} ( ((\text{shiftFunctor}_1\_2 CommIso C x y).hom.app K) ) (up \Z) \; \circ \; (((\text{shift}_1 C x).obj K).totalShift_2^y).hom \circ \; (K.totalShift_1^x).hom\langle y\rangle' \circ (\text{shiftFunctorComm}(CochainComplex C \Z) x y).hom.app _ \big)$$$
Lean4
@[reassoc (attr := simp)]
theorem ιTotal_totalFlipIso_f_hom (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₂ c₁ c (i₂, i₁) = j) :
K.flip.ιTotal c i₂ i₁ j h ≫ (K.totalFlipIso c).hom.f j =
ComplexShape.σ c₁ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j (by rw [← ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]) :=
by simp [totalFlipIso, totalFlipIsoX]
