shiftFunctor₂XXIso — Mathlib

English

There is a canonical isomorphism between the shifted second-index total and the total of the shifted bicomplex, matching the X-objects across the shift in the second index.

Русский

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

LaTeX

$$$K \\mapsto ((\\text{shiftFunctor}_2 C y).obj K).total (up\\;\\mathbb{Z}) \\cong (K.total (up\\;\\mathbb{Z})).⟦y⟧.$$$

Lean4

/-- The isomorphism `(((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b'` when `b' = b + y`. -/
def shiftFunctor₂XXIso (a b y b' : ℤ) (h : b' = b + y) : (((shiftFunctor₂ C y).obj K).X a).X b ≅ (K.X a).X b' :=
  eqToIso (by subst h; rfl)

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