shiftFunctorObjXIso — Mathlib

English

A precise equality about shifting indices i,j with a given equality j = i + n; the iso respects this index relation.

Русский

Точная равенство по перемещению индексов i,j при условии j = i+n; изоморфизм сохраняет эту связь индексов.

LaTeX

$$$ (\\mathrm{shiftFunctorObjXIso}\\, K\\, n\\, i\\, m)\\;: \\; X_i^{\\langle n \\rangle} \\cong X_m $$$

Lean4

/-- The canonical isomorphism `((shiftFunctor C n).obj K).X i ≅ K.X m` when `m = i + n`. -/
@[simp]
def shiftFunctorObjXIso (K : CochainComplex C ℤ) (n i m : ℤ) (hm : m = i + n) :
    ((shiftFunctor C n).obj K).X i ≅ K.X m :=
  K.XIsoOfEq hm.symm

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