The differential graded category of DG functors

For differential graded categories C and D over R, with C small, the DG functors C ⥤ D form a differential graded category. A morphism F ⟶ G of degree n is a family of degree-n morphisms η X : F X ⟶ G X which is natural up to the Koszul sign: for every morphism f : X ⟶ Y of degree p,

F f ≫ η Y = (-1) ^ (p * n) • (η X ≫ G f),

in Mathlib's enriched factor order. In Keller's order this is the familiar condition G f ∘ η X = (-1) ^ (p * n) • η Y ∘ F f. The differential, composition and identity are computed objectwise: (d η) X = d (η X), (η ≫ θ) X = η X ≫ θ X and (𝟙 F) X = 𝟙 (F X). The Leibniz rule shows that the differential of a natural family is natural with the sign of the next degree.

This is the DG category in which modules over a DG category live: a right DG module over C is a DG functor Cᵒᵖ ⥤ C(R) to cochain complexes, and the morphism complexes of modules are the Hom complexes constructed here.

The objects are those of TauCeti.DGFunctor R C D, whose ordinary morphisms are the closed degree-zero DG natural transformations; these are exactly the closed degree-zero morphisms of the DG category constructed here. The source C lives in the universe of the ground ring, so that a natural family, a family indexed by the objects of C, is again a module in that universe.

Main definitions

• TauCeti.DGFunctor.IsNatural: a family of homogeneous morphisms is natural up to the Koszul sign.
• TauCeti.DGFunctor.natTransSubmodule: the natural families of degree n.
• TauCeti.DGFunctor.homComplexData: the Hom-complex data of DG functors.
• TauCeti.DGFunctor.instDGCategory: DG functors C ⥤ D form a differential graded category.
• TauCeti.DGFunctor.dgHomEquiv: a morphism of degree n is a natural family of degree n.
• TauCeti.DGFunctor.dgApp: the component of a morphism of DG functors at an object.
• TauCeti.DGFunctor.homEquivDGCycles: DG natural transformations F ⟶ G are the closed degree-zero morphisms F ⟶ G of the DG category of DG functors.

Main results

• TauCeti.DGFunctor.IsNatural.dgDifferential: the differential of a natural family is natural.
• TauCeti.DGFunctor.IsNatural.dgComp: composites of natural families are natural.
• TauCeti.DGFunctor.dgComp_dgMap_dgApp: morphisms of DG functors are natural up to the Koszul sign.
• TauCeti.DGFunctor.dgApp_dgDifferential, TauCeti.DGFunctor.dgApp_dgComp and TauCeti.DGFunctor.dgApp_dgId: the differential, composition and identity are objectwise.
• TauCeti.DGFunctor.homEquivDGCycles_id and TauCeti.DGFunctor.homEquivDGCycles_comp: the identification of DG natural transformations with closed morphisms respects identities and composition.

References

• TauCeti.CategoryTheory.DG.AdditiveClosure.Basic, whose explicit construction through DGCategoryData.toDGCategory is followed here.
• B. Keller, Deriving DG categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.

Natural families of homogeneous morphisms

def TauCeti.DGFunctor.IsNatural {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} (η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)) : Prop

A family η X : F X ⟶ G X of morphisms of degree n is natural when it commutes with every homogeneous morphism up to the Koszul sign: for f : X ⟶ Y of degree p, the composite F f ≫ η Y is (-1) ^ (p * n) times η X ≫ G f. The degree m of both composites is left free, so that the condition can be used without transporting degrees.

theorem TauCeti.DGFunctor.isNatural_def {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} : IsNatural η ↔ ∀ ⦃X Y : C⦄ ⦃p m : ℤ⦄ (f : DGHom R p X Y) (h₁ : p + n = m) (h₂ : n + p = m), dgComp R ((F.toEnrichedFunctor.dgMap p) f) (η Y) h₁ = (p * n).negOnePow • dgComp R (η X) ((G.toEnrichedFunctor.dgMap p) f) h₂

The defining condition of a natural family.

theorem TauCeti.DGFunctor.IsNatural.dgComp_dgMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} (hη : IsNatural η) {X Y : C} {p m : ℤ} (f : DGHom R p X Y) (h₁ : p + n = m) (h₂ : n + p = m) : TauCeti.dgComp R ((F.toEnrichedFunctor.dgMap p) f) (η Y) h₁ = (p * n).negOnePow • TauCeti.dgComp R (η X) ((G.toEnrichedFunctor.dgMap p) f) h₂

A natural family commutes with a homogeneous morphism f of degree p up to the Koszul sign: F f ≫ η Y = (-1) ^ (p * n) • (η X ≫ G f).

theorem TauCeti.DGFunctor.isNatural_iff {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} : IsNatural η ↔ ∀ ⦃X Y : C⦄ (p : ℤ) (f : DGHom R p X Y), dgComp R ((F.toEnrichedFunctor.dgMap p) f) (η Y) ⋯ = (p * n).negOnePow • dgComp R (η X) ((G.toEnrichedFunctor.dgMap p) f) ⋯

Naturality may be checked with the degree of the two composites fixed to be p + n.

theorem TauCeti.DGFunctor.isNatural_zero {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} (n : ℤ) : IsNatural fun (x : C) => 0

The zero family is natural.

theorem TauCeti.DGFunctor.IsNatural.add {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η θ : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} (hη : IsNatural η) (hθ : IsNatural θ) : IsNatural (η + θ)

A sum of natural families is natural.

theorem TauCeti.DGFunctor.IsNatural.smul {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} (hη : IsNatural η) (r : R) : IsNatural (r • η)

A scalar multiple of a natural family is natural.

theorem TauCeti.DGFunctor.IsNatural.dgDifferential {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} (hη : IsNatural η) : IsNatural fun (X : C) => (TauCeti.dgDifferential R n) (η X)

The differential of a natural family is natural, with the Koszul sign of the next degree n + 1.

theorem TauCeti.DGFunctor.IsNatural.d {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} (hη : IsNatural η) (m : ℤ) : IsNatural fun (X : C) => (ModuleCat.Hom.hom ((dgHomComplex R (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)).d n m)) (η X)

The differentials of a Hom complex between arbitrary indices preserve natural families.

theorem TauCeti.DGFunctor.IsNatural.dgComp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : DGFunctor R C D} {p q n : ℤ} {η : (X : C) → DGHom R p (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} {θ : (X : C) → DGHom R q (G.toEnrichedFunctor.obj X) (H.toEnrichedFunctor.obj X)} (hη : IsNatural η) (hθ : IsNatural θ) (h : p + q = n) : IsNatural fun (X : C) => TauCeti.dgComp R (η X) (θ X) h

Composites of natural families are natural.

theorem TauCeti.DGFunctor.isNatural_dgId {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F : DGFunctor R C D) : IsNatural fun (X : C) => dgId R (F.toEnrichedFunctor.obj X)

The family of identities is natural.

def TauCeti.DGFunctor.natTransSubmodule {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F G : DGFunctor R C D) (n : ℤ) : Submodule R ((X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X))

The R-module of natural families of morphisms F X ⟶ G X of degree n: the degree-n morphisms F ⟶ G of the DG category of DG functors.

@[simp]

theorem TauCeti.DGFunctor.mem_natTransSubmodule {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η : (X : C) → DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)} : η ∈ F.natTransSubmodule G n ↔ IsNatural η

The Hom complexes

noncomputable def TauCeti.DGFunctor.homComplexData (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] : DGCategoryData R (DGFunctor R C D)

The Hom-complex data of DG functors C ⥤ D: natural families of homogeneous morphisms with the objectwise differential, composition and identities.

@[instance_reducible]

noncomputable instance TauCeti.DGFunctor.instDGCategory (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] : DGCategory R (DGFunctor R C D)

DG functors C ⥤ D form a differential graded category, whose morphisms of degree n are the natural families of degree n.

Morphisms, differential, composition and identity

noncomputable def TauCeti.DGFunctor.dgHomEquiv (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F G : DGFunctor R C D) (n : ℤ) : DGHom R n F G ≃ₗ[R] ↥(F.natTransSubmodule G n)

A morphism F ⟶ G of degree n of DG functors is a natural family of degree-n morphisms F X ⟶ G X.

noncomputable def TauCeti.DGFunctor.dgApp (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} (n : ℤ) (X : C) : DGHom R n F G →ₗ[R] DGHom R n (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)

The component at X of a morphism of DG functors of degree n.

theorem TauCeti.DGFunctor.dgApp_apply (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} (η : DGHom R n F G) (X : C) : (dgApp R n X) η = ↑((dgHomEquiv R F G n) η) X

The components of a morphism of DG functors are its underlying natural family.

@[simp]

theorem TauCeti.DGFunctor.dgApp_dgHomEquiv_symm_apply (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} (η : ↥(F.natTransSubmodule G n)) (X : C) : (dgApp R n X) ((dgHomEquiv R F G n).symm η) = ↑η X

The components of the morphism determined by a natural family are the members of the family.

theorem TauCeti.DGFunctor.isNatural_dgApp (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} (η : DGHom R n F G) : IsNatural fun (X : C) => (dgApp R n X) η

The components of a morphism of DG functors form a natural family.

theorem TauCeti.DGFunctor.dgComp_dgMap_dgApp (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n p m : ℤ} (η : DGHom R n F G) {X Y : C} (f : DGHom R p X Y) (h₁ : p + n = m) (h₂ : n + p = m) : dgComp R ((F.toEnrichedFunctor.dgMap p) f) ((dgApp R n Y) η) h₁ = (p * n).negOnePow • dgComp R ((dgApp R n X) η) ((G.toEnrichedFunctor.dgMap p) f) h₂

Naturality of a morphism of DG functors: for f : X ⟶ Y of degree p and η : F ⟶ G of degree n, F f ≫ η Y = (-1) ^ (p * n) • (η X ≫ G f).

theorem TauCeti.DGFunctor.dgHom_ext (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} {η θ : DGHom R n F G} (h : ∀ (X : C), (dgApp R n X) η = (dgApp R n X) θ) : η = θ

Morphisms of DG functors are determined by their components.

@[simp]

theorem TauCeti.DGFunctor.dgApp_dgDifferential (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {n : ℤ} (η : DGHom R n F G) (X : C) : (dgApp R (n + 1) X) ((dgDifferential R n) η) = (dgDifferential R n) ((dgApp R n X) η)

The differential of DG functors is objectwise: (d η) X = d (η X).

@[simp]

theorem TauCeti.DGFunctor.dgApp_dgComp (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : DGFunctor R C D} {p q n : ℤ} (η : DGHom R p F G) (θ : DGHom R q G H) (h : p + q = n) (X : C) : (dgApp R n X) (dgComp R η θ h) = dgComp R ((dgApp R p X) η) ((dgApp R q X) θ) h

Composition of DG functors is objectwise: (η ≫ θ) X = η X ≫ θ X.

@[simp]

theorem TauCeti.DGFunctor.dgApp_dgId (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F : DGFunctor R C D) (X : C) : (dgApp R 0 X) (dgId R F) = dgId R (F.toEnrichedFunctor.obj X)

The identity of a DG functor is objectwise: 𝟙 F X = 𝟙 (F X).

Closed degree-zero morphisms

The closed degree-zero morphisms F ⟶ G of this DG category are the morphisms of the ordinary category of DG functors, whose components are maps from the tensor unit to the Hom complexes.

theorem TauCeti.DGFunctor.dgApp_mem_dgCycles (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} {η : DGHom R 0 F G} (hη : η ∈ dgCycles R F G) (X : C) : (dgApp R 0 X) η ∈ dgCycles R (F.toEnrichedFunctor.obj X) (G.toEnrichedFunctor.obj X)

The components of a closed morphism of DG functors are closed.

noncomputable def TauCeti.DGFunctor.homEquivDGCycles (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F G : DGFunctor R C D) : (F ⟶ G) ≃ ↥(dgCycles R F G)

Closed degree-zero morphisms of DG functors are DG natural transformations: the morphisms F ⟶ G of the category of DG functors correspond to the closed degree-zero morphisms F ⟶ G of the DG category of DG functors, componentwise.

@[simp]

theorem TauCeti.DGFunctor.dgApp_homEquivDGCycles_apply (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} (α : F ⟶ G) (X : C) : (dgApp R 0 X) ↑((homEquivDGCycles R F G) α) = dgClosedHom R (CategoryTheory.ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (α.app X))

The components of the closed morphism determined by a DG natural transformation α are the closed morphisms underlying the components of α.

@[simp]

theorem TauCeti.DGFunctor.homEquivDGCycles_symm_app (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} (η : ↥(dgCycles R F G)) (X : C) : ((homEquivDGCycles R F G).symm η).app X = CategoryTheory.ForgetEnrichment.homTo (CochainComplex (ModuleCat R) ℤ) (dgClosedHomOf R ((dgApp R 0 X) ↑η) ⋯)

The components of the DG natural transformation determined by a closed morphism η are the components of η, regarded as maps from the tensor unit.

@[simp]

theorem TauCeti.DGFunctor.homEquivDGCycles_id (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F : DGFunctor R C D} : ↑((homEquivDGCycles R F F) (CategoryTheory.CategoryStruct.id F)) = dgId R F

The identity DG natural transformation is the identity of the DG category of DG functors.

@[simp]

theorem TauCeti.DGFunctor.homEquivDGCycles_comp (R : Type v) [CommRing R] {C : Type v} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : DGFunctor R C D} (α : F ⟶ G) (β : G ⟶ H) : ↑((homEquivDGCycles R F H) (CategoryTheory.CategoryStruct.comp α β)) = dgCompZero R ↑((homEquivDGCycles R F G) α) ↑((homEquivDGCycles R G H) β)

Composition of DG natural transformations is composition in the DG category of DG functors.