The direct-sum module of a nonnegative cochain complex

The terms of a cochain complex form one module by external direct sum. Its differential sends the degree-n inclusion to the degree-n + 1 inclusion of the original differential. This gives a square-zero endomorphism of degree one, with zero homogeneous pieces in negative degrees. The construction lets finite tensor products of complexes use a differential on one carrier. A homotopy between cochain morphisms likewise becomes one map of degree minus one on the total modules, which satisfies the homotopy identity d ∘ h + h ∘ d = f - g there; this is how a contraction of a complex is carried to its total module.

The universal-property and componentwise map constructions are Mathlib's DirectSum.toModule and DirectSum.lmap. No exactness or decomposition assumption is required. The inclusion equations accept the caller's decision procedure for equality on natural numbers; the constructions themselves do not depend on that choice.

@[reducible, inline]

abbrev CochainComplex.directSumModule {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) : Type v

The external direct sum of the terms of a nonnegative cochain complex.

def CochainComplex.directSumDifferential {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) : K.directSumModule →ₗ[R] K.directSumModule

The endomorphism which applies the differential and raises the summand index by one.

@[simp]

theorem CochainComplex.directSumDifferential_lof {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) [h : DecidableEq ℕ] (n : ℕ) (x : ↑(K.X n)) : K.directSumDifferential ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) (n + 1)) ((ModuleCat.Hom.hom (K.d n (n + 1))) x)

The total differential on an included term is the included original differential.

@[simp]

theorem CochainComplex.directSumDifferential_sq {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) (x : K.directSumModule) : K.directSumDifferential (K.directSumDifferential x) = 0

The total differential squares to zero.

def CochainComplex.directSumPiece {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) : ℤ → Submodule R K.directSumModule

The homogeneous pieces of the total module, extended by zero in negative degrees.

theorem CochainComplex.isInternal_directSumPiece {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) : DirectSum.IsInternal K.directSumPiece

The homogeneous pieces decompose the total module as an internal direct sum.

@[simp]

theorem CochainComplex.directSumPiece_natCast {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) [h : DecidableEq ℕ] (n : ℕ) : K.directSumPiece ↑n = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) n).range

A nonnegative homogeneous piece is the range of the corresponding inclusion.

theorem CochainComplex.directSumPiece_of_neg {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) {p : ℤ} (hp : p < 0) : K.directSumPiece p = ⊥

Negative homogeneous pieces vanish.

theorem CochainComplex.lof_mem_directSumPiece {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) [DecidableEq ℕ] (n : ℕ) (x : ↑(K.X n)) : (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) n) x ∈ K.directSumPiece ↑n

Every included term is homogeneous in its summand degree.

theorem CochainComplex.isHomogeneous_directSumDifferential {R : Type u} [Ring R] (K : CochainComplex (ModuleCat R) ℕ) : TauCeti.LinearMap.IsHomogeneous K.directSumDifferential K.directSumPiece K.directSumPiece 1

The total differential is homogeneous of degree one.

def CochainComplex.directSumMap {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} (f : K ⟶ L) : K.directSumModule →ₗ[R] L.directSumModule

The componentwise map of total modules induced by a cochain morphism.

@[simp]

theorem CochainComplex.directSumMap_lof {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} [DecidableEq ℕ] (f : K ⟶ L) (n : ℕ) (x : ↑(K.X n)) : (directSumMap f) ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) n) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(L.X n)) n) ((ModuleCat.Hom.hom (f.f n)) x)

On an included term the total map is the component of the cochain morphism.

@[simp]

theorem CochainComplex.directSumMap_id {R : Type u} [Ring R] {K : CochainComplex (ModuleCat R) ℕ} : directSumMap (CategoryTheory.CategoryStruct.id K) = LinearMap.id

Taking the total map preserves identity morphisms.

@[simp]

theorem CochainComplex.directSumMap_comp {R : Type u} [Ring R] {K L N : CochainComplex (ModuleCat R) ℕ} (f : K ⟶ L) (g : L ⟶ N) : directSumMap (CategoryTheory.CategoryStruct.comp f g) = directSumMap g ∘ₗ directSumMap f

Taking the total map preserves composition.

theorem CochainComplex.directSumMap_differential {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} (f : K ⟶ L) (x : K.directSumModule) : (directSumMap f) (K.directSumDifferential x) = L.directSumDifferential ((directSumMap f) x)

A total map commutes with the total differentials.

theorem CochainComplex.isHomogeneous_directSumMap {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} (f : K ⟶ L) : TauCeti.LinearMap.IsHomogeneous (directSumMap f) K.directSumPiece L.directSumPiece 0

A cochain morphism preserves the homogeneous pieces in the total module.

def Homotopy.directSumHomotopy {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} {f g : K ⟶ L} (H : Homotopy f g) : K.directSumModule →ₗ[R] L.directSumModule

The total map of a homotopy between cochain morphisms: it lowers the summand index by one, applying the component H.hom (n + 1) n to the degree-n + 1 summand, and vanishes on the degree-zero summand.

@[simp]

theorem Homotopy.directSumHomotopy_lof_zero {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} {f g : K ⟶ L} [h : DecidableEq ℕ] (H : Homotopy f g) (x : ↑(K.X 0)) : H.directSumHomotopy ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) 0) x) = 0

The total map of a homotopy vanishes on the degree-zero summand.

@[simp]

theorem Homotopy.directSumHomotopy_lof_succ {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} {f g : K ⟶ L} [h : DecidableEq ℕ] (H : Homotopy f g) (n : ℕ) (x : ↑(K.X (n + 1))) : H.directSumHomotopy ((DirectSum.lof R ℕ (fun (n : ℕ) => ↑(K.X n)) (n + 1)) x) = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(L.X n)) n) ((ModuleCat.Hom.hom (H.hom (n + 1) n)) x)

On a positive summand the total map of a homotopy is its component, one degree down.

theorem Homotopy.directSumDifferential_directSumHomotopy_add {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} {f g : K ⟶ L} (H : Homotopy f g) (x : K.directSumModule) : L.directSumDifferential (H.directSumHomotopy x) + H.directSumHomotopy (K.directSumDifferential x) = (CochainComplex.directSumMap f) x - (CochainComplex.directSumMap g) x

The homotopy identity on total modules: d ∘ h + h ∘ d = f - g.

theorem Homotopy.isHomogeneous_directSumHomotopy {R : Type u} [Ring R] {K L : CochainComplex (ModuleCat R) ℕ} {f g : K ⟶ L} (H : Homotopy f g) : TauCeti.LinearMap.IsHomogeneous H.directSumHomotopy K.directSumPiece L.directSumPiece (-1)

The total map of a homotopy is homogeneous of degree minus one.