Formal shifts of cochain complexes are cochain shifts

Cochain complexes in an R-linear preadditive category form a differential graded category, and so do the formal shifts K[r] of its shift closure TauCeti.DGShiftClosure. This file evaluates the formal shifts: it constructs the DG functor TauCeti.DGShiftClosure.toCochainComplex sending K[r] to Mathlib's shifted complex K⟦r⟧, and proves it is an isomorphism on Hom complexes.

On morphisms it is the normalized identification Hom(K, L)[s - r] ≅ Hom(K⟦r⟧, L⟦s⟧): a cochain z of degree p + s - r from K to L goes to the cochain of degree p from K⟦r⟧ to L⟦s⟧ whose component K⟦r⟧^i ⟶ L⟦s⟧^j is (-1)^(r * p) times the component K^(i + r) ⟶ L^(j + s) of z (TauCeti.DGShiftClosure.shiftCochainEquiv_v). That this is a DG functor is a check of every sign in TauCeti/CategoryTheory/DG/ShiftClosure/Basic.lean against Mathlib's shift: the shift closure differential (-1)^(s - r) d matches the differential δ of cochains between shifted complexes, and the shift closure composition sign (-1)^((t - s) * (p + s - r)) matches the Koszul-signed composition of cochains.

The identification is the general normalized identification of cochains between shifted complexes, TauCeti.cochainShiftLinearEquiv, precomposed with the defining identification TauCeti.DGShiftClosure.dgHomEquiv of the Hom complexes of the shift closure.

Main definitions

• TauCeti.DGShiftClosure.shiftCochainEquiv: the normalized identification Hom(K, L)[s - r] ≅ Hom(K⟦r⟧, L⟦s⟧) in each degree.
• TauCeti.DGShiftClosure.toCochainComplex: the DG functor K[r] ↦ K⟦r⟧.

Main results

• TauCeti.DGShiftClosure.shiftCochainEquiv_v: the identification multiplies the underlying cochain by (-1)^(r * p).
• TauCeti.DGShiftClosure.isIso_toCochainComplex_map: K[r] ↦ K⟦r⟧ is an isomorphism on Hom complexes.

References

• A. I. Bondal and M. M. Kapranov, Enhanced triangulated categories, Section 1.
• B. Keller, Deriving DG categories, Section 1.

noncomputable def TauCeti.DGShiftClosure.shiftCochainEquiv (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (X Y : DGShiftClosure (CochainComplex V ℤ)) (n : ℤ) : DGHom R n X Y ≃ₗ[R] DGHom R n (X.obj⟦X.shift⟧) (Y.obj⟦Y.shift⟧)

The normalized identification Hom(K, L)[s - r] ≅ Hom(K⟦r⟧, L⟦s⟧) in degree n: a morphism K[r] ⟶ L[s] of degree n in the shift closure, that is, a cochain z of degree n + (s - r) from K to L, goes to the cochain from K⟦r⟧ to L⟦s⟧ with components (-1)^(r * n) • z^(i + r, j + s).

@[simp]

theorem TauCeti.DGShiftClosure.shiftCochainEquiv_v (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] {X Y : DGShiftClosure (CochainComplex V ℤ)} {n : ℤ} (f : DGHom R n X Y) (i j : ℤ) (hij : i + n = j) : CochainComplex.HomComplex.Cochain.v ((shiftCochainEquiv R X Y n) f) i j hij = (X.shift * n).negOnePow • CochainComplex.HomComplex.Cochain.v ((dgHomEquiv R X Y n) f) (i + X.shift) (j + Y.shift) ⋯

The normalized identification multiplies the underlying cochain by (-1)^(r * n): its component K⟦r⟧^i ⟶ L⟦s⟧^j is (-1)^(r * n) times the component K^(i + r) ⟶ L^(j + s).

noncomputable def TauCeti.DGShiftClosure.toCochainComplex (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) (DGShiftClosure (CochainComplex V ℤ)) (CochainComplex V ℤ)

The DG functor K[r] ↦ K⟦r⟧ evaluating the formal shifts of cochain complexes, acting on morphisms by the normalized identification TauCeti.DGShiftClosure.shiftCochainEquiv.

@[simp]

theorem TauCeti.DGShiftClosure.toCochainComplex_obj (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (X : DGShiftClosure (CochainComplex V ℤ)) : (toCochainComplex R).obj X = X.obj⟦X.shift⟧

The formal shift K[r] goes to the shifted complex K⟦r⟧.

theorem TauCeti.DGShiftClosure.dgMap_toCochainComplex (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] {X Y : DGShiftClosure (CochainComplex V ℤ)} {n : ℤ} (f : DGHom R n X Y) : ((toCochainComplex R).dgMap n) f = (shiftCochainEquiv R X Y n) f

The functor K[r] ↦ K⟦r⟧ acts on morphisms by the normalized identification.

instance TauCeti.DGShiftClosure.isIso_toCochainComplex_map (R : Type v) [CommRing R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (X Y : DGShiftClosure (CochainComplex V ℤ)) : CategoryTheory.IsIso ((toCochainComplex R).map X Y)

Formal shifts of cochain complexes are cochain shifts: the DG functor K[r] ↦ K⟦r⟧ is an isomorphism on Hom complexes, so the shift-closure signs agree with Mathlib's cochain shifts.