k-linear dg categories

DGCategory is stated over abelian groups so that its Hom-complexes are exactly the complexes CochainComplex.HomComplex produces. Linearity over a commutative ring is layered on top, the way CategoryTheory.Linear layers over Preadditive in Mathlib.

DGLinear.homComplex exposes those same graded groups and differentials as a ModuleCat k-valued cochain complex. It is an abbreviation rather than a second Hom-complex: only the already supplied module structures and DGLinear.d_smul are added.

ADR-0011 records why this is a refinement rather than part of the definition: a first draft that baked ModuleCat k into dgHom collided with the AddCommGrpCat-valued HomComplex three separate times.

class CategoryTheory.DGLinear (k : Type w) [CommRing k] (C : Type u) [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] : Prop

A k-linear structure on a dg category: given k-module structures on the graded pieces of the Hom-complexes, both the differential and the composition are k-linear.

The module structures are a parameter rather than a field. A field cannot be used as an instance inside the same class's later field types, and the version that tried produced a stuck HSMul metavariable on the first axiom.

• d_smul {X Y : C} (p q : ℤ) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p q)) (c • f) = c • (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p q)) f

  The differential is k-linear.

• comp_smul_left {X Y Z : C} (p q r : ℤ) (h : p + q = r) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : ((DGCategoryStruct.dgComp p q r h) (c • f)) g = c • ((DGCategoryStruct.dgComp p q r h) f) g

  Composition is k-linear in its first argument.

• comp_smul_right {X Y Z : C} (p q r : ℤ) (h : p + q = r) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) (g : ↑((DGCategoryStruct.dgHom Y Z).X q)) : ((DGCategoryStruct.dgComp p q r h) f) (c • g) = c • ((DGCategoryStruct.dgComp p q r h) f) g

  Composition is k-linear in its second argument.

@[reducible, inline]

abbrev CategoryTheory.DGLinear.homComplex (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) : CochainComplex (ModuleCat k) ℤ

The Hom-complex of a k-linear dg category, regarded as a complex of k-modules. Its underlying graded groups and differentials are unchanged.

Equations

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

@[simp]

theorem CategoryTheory.DGLinear.homComplex_X (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) (p : ℤ) : (homComplex k X Y).X p = ModuleCat.of k ↑((DGCategoryStruct.dgHom X Y).X p)

@[simp]

theorem CategoryTheory.DGLinear.homComplex_d_apply (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X Y : C) (p q : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (ModuleCat.Hom.hom ((homComplex k X Y).d p q)) f = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d p q)) f

def CategoryTheory.DGLinear.postcompCochain (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X : C) {Y Z : C} (p : ℤ) : ↑((homComplex k Y Z).X p) →ₗ[k] CochainComplex.HomComplex.Cochain (homComplex k X Y) (homComplex k X Z) p

Right composition by a degree-p dg morphism, as a degree-p linear cochain between Hom-complexes with a fixed source.

Equations

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

@[simp]

theorem CategoryTheory.DGLinear.postcompCochain_apply (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X : C) {Y Z : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom Y Z).X p)) (i j : ℤ) (h : i + p = j) (g : ↑((DGCategoryStruct.dgHom X Y).X i)) : (ModuleCat.Hom.hom (((postcompCochain k X p) f).v i j h)) g = ((DGCategoryStruct.dgComp i p j h) g) f

theorem CategoryTheory.DGLinear.postcompCochain_d (k : Type w) [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] (X : C) {Y Z : C} (p q : ℤ) (f : ↑((DGCategoryStruct.dgHom Y Z).X p)) : CochainComplex.HomComplex.δ p q ((postcompCochain k X p) f) = (postcompCochain k X q) ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom Y Z).d p q)) f)

Right composition intertwines the Hom-complex differential with the dg differential. The two Koszul terms cancel because Mathlib's Hom differential uses the successor sign.

class CategoryTheory.DGFunctor.Linear (k : Type w) [CommRing k] {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [(X Y : D) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [DGLinear k D] (F : DGFunctor C D) : Prop

A scalar-preserving dg functor between k-linear dg categories. This is a refinement of DGFunctor, parallel to Mathlib's Functor.Linear; it records only linearity of the maps on Hom-complexes.

• map_smul {X Y : C} (p : ℤ) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (F.map p) (c • f) = c • (F.map p) f

  A linear dg functor preserves scalar multiplication in every degree.

@[simp]

theorem CategoryTheory.DGFunctor.map_smul {k : Type w} [CommRing k] {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [(X Y : D) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [DGLinear k D] {F : DGFunctor C D} [Linear k F] {X Y : C} (p : ℤ) (c : k) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : (F.map p) (c • f) = c • (F.map p) f

A linear dg functor preserves scalar multiplication in every degree.

instance CategoryTheory.DGFunctor.idLinear {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] : Linear k (id C)

The identity dg functor is linear.

instance CategoryTheory.DGFunctor.compLinear {k : Type w} [CommRing k] {C : Type u} {D : Type u'} {E : Type u''} [DGCategory C] [DGCategory D] [DGCategory E] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [(X Y : D) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [(X Y : E) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [DGLinear k D] [DGLinear k E] {F : DGFunctor C D} {G : DGFunctor D E} [Linear k F] [Linear k G] : Linear k (F.comp G)

A composite of linear dg functors is linear.