Scalar-linear copowers in the standard dg category of module complexes

For a commutative ring k, Mathlib's total tensor product of cochain complexes represents the repository's scalar-linear copower interface in Cdg (ModuleCat k). The core comparison curries a degree-p cochain

K ⊗ X ⟶ W

to a degree-p cochain

K ⟶ DGLinear.homComplex k X W.

The inverse is assembled with Mathlib's coproduct eliminator for the total complex and TensorProduct.lift. The universal cochain is the curry of the identity on K ⊗ X; its chain-map law is the usual Koszul cancellation between the vertical tensor differential (-1)^i d_X and the Hom-complex term (-1)^(i+1) d_X.

Mathlib's current monoidal structure on ModuleCat requires the scalar ring and module objects to live in the same universe. Accordingly this first concrete instance is intentionally stated for k : Type v and ModuleCat.{v} k; no universe-lifting wrapper is introduced here.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Cdg.linearTensorObj (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : Cdg (ModuleCat k)

Mathlib's total tensor product, regarded as an object of the standard dg category of module complexes.

Equations

• CategoryTheory.Cdg.linearTensorObj k K X = HomologicalComplex.tensorObj K (CategoryTheory.Cdg.of (ModuleCat k) X)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Cdg.linearTensorιOfEq (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) (i j n : ℤ) (h : i + j = n) : ((MonoidalCategory.curriedTensor (ModuleCat k)).obj (K.X i)).obj ((of (ModuleCat k) X).X j) ⟶ (of (ModuleCat k) (linearTensorObj k K X)).X n

The inclusion of the (i,j) summand in an arbitrarily equal total degree.

Equations

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Cdg.linearTensorι (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) (i j : ℤ) : ((MonoidalCategory.curriedTensor (ModuleCat k)).obj (K.X i)).obj ((of (ModuleCat k) X).X j) ⟶ (of (ModuleCat k) (linearTensorObj k K X)).X (i + j)

The inclusion of the (i,j) summand in total degree i + j.

Equations

• CategoryTheory.Cdg.linearTensorι k K X i j = CategoryTheory.Cdg.linearTensorιOfEq k K X i j (i + j) ⋯

noncomputable def CategoryTheory.Cdg.tensorCurryCochain (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X W : Cdg (ModuleCat k)) (p : ℤ) : ↑((DGCategoryStruct.dgHom (linearTensorObj k K X) W).X p) →ₗ[k] CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p

Curry a homogeneous cochain out of a total tensor product into a homogeneous cochain whose values are Hom-complex cochains.

Equations

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

noncomputable def CategoryTheory.Cdg.tensorCochainLinearEquiv (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X W : Cdg (ModuleCat k)) (p : ℤ) : ↑((DGCategoryStruct.dgHom (linearTensorObj k K X) W).X p) ≃ₗ[k] CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p

The degreewise tensor--Hom adjunction for homogeneous cochains.

Equations

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

noncomputable def CategoryTheory.Cdg.linearTensorUnivCochain (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X (linearTensorObj k K X)) 0

The universal degree-zero cochain, obtained by currying the identity of the total tensor product.

Equations

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

theorem CategoryTheory.Cdg.linearTensorUnivCochain_apply (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) (i j q : ℤ) (hjq : j + i = q) (x : ↑(K.X i)) (y : ↑((of (ModuleCat k) X).X j)) : (ModuleCat.Hom.hom (CochainComplex.HomComplex.Cochain.v ((ModuleCat.Hom.hom ((linearTensorUnivCochain k K X).v i i ⋯)) x) j q hjq)) y = (ModuleCat.Hom.hom (linearTensorιOfEq k K X i j q ⋯)) (x ⊗ₜ[k] y)

Pointwise evaluation of the universal cochain is the corresponding total tensor summand inclusion.

theorem CategoryTheory.Cdg.linearTensorι_d_apply (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) (i j n n' : ℤ) (hij : i + j = n) (hnn' : n + 1 = n') (x : ↑(K.X i)) (y : ↑((of (ModuleCat k) X).X j)) : (ModuleCat.Hom.hom ((of (ModuleCat k) (linearTensorObj k K X)).d n n')) ((ModuleCat.Hom.hom (linearTensorιOfEq k K X i j n hij)) (x ⊗ₜ[k] y)) = (ModuleCat.Hom.hom (linearTensorιOfEq k K X (i + 1) j n' ⋯)) ((ModuleCat.Hom.hom (K.d i (i + 1))) x ⊗ₜ[k] y) + i.negOnePow • (ModuleCat.Hom.hom (linearTensorιOfEq k K X i (j + 1) n' ⋯)) (x ⊗ₜ[k] (ModuleCat.Hom.hom ((of (ModuleCat k) X).d j (j + 1))) y)

The total tensor differential on a pure tensor in one summand is the sum of the horizontal differential and the signed vertical differential.

theorem CategoryTheory.Cdg.linearTensorUnivCochain_mem (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : CochainComplex.HomComplex.δ 0 1 (linearTensorUnivCochain k K X) = 0

The universal cochain is closed. Its two vertical Koszul terms have coefficients (-1)^i and (-1)^(i+1) and cancel.

noncomputable def CategoryTheory.Cdg.linearTensorUnivCocycle (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : CochainComplex.HomComplex.Cocycle K (DGLinear.homComplex k X (linearTensorObj k K X)) 0

The universal cochain bundled as a degree-zero cocycle.

Equations

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

noncomputable def CategoryTheory.Cdg.linearTensorUniv (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : K ⟶ DGLinear.homComplex k X (linearTensorObj k K X)

The universal chain map from the coefficient complex to the Hom-complex out of X.

Equations

• CategoryTheory.Cdg.linearTensorUniv k K X = (CategoryTheory.Cdg.linearTensorUnivCocycle k K X).homOf

theorem CategoryTheory.Cdg.cochain_ofHom_linearTensorUniv (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : CochainComplex.HomComplex.Cochain.ofHom (linearTensorUniv k K X) = linearTensorUnivCochain k K X

Forgetting the universal chain map back to a cochain recovers the explicitly curried identity.

theorem CategoryTheory.Cdg.linearCopowerCochain_linearTensorUniv (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X W : Cdg (ModuleCat k)) (p : ℤ) : linearCopowerCochain k (linearTensorUniv k K X) p = tensorCurryCochain k K X W p

Composition with the universal chain map is exactly tensor currying.

noncomputable def CategoryTheory.Cdg.isLinearCopowerOfLinearTensor (k : Type v) [CommRing k] (K : CochainComplex (ModuleCat k) ℤ) (X : Cdg (ModuleCat k)) : IsLinearCopowerOf k K X (linearTensorObj k K X)

Mathlib's total tensor product represents the scalar-linear copower in the standard dg category of module complexes.

Equations

• CategoryTheory.Cdg.isLinearCopowerOfLinearTensor k K X = { univ := CategoryTheory.Cdg.linearTensorUniv k K X, bijective := ⋯ }

instance CategoryTheory.Cdg.hasLinearCopowers (k : Type v) [CommRing k] : HasLinearCopowers k (Cdg (ModuleCat k))

The standard dg category of same-universe k-module complexes has all scalar-linear copowers.