totalShift₁XIso — Mathlib

English

There is a canonical isomorphism between the total complex of the shifted bicomplex and the shifted total complex, with a natural identification on X-components.

Русский

Существует канонический изоморфизм между общим комплексом смещённого бикомплекса и смещённым общим комплексом, с естественным сопряжением на X-компонентах.

LaTeX

$$$\\text{totalShift1XIso} : ((\\text{shiftFunctor}_1 C x).obj K).total (up\\;\\mathbb{Z}) \\cong (K.total (up\\;\\mathbb{Z})).⟦x⟧$$$

Lean4

/-- Auxiliary definition for `totalShift₁Iso`. -/
noncomputable def totalShift₁XIso (n n' : ℤ) (h : n + x = n') :
    (((shiftFunctor₁ C x).obj K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X n'
    where
  hom := totalDesc _ (fun p q hpq => K.ιTotal (up ℤ) (p + x) q n' (by dsimp at hpq ⊢; omega))
  inv :=
    totalDesc _
      (fun p q hpq =>
        (K.XXIsoOfEq _ _ _ (Int.sub_add_cancel p x) rfl).inv ≫
          ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n (by dsimp at hpq ⊢; omega))
  hom_inv_id := by
    ext p q h
    dsimp
    simp only [ι_totalDesc_assoc, CochainComplex.shiftFunctor_obj_X', ι_totalDesc, comp_id]
    exact ((shiftFunctor₁ C x).obj K).XXIsoOfEq_inv_ιTotal _ (by omega) rfl _ _
  inv_hom_id := by
    ext
    dsimp
    simp only [ι_totalDesc_assoc, Category.assoc, ι_totalDesc, XXIsoOfEq_inv_ιTotal, comp_id]

Похожие утверждения