Cochain complexes enriched in their linear Hom complexes #

Let C be an R-linear preadditive category. This file enriches CochainComplex C ℤ in CochainComplex (ModuleCat R) ℤ. The enriched Hom object from F to G is TauCeti.linearHomComplex R F G, and the enriched identity is the degree-zero cocycle associated to the identity morphism of F.

Mathlib's enriched-category convention orders composition as

Hom(F, G) ⊗ Hom(G, K) ⟶ Hom(F, K).

The closed composition map TauCeti.linearHomComplexComp has the opposite factor order, dictated by the tensor differential and Keller's convention m₂(g, f) = g ∘ f. The enriched composition therefore first applies the Koszul braiding. On homogeneous cochains of degrees p and q, it sends f ⊗ g to (-1)^(p*q) • (g ∘ f), exactly the bridge between Mathlib's factor order and Keller's operation.

Main definitions #

TauCeti.linearHomComplexEnrichedComp: composition in Mathlib's enriched-category factor order.
TauCeti.linearHomComplexEnrichedCategory: the enrichment of cochain complexes in their R-linear Hom complexes.

Main results #

TauCeti.ι_linearHomComplexEnrichedComp: enriched composition on a bidegree summand.
TauCeti.cochainCompTensor_braiding_tmul: the signed braided closed-composition expression on pure tensors.
TauCeti.linearHomComplexEnrichedCategory_hom, TauCeti.linearHomComplexEnrichedCategory_eId, and TauCeti.linearHomComplexEnrichedCategory_eComp: the Hom, identity, and composition fields of the enrichment.

This advances TauCetiRoadmap/DGAInfinity/README.md, Layer 0, item "signed graded multilinear and tensor-coalgebra infrastructure", specifically "construct the k-linear Hom complex, its signed differential ..., closed composition map, and the enrichment". No formalization is vendored: the enriched-category interface and totalized monoidal structure are Mathlib's, and the closed composition map and Koszul braiding are the preceding Tau Ceti stages of this roadmap item.

References #

B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.
B. Keller, Deriving DG categories, Section 1.
Kim Morrison's Mathlib CategoryTheory.EnrichedCategory interface.

source

noncomputable def TauCeti.linearHomComplexEnrichedComp (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 ℤ) :

CategoryTheory.MonoidalCategoryStruct.tensorObj (linearHomComplex R F G) (linearHomComplex R G K) ⟶ linearHomComplex R F K

Composition of linear Hom complexes in Mathlib's enriched-category factor order. It applies the Koszul braiding and then composes cochains in Keller's order.

Equations

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

Instances For

source

theorem TauCeti.linearHomComplexEnrichedComp_def (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 ℤ) :

linearHomComplexEnrichedComp R F G K = CategoryTheory.CategoryStruct.comp (β_ (linearHomComplex R F G) (linearHomComplex R G K)).hom (linearHomComplexComp R F G K)

The enriched-order composition is the closed composition map preceded by the Koszul braiding.

source

@[simp]

theorem TauCeti.ι_linearHomComplexEnrichedComp (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 j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (linearHomComplex R F G) (linearHomComplex R G K) (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) ((linearHomComplexEnrichedComp R F G K).f j) = (p * q).negOnePow • CategoryTheory.CategoryStruct.comp (β_ ((linearHomComplex R F G).X p) ((linearHomComplex R G K).X q)).hom (cochainCompTensor R F G K q p j ⋯)

On the bidegree-(p, q) summand, enriched-order composition carries the Koszul sign (-1)^(p*q), swaps the two module factors, and composes the resulting cochains.

source

@[simp]

theorem TauCeti.ι_linearHomComplexEnrichedComp_assoc (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 j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) {Z : ModuleCat R} (h✝ : (linearHomComplex R F K).X j ⟶ Z) :

CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιMapBifunctor (linearHomComplex R F G) (linearHomComplex R G K) (CategoryTheory.MonoidalCategory.curriedTensor (ModuleCat R)) (ComplexShape.up ℤ) p q j h) (CategoryTheory.CategoryStruct.comp ((linearHomComplexEnrichedComp R F G K).f j) h✝) = CategoryTheory.CategoryStruct.comp ((p * q).negOnePow • CategoryTheory.CategoryStruct.comp (β_ ((linearHomComplex R F G).X p) ((linearHomComplex R G K).X q)).hom (cochainCompTensor R F G K q p j ⋯)) h✝

On the bidegree-(p, q) summand, enriched-order composition carries the Koszul sign (-1)^(p*q), swaps the two module factors, and composes the resulting cochains.

source

@[simp]

theorem TauCeti.cochainCompTensor_braiding_tmul (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 j : ℤ) (h : (ComplexShape.up ℤ).π (ComplexShape.up ℤ) (ComplexShape.up ℤ) (p, q) = j) (z₁ : ↑↧(CochainComplex.HomComplex.Cochain F G p)) (z₂ : ↑↧(CochainComplex.HomComplex.Cochain G K q)) :

(p * q).negOnePow • (ModuleCat.Hom.hom (cochainCompTensor R F G K q p j ⋯)) ((ModuleCat.Hom.hom (β_ ↧(CochainComplex.HomComplex.Cochain F G p) ↧(CochainComplex.HomComplex.Cochain G K q)).hom) (z₁ ⊗ₜ[R] z₂)) = (p * q).negOnePow • CochainComplex.HomComplex.Cochain.comp z₁ z₂ h

On a pure tensor, the signed closed-composition expression after the module braiding is Keller composition with the Koszul sign converting from Mathlib's factor order.

source

@[instance_reducible]