English
The inverse relation to the previous compatibility shows how the inverse of the totalShift₁Iso interacts with the second shift homomorphism, again up to the sign (xy).
Русский
Обратная совместимость аналогична предыдущей, демонстрируя как взаимо действует обратное отображение totalShift₁Iso с гомоморфизмом второго сдвига, с учётом знака (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.mapIso}( ((\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_inv (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j =
ComplexShape.σ c₁ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]) :=
by simp [totalFlipIso, totalFlipIsoX]
