shiftFunctorZero' — Mathlib

English

There is a canonical isomorphism between the shift by zero and the identity functor, i.e., shift by 0 is naturally isomorphic to the identity on cochain complexes.

Русский

Существует каноническое изоморфизм между сдвигом на ноль и тождественным функтором: сдвиг на 0 эквивалентен тождественному на комплексах Cochain.

LaTeX

$$$ \\mathrm{shiftFunctor}(C,0) \\simeq \\mathrm{Id}_{\\mathrm{CochainComplex}(C,\\mathbb{Z})} $$$

Lean4

/-- The shift functor by `n` on `CochainComplex C ℤ` identifies to the identity
functor when `n = 0`. -/
@[simps!]
def shiftFunctorZero' (n : ℤ) (h : n = 0) : shiftFunctor C n ≅ 𝟭 _ :=
  NatIso.ofComponents
    (fun K => Hom.isoOfComponents (fun i => K.shiftFunctorObjXIso _ _ _ (by cutsat)) (fun _ _ _ => by simp [h]))
    (fun _ ↦ by ext; simp)

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