The R-linear Hom complex of two cochain complexes

Let C be an R-linear preadditive category and let F and G be cochain complexes in C. Mathlib's CochainComplex.HomComplex.Cochain F G n is the R-module of degree-n cochains from F to G, and CochainComplex.HomComplex.δ is the signed differential δ z = d_G ∘ z + (-1)^{n+1} z ∘ d_F, already known to be R-linear and square-zero. Mathlib assembles this data into CochainComplex.HomComplex F G, a cochain complex of abelian groups, which forgets the R-module structure. This file assembles the same data into a cochain complex of R-modules.

That complex is the object a differential graded category is enriched in: a DG category over R is a category enriched in CochainComplex (ModuleCat R) ℤ, and CochainComplex C ℤ is the motivating example. The AddCommGrpCat-valued complex retains only the underlying ℤ-linearity, whereas a DG category over R requires the R-module structure on its Hom complexes.

Main definitions

• TauCeti.linearHomComplex R F G: the R-linear Hom complex, a cochain complex of R-modules whose degree-n term is Cochain F G n and whose differential is δ.
• TauCeti.linearHomComplexPrecomp and TauCeti.linearHomComplexPostcomp: precomposition and postcomposition by a morphism of cochain complexes, as morphisms of R-linear Hom complexes.
• TauCeti.linearHomComplexFunctor: the two variances bundled into a bifunctor, contravariant in the source and covariant in the target.

Main results

• TauCeti.forget₂LinearHomComplexIso: forgetting the R-module structure degreewise recovers Mathlib's CochainComplex.HomComplex.

This advances TauCetiRoadmap/DGAInfinity/README.md, Layer 0, item "signed graded multilinear and tensor-coalgebra infrastructure", specifically its request to "construct the k-linear Hom complex, its signed differential d(f) = d_Y f - (-1)^{|f|} f d_X, closed composition map, and the enrichment, and compare its underlying additive-group complex with Mathlib's CochainComplex.HomComplex". No formalization is vendored: the cochain modules, the differential δ, its R-linearity and the Leibniz rule for composition are all Mathlib's.

Implementation notes

linearHomComplex and linearHomComplexFunctor carry @[expose], while every operation built from them is sealed and used only through its characteristic lemmas. The exposures permit the dependent component types (linearHomComplex R F G).X n and ((linearHomComplexFunctor R).obj F).obj G to elaborate against their advertised values. The element-level API itself is normalized to ModuleCat.of R (Cochain F G n) and explicit .hom application, so ordinary simp and rw use it without unfolding either construction.

References

• B. Keller, Deriving DG categories, Section 1.
• Joël Riou's Mathlib construction CochainComplex.HomComplex and its cochain/δ API in Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean. The construction here adapts it by retaining ModuleCat R in place of AddCommGrpCat, with the same sign convention.

def TauCeti.linearHomComplex (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) : CochainComplex (ModuleCat R) ℤ

The R-linear Hom complex of two cochain complexes: in degree n it is the R-module CochainComplex.HomComplex.Cochain F G n of degree-n cochains, and its differential is the signed differential δ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.linearHomComplex_X (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n : ℤ) : (linearHomComplex R F G).X n = ↧(CochainComplex.HomComplex.Cochain F G n)

@[simp]

theorem TauCeti.linearHomComplex_d_apply (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n m : ℤ) (z : ↑↧(CochainComplex.HomComplex.Cochain F G n)) : (ModuleCat.Hom.hom ((linearHomComplex R F G).d n m)) z = CochainComplex.HomComplex.δ n m z

def TauCeti.forget₂LinearHomComplexIso (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) : ((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).mapHomologicalComplex (ComplexShape.up ℤ)).obj (linearHomComplex R F G) ≅ F.HomComplex G

Forgetting the R-module structure of the R-linear Hom complex recovers Mathlib's CochainComplex.HomComplex.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.forget₂LinearHomComplexIso_hom_f (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n : ℤ) : (forget₂LinearHomComplexIso R F G).hom.f n = CategoryTheory.CategoryStruct.id ((((CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat).mapHomologicalComplex (ComplexShape.up ℤ)).obj (linearHomComplex R F G)).X n)

The forward component of the comparison isomorphism is the identity.

@[simp]

theorem TauCeti.forget₂LinearHomComplexIso_inv_f (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) (n : ℤ) : (forget₂LinearHomComplexIso R F G).inv.f n = CategoryTheory.CategoryStruct.id ((F.HomComplex G).X n)

The inverse component of the comparison isomorphism is the identity.

def TauCeti.linearHomComplexPrecomp (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (G : CochainComplex C ℤ) : linearHomComplex R F₂ G ⟶ linearHomComplex R F₁ G

Precomposition by a morphism φ : F₁ ⟶ F₂ of cochain complexes, as a morphism of R-linear Hom complexes. It commutes with the differentials because φ is a cocycle, so that the second term of the Leibniz rule for δ vanishes.

Equations

• TauCeti.linearHomComplexPrecomp R φ G = { f := fun (n : ℤ) => ModuleCat.ofHom (TauCeti.cochainPrecomp✝ R φ G n), comm' := ⋯ }

def TauCeti.linearHomComplexPostcomp (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {G₁ G₂ : CochainComplex C ℤ} (F : CochainComplex C ℤ) (ψ : G₁ ⟶ G₂) : linearHomComplex R F G₁ ⟶ linearHomComplex R F G₂

Postcomposition by a morphism ψ : G₁ ⟶ G₂ of cochain complexes, as a morphism of R-linear Hom complexes.

Equations

• TauCeti.linearHomComplexPostcomp R F ψ = { f := fun (n : ℤ) => ModuleCat.ofHom (TauCeti.cochainPostcomp✝ R F ψ n), comm' := ⋯ }

@[simp]

theorem TauCeti.linearHomComplexPrecomp_f_apply {R : Type w} [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (G : CochainComplex C ℤ) (n : ℤ) (z : ↑↧(CochainComplex.HomComplex.Cochain F₂ G n)) : (ModuleCat.Hom.hom ((linearHomComplexPrecomp R φ G).f n)) z = (CochainComplex.HomComplex.Cochain.ofHom φ).comp z ⋯

@[simp]

theorem TauCeti.linearHomComplexPostcomp_f_apply {R : Type w} [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {G₁ G₂ : CochainComplex C ℤ} (F : CochainComplex C ℤ) (ψ : G₁ ⟶ G₂) (n : ℤ) (z : ↑↧(CochainComplex.HomComplex.Cochain F G₁ n)) : (ModuleCat.Hom.hom ((linearHomComplexPostcomp R F ψ).f n)) z = CochainComplex.HomComplex.Cochain.comp z (CochainComplex.HomComplex.Cochain.ofHom ψ) ⋯

@[simp]

theorem TauCeti.linearHomComplexPrecomp_id (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) : linearHomComplexPrecomp R (CategoryTheory.CategoryStruct.id F) G = CategoryTheory.CategoryStruct.id (linearHomComplex R F G)

@[simp]

theorem TauCeti.linearHomComplexPrecomp_comp (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ F₃ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (φ' : F₂ ⟶ F₃) (G : CochainComplex C ℤ) : linearHomComplexPrecomp R (CategoryTheory.CategoryStruct.comp φ φ') G = CategoryTheory.CategoryStruct.comp (linearHomComplexPrecomp R φ' G) (linearHomComplexPrecomp R φ G)

@[simp]

theorem TauCeti.linearHomComplexPostcomp_id (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F G : CochainComplex C ℤ) : linearHomComplexPostcomp R F (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (linearHomComplex R F G)

@[simp]

theorem TauCeti.linearHomComplexPostcomp_comp (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {G₁ G₂ G₃ : CochainComplex C ℤ} (F : CochainComplex C ℤ) (ψ : G₁ ⟶ G₂) (ψ' : G₂ ⟶ G₃) : linearHomComplexPostcomp R F (CategoryTheory.CategoryStruct.comp ψ ψ') = CategoryTheory.CategoryStruct.comp (linearHomComplexPostcomp R F ψ) (linearHomComplexPostcomp R F ψ')

theorem TauCeti.linearHomComplexPrecomp_postcomp_comm (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {F₁ F₂ G₁ G₂ : CochainComplex C ℤ} (φ : F₁ ⟶ F₂) (ψ : G₁ ⟶ G₂) : CategoryTheory.CategoryStruct.comp (linearHomComplexPrecomp R φ G₁) (linearHomComplexPostcomp R F₁ ψ) = CategoryTheory.CategoryStruct.comp (linearHomComplexPostcomp R F₂ ψ) (linearHomComplexPrecomp R φ G₂)

Precomposition and postcomposition commute.

def TauCeti.linearHomComplexFunctor (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] : CategoryTheory.Functor (CochainComplex C ℤ)ᵒᵖ (CategoryTheory.Functor (CochainComplex C ℤ) (CochainComplex (ModuleCat R) ℤ))

The R-linear Hom complex as a bifunctor: contravariant in the source cochain complex and covariant in the target one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.linearHomComplexFunctor_obj_map (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : (CochainComplex C ℤ)ᵒᵖ) {X✝ Y✝ : CochainComplex C ℤ} (ψ : X✝ ⟶ Y✝) : ((linearHomComplexFunctor R).obj F).map ψ = linearHomComplexPostcomp R (Opposite.unop F) ψ

@[simp]

theorem TauCeti.linearHomComplexFunctor_map_app (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] {X✝ Y✝ : (CochainComplex C ℤ)ᵒᵖ} (φ : X✝ ⟶ Y✝) (G : CochainComplex C ℤ) : ((linearHomComplexFunctor R).map φ).app G = linearHomComplexPrecomp R φ.unop G

@[simp]

theorem TauCeti.linearHomComplexFunctor_obj_obj (R : Type w) [Ring R] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear R C] (F : (CochainComplex C ℤ)ᵒᵖ) (G : CochainComplex C ℤ) : ((linearHomComplexFunctor R).obj F).obj G = linearHomComplex R (Opposite.unop F) G