shiftFunctor₁XXIso — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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