Documentation

TauCeti.CategoryTheory.DG.CochainComplex.Basic

Cochain complexes as a differential graded category #

Cochain complexes in an R-linear preadditive category are enriched in cochain complexes of R-modules through CochainComplex.linearHomComplex, so they form a differential graded category. This file evaluates the differential graded operations of TauCeti/CategoryTheory/DG/Basic.lean on that example: the degree-n morphisms are the degree-n cochains, the differential is Mathlib's signed CochainComplex.HomComplex.δ, the identity is the identity cochain, and composition is composition of cochains with the Koszul sign.

That sign is the whole content of the comparison. A differential graded category composes Hom(X, Y) ⊗ Hom(Y, Z) ⟶ Hom(X, Z) while composition of cochains is a closed map out of Hom(Y, Z) ⊗ Hom(X, Y), and interchanging the two factors of a tensor product of complexes is the Koszul braiding. Hence a degree-p cochain z₁ followed by a degree-q cochain z₂ composes to (-1) ^ (p * q) • z₁.comp z₂. This is the bridge between Mathlib's enriched factor order and Keller's untwisted operation m₂ (g, f) = g ∘ f, and it is what fixes the sign conventions of every later differential graded construction.

Main results #

Main definitions #

References #

source
@[simp]
theorem TauCeti.dgDifferential_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G : CochainComplex C ℤ} (n : ℤ) (z : DGHom R n F G) :
(dgDifferential R n) z = CochainComplex.HomComplex.δ n (n + 1) z

The differential of the differential graded category of cochain complexes is the signed differential δ of cochains.

source
@[simp]
theorem TauCeti.dgId_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : CochainComplex C ℤ) :
dgId R F = CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id F)

The identity of the differential graded category of cochain complexes is the identity cochain.

source
@[simp]
theorem TauCeti.dgComp_linearHomComplex (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {p q n : ℤ} (z₁ : DGHom R p F G) (z₂ : DGHom R q G K) (h : p + q = n) :
dgComp R z₁ z₂ h = (p * q).negOnePow • CochainComplex.HomComplex.Cochain.comp z₁ z₂ h

Composition in the differential graded category of cochain complexes is composition of cochains, carrying the Koszul sign which converts Mathlib's enriched factor order into Keller's untwisted operation.

source
theorem TauCeti.xIsoOfEq_hom_v (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {a b : ℤ} (h : a = b) (z : DGHom R a K L) (p q : ℤ) (hpq : p + b = q) :
CochainComplex.HomComplex.Cochain.v ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.XIsoOfEq (dgHomComplex R K L) h).hom) z) p q hpq = CochainComplex.HomComplex.Cochain.v z p q ⋯

Degree transport of a cochain does not change its components.

source
theorem TauCeti.dgComp_v (R : Type v) [CommRing R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {K L M : CochainComplex C ℤ} {a b c : ℤ} (z₁ : DGHom R a K L) (z₂ : DGHom R b L M) (h : a + b = c) (x y w : ℤ) (h₁ : x + a = y) (h₂ : y + b = w) :
CochainComplex.HomComplex.Cochain.v (dgComp R z₁ z₂ h) x w ⋯ = (a * b).negOnePow • CategoryTheory.CategoryStruct.comp (CochainComplex.HomComplex.Cochain.v z₁ x y h₁) (CochainComplex.HomComplex.Cochain.v z₂ y w h₂)

The component of the DG composition of cochains is their componentwise composition with the Koszul sign.

source
noncomputable def TauCeti.cochainEval (R : Type v) [CommRing R] {K L : CochainComplex (ModuleCat R) ℤ} {n : ℤ} (x : ↑(K.X n)) (p q : ℤ) (h : n + p = q) :
DGHom R p K L →ₗ[R] ↑(L.X q)

Evaluation of degree-p cochains between complexes of R-modules at an element x of degree n of the source, as an R-linear map to the degree-q part of the target.

Instances For
    source
    @[simp]
    theorem TauCeti.cochainEval_apply (R : Type v) [CommRing R] {K L : CochainComplex (ModuleCat R) ℤ} {n : ℤ} (x : ↑(K.X n)) (p q : ℤ) (h : n + p = q) (z : DGHom R p K L) :
    (cochainEval R x p q h) z = (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v z n q h)) x

    Evaluating a cochain at x applies its component out of the degree of x.

    source
    theorem CochainComplex.HomComplex.δ_v_apply_of_d_eq_zero {R : Type u_1} [Ring R] {K L : CochainComplex (ModuleCat R) ℤ} {n m : ℤ} (hnm : n + 1 = m) (z : Cochain K L n) {p q r : ℤ} (hpq : p + n = q) (hpr : p + m = r) {a : ↑(K.X p)} (ha : (ModuleCat.Hom.hom (K.d p (p + 1))) a = 0) :
    (ModuleCat.Hom.hom ((δ n m z).v p r hpr)) a = (ModuleCat.Hom.hom (L.d q r)) ((ModuleCat.Hom.hom (z.v p q hpq)) a)

    On an element killed by the differential of the source, the differential of a cochain of complexes of modules is the differential of the target applied to the value of the cochain.

    source
    theorem CochainComplex.HomComplex.Cochain.v_apply_mem_ker_of_δ_eq_zero {R : Type u_1} [Ring R] {K L : CochainComplex (ModuleCat R) ℤ} (z : Cochain K L 0) (hz : δ 0 1 z = 0) {p q : ℤ} (hpq : p + 1 = q) {a : ↑(K.X p)} (ha : (ModuleCat.Hom.hom (K.d p q)) a = 0) :
    (ModuleCat.Hom.hom (z.v p p ⋯)) a ∈ (ModuleCat.Hom.hom (L.d p q)).ker

    A closed cochain of degree zero between complexes of modules sends elements killed by the differential to elements killed by the differential.