shiftShortComplexFunctor' — Mathlib

English

There is a natural linear isomorphism between shifted homology functors: shift by n on homology in degree a corresponds to homology in degree a+n.

Русский

Существует естественная линейная изоморфия между сдвигами гомологии: сдвиг на n в степени a соответствует гомологии в степени a+n.

LaTeX

$$$ (\\mathrm{homologyFunctor} (C, \\mathrm{up}\\mathbb{Z}) a)^{\\mathrm{shift}}_n \\cong \\mathrm{homologyFunctor} (C, \\mathrm{up}\\mathbb{Z}) (a+n)$$$

Lean4

/-- The natural isomorphism `(K⟦n⟧).sc' i j k ≅ K.sc' i' j' k'` when `n + i = i'`,
`n + j = j'` and `n + k = k'`. -/
@[simps!]
def shiftShortComplexFunctor' (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') :
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n) ⋙ shortComplexFunctor' C _ i j k ≅
      shortComplexFunctor' C _ i' j' k' :=
  NatIso.ofComponents
    (fun K =>
      ShortComplex.isoMk (n.negOnePow • ((shiftEval C n i i' hi).app K)) ((shiftEval C n j j' hj).app K)
        (n.negOnePow • ((shiftEval C n k k' hk).app K)) (by simp) (by simp))
    (fun f ↦ by ext <;> simp)

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