The normalized identification of cochains between shifted complexes

For cochain complexes K and L and shifts r and s, the cochains of degree n + (s - r) from K to L are identified with the cochains of degree n from K⟦r⟧ to L⟦s⟧. This file records the normalized such identification: it sends a cochain z to the cochain whose component K⟦r⟧^i ⟶ L⟦s⟧^j is (-1)^(r * n) times the component K^(i + r) ⟶ L^(j + s) of z, and it intertwines the differential δ of the target with (-1)^(s - r) δ on the source.

It is assembled from Mathlib's CochainComplex.HomComplex.Cochain.rightShift and CochainComplex.HomComplex.Cochain.leftShift, which together differ from it by the sign (-1)^(r * (r - 1) / 2) depending only on the source shift. This is the sign convention of the shift closure of a differential graded category.

Main definitions

• TauCeti.cochainShiftLinearEquiv: the normalized identification Cochain K L (n + (s - r)) ≃ₗ[R] Cochain (K⟦r⟧) (L⟦s⟧) n.

Main results

• TauCeti.cochainShiftLinearEquiv_v: the identification multiplies the underlying components by (-1)^(r * n).
• TauCeti.δ_cochainShiftLinearEquiv: the identification intertwines δ with (-1)^(s - r) δ.

References

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

noncomputable def TauCeti.cochainShiftLinearEquiv (R : Type v) [Ring R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (K L : CochainComplex V ℤ) (r s n : ℤ) : CochainComplex.HomComplex.Cochain K L (n + (s - r)) ≃ₗ[R] CochainComplex.HomComplex.Cochain (K⟦r⟧) (L⟦s⟧) n

The normalized identification of the cochains of degree n + (s - r) from K to L with the cochains of degree n from K⟦r⟧ to L⟦s⟧, assembled from Mathlib's right and left shifts of cochains and the sign (-1)^(r * (r - 1) / 2). Its components are computed by TauCeti.cochainShiftLinearEquiv_v.

@[simp]

theorem TauCeti.cochainShiftLinearEquiv_v (R : Type v) [Ring R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (K L : CochainComplex V ℤ) (r s n : ℤ) (z : CochainComplex.HomComplex.Cochain K L (n + (s - r))) (i j : ℤ) (hij : i + n = j) : ((cochainShiftLinearEquiv R K L r s n) z).v i j hij = (r * n).negOnePow • z.v (i + r) (j + s) ⋯

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).

theorem TauCeti.δ_cochainShiftLinearEquiv (R : Type v) [Ring R] {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Preadditive V] [CategoryTheory.Linear R V] (K L : CochainComplex V ℤ) (r s n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain K L (n + (s - r))) : CochainComplex.HomComplex.δ n m ((cochainShiftLinearEquiv R K L r s n) z) = (cochainShiftLinearEquiv R K L r s m) ((s - r).negOnePow • CochainComplex.HomComplex.δ (n + (s - r)) (m + (s - r)) z)

The normalized identification intertwines the differential δ of cochains between the shifted complexes with (-1)^(s - r) δ on cochains between the unshifted ones.