Differential graded functors and their homotopy functors

A DG functor between differential graded categories is an enriched functor CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D: a chain map Hom(X, Y) ⟶ Hom(F X, F Y) for every pair of objects, compatible with the enriched identities and compositions. This file unpacks that data into the calculus of homogeneous morphisms used throughout TauCeti.CategoryTheory.DG.Basic: a DG functor acts on morphisms of each degree, and this action commutes with the differential and preserves identities and composition. Conversely, such an action on homogeneous morphisms determines a DG functor.

Consequently a DG functor sends closed degree-zero morphisms to closed ones and boundaries to boundaries, and it induces a linear functor H⁰(F) : H⁰(C) ⥤ H⁰(D) between homotopy categories. Its action on the morphisms H⁰(Hom(X, Y)) is the map induced on degree-zero cohomology by the chain map F.map X Y, so the quasi-isomorphism conditions on DG functors translate directly into statements about H⁰(F).

Main definitions

• CategoryTheory.EnrichedFunctor.dgMap: the action of a DG functor on morphisms of degree n.
• CategoryTheory.EnrichedFunctor.ofDGMap: the DG functor with a prescribed action on homogeneous morphisms commuting with the differential, identities, and composition.
• CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory: the functor H⁰(F) induced on homotopy categories.
• CategoryTheory.EnrichedFunctor.mapDGHomotopyCategoryIdIso and CategoryTheory.EnrichedFunctor.mapDGHomotopyCategoryCompIso: H⁰ of the identity DG functor and of a composite.

Main results

• CategoryTheory.EnrichedFunctor.dgMap_dgDifferential: a DG functor commutes with the differential.
• CategoryTheory.EnrichedFunctor.dgMap_dgId and CategoryTheory.EnrichedFunctor.dgMap_dgComp: a DG functor preserves identities and composition of homogeneous morphisms.
• CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory_map_homOf: H⁰(F) sends the class of a closed degree-zero morphism f to the class of F f.

References

• B. Keller, Deriving DG categories, Sections 1 and 2.
• V. Drinfeld, DG quotients of DG categories, Section 2.

The action on homogeneous morphisms

def CategoryTheory.EnrichedFunctor.dgMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} (n : ℤ) : TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n (F.obj X) (F.obj Y)

The action of a DG functor on morphisms of degree n: the degree-n component of its chain map on Hom complexes.

Equations

• F.dgMap n = ModuleCat.Hom.hom ((F.map X Y).f n)

theorem CategoryTheory.EnrichedFunctor.dgMap_apply {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (F.dgMap n) f = (ModuleCat.Hom.hom ((F.map X Y).f n)) f

The action of a DG functor on degree-n morphisms is the degree-n component of its map on Hom complexes.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_dgDifferential {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : (F.dgMap (n + 1)) ((TauCeti.dgDifferential R n) f) = (TauCeti.dgDifferential R n) ((F.dgMap n) f)

A DG functor commutes with the differential of the Hom complexes.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_dgId {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (X : C) : (F.dgMap 0) (TauCeti.dgId R X) = TauCeti.dgId R (F.obj X)

A DG functor preserves identities.

theorem CategoryTheory.EnrichedFunctor.dgCompMap_naturality {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y Z : C} (p q n : ℤ) (h : p + q = n) : CategoryStruct.comp (TauCeti.dgCompMap R X Y Z p q n h) ((F.map X Z).f n) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ((F.map X Y).f p) ((F.map Y Z).f q)) (TauCeti.dgCompMap R (F.obj X) (F.obj Y) (F.obj Z) p q n h)

The bidegree component of enriched composition is natural under a DG functor.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_dgComp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y Z : C} {p q n : ℤ} (f : TauCeti.DGHom R p X Y) (g : TauCeti.DGHom R q Y Z) (h : p + q = n) : (F.dgMap n) (TauCeti.dgComp R f g h) = TauCeti.dgComp R ((F.dgMap p) f) ((F.dgMap q) g) h

A DG functor preserves the composition of homogeneous morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.id_dgMap {R : Type v} [CommRing R] {C : Type u₁} [TauCeti.DGCategory R C] {X Y : C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : ((id (CochainComplex (ModuleCat R) ℤ) C).dgMap n) f = f

The identity DG functor acts as the identity on homogeneous morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.comp_dgMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] [TauCeti.DGCategory R E] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (G : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) D E) {X Y : C} {n : ℤ} (f : TauCeti.DGHom R n X Y) : ((comp (CochainComplex (ModuleCat R) ℤ) F G).dgMap n) f = (G.dgMap n) ((F.dgMap n) f)

A composite of DG functors acts on homogeneous morphisms by composing the two actions.

DG functors from their action on homogeneous morphisms

def CategoryTheory.EnrichedFunctor.ofDGMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (obj : C → D) (map : {X Y : C} → (n : ℤ) → TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n (obj X) (obj Y)) (map_dgDifferential : ∀ {X Y : C} (n : ℤ) (f : TauCeti.DGHom R n X Y), (map (n + 1)) ((TauCeti.dgDifferential R n) f) = (TauCeti.dgDifferential R n) ((map n) f)) (map_dgId : ∀ (X : C), (map 0) (TauCeti.dgId R X) = TauCeti.dgId R (obj X)) (map_dgComp : ∀ {X Y Z : C} {p q n : ℤ} (f : TauCeti.DGHom R p X Y) (g : TauCeti.DGHom R q Y Z) (h : p + q = n), (map n) (TauCeti.dgComp R f g h) = TauCeti.dgComp R ((map p) f) ((map q) g) h) : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D

The DG functor with a prescribed action on homogeneous morphisms: linear maps on the morphisms of each degree which commute with the differential and preserve identities and composition. This is the converse of CategoryTheory.EnrichedFunctor.dgMap_dgDifferential, CategoryTheory.EnrichedFunctor.dgMap_dgId and CategoryTheory.EnrichedFunctor.dgMap_dgComp: the chain maps on Hom complexes and the enriched functor axioms are assembled from these elementwise laws.

Equations

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

@[simp]

theorem CategoryTheory.EnrichedFunctor.ofDGMap_obj {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (obj : C → D) (map : {X Y : C} → (n : ℤ) → TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n (obj X) (obj Y)) (map_dgDifferential : ∀ {X Y : C} (n : ℤ) (f : TauCeti.DGHom R n X Y), (map (n + 1)) ((TauCeti.dgDifferential R n) f) = (TauCeti.dgDifferential R n) ((map n) f)) (map_dgId : ∀ (X : C), (map 0) (TauCeti.dgId R X) = TauCeti.dgId R (obj X)) (map_dgComp : ∀ {X Y Z : C} {p q n : ℤ} (f : TauCeti.DGHom R p X Y) (g : TauCeti.DGHom R q Y Z) (h : p + q = n), (map n) (TauCeti.dgComp R f g h) = TauCeti.dgComp R ((map p) f) ((map q) g) h) (X : C) : (ofDGMap obj (fun {X Y : C} => map) ⋯ map_dgId ⋯).obj X = obj X

The DG functor with a prescribed action on homogeneous morphisms acts on objects by the prescribed map.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgMap_ofDGMap {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (obj : C → D) (map : {X Y : C} → (n : ℤ) → TauCeti.DGHom R n X Y →ₗ[R] TauCeti.DGHom R n (obj X) (obj Y)) (map_dgDifferential : ∀ {X Y : C} (n : ℤ) (f : TauCeti.DGHom R n X Y), (map (n + 1)) ((TauCeti.dgDifferential R n) f) = (TauCeti.dgDifferential R n) ((map n) f)) (map_dgId : ∀ (X : C), (map 0) (TauCeti.dgId R X) = TauCeti.dgId R (obj X)) (map_dgComp : ∀ {X Y Z : C} {p q n : ℤ} (f : TauCeti.DGHom R p X Y) (g : TauCeti.DGHom R q Y Z) (h : p + q = n), (map n) (TauCeti.dgComp R f g h) = TauCeti.dgComp R ((map p) f) ((map q) g) h) {X Y : C} (n : ℤ) (f : TauCeti.DGHom R n X Y) : ((ofDGMap obj (fun {X Y : C} => map) ⋯ map_dgId ⋯).dgMap n) f = (map n) f

The DG functor with a prescribed action on homogeneous morphisms acts on them by that action.

theorem CategoryTheory.EnrichedFunctor.dgMap_mem_dgCycles {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} {f : TauCeti.DGHom R 0 X Y} (hf : f ∈ TauCeti.dgCycles R X Y) : (F.dgMap 0) f ∈ TauCeti.dgCycles R (F.obj X) (F.obj Y)

A DG functor sends closed degree-zero morphisms to closed degree-zero morphisms.

@[simp]

theorem CategoryTheory.EnrichedFunctor.dgClosedHom_forget_map {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : TauCeti.dgClosedHom R (ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (CategoryStruct.comp (ForgetEnrichment.homTo (CochainComplex (ModuleCat R) ℤ) f) (F.map (ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y)))) = (F.dgMap 0) (TauCeti.dgClosedHom R f)

The underlying functor of a DG functor acts on closed morphisms by its degree-zero map.

@[simp]

theorem CategoryTheory.EnrichedFunctor.forget_map_dgClosedHomOf {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} (f : TauCeti.DGHom R 0 X Y) (hf : f ∈ TauCeti.dgCycles R X Y) : ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (CategoryStruct.comp (ForgetEnrichment.homTo (CochainComplex (ModuleCat R) ℤ) (TauCeti.dgClosedHomOf R f hf)) (F.map X Y)) = TauCeti.dgClosedHomOf R ((F.dgMap 0) f) ⋯

The underlying functor sends a morphism represented by a cocycle to the morphism represented by its image under the DG functor.

theorem CategoryTheory.EnrichedFunctor.dgMap_mem_dgBoundaries {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} {f : TauCeti.DGHom R 0 X Y} (hf : f ∈ TauCeti.dgBoundaries R X Y) : (F.dgMap 0) f ∈ TauCeti.dgBoundaries R (F.obj X) (F.obj Y)

A DG functor sends degree-zero boundaries to degree-zero boundaries.

The induced functor on homotopy categories

theorem CategoryTheory.EnrichedFunctor.homologyMap_dgHomotopyComp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y Z : C} (a : ↑(TauCeti.DGHomotopyClass R X Y)) (b : ↑(TauCeti.DGHomotopyClass R Y Z)) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (F.map X Z) 0)) (((TauCeti.dgHomotopyComp R X Y Z) a) b) = ((TauCeti.dgHomotopyComp R (F.obj X) (F.obj Y) (F.obj Z)) ((ModuleCat.Hom.hom (HomologicalComplex.homologyMap (F.map X Y) 0)) a)) ((ModuleCat.Hom.hom (HomologicalComplex.homologyMap (F.map Y Z) 0)) b)

The map induced by a DG functor on degree-zero cohomology of Hom complexes is compatible with the composition of homotopy classes.

noncomputable def CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : Functor (TauCeti.DGHomotopyCategory R C) (TauCeti.DGHomotopyCategory R D)

The functor H⁰(F) : H⁰(C) ⥤ H⁰(D) induced by a DG functor F. On morphisms it is the map induced by F.map X Y on degree-zero cohomology of Hom complexes; by CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory_map_homOf it sends the class of a closed morphism f to the class of F f.

Equations

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

@[simp]

theorem CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory_obj_of {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (X : C) : F.mapDGHomotopyCategory.obj (TauCeti.DGHomotopyCategory.of R X) = TauCeti.DGHomotopyCategory.of R (F.obj X)

H⁰(F) sends an object X of H⁰(C) to F X.

theorem CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory_map {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : TauCeti.DGHomotopyCategory R C} (f : X ⟶ Y) : F.mapDGHomotopyCategory.map f = (ModuleCat.Hom.hom (HomologicalComplex.homologyMap (F.map (TauCeti.DGHomotopyCategory.underlying R X) (TauCeti.DGHomotopyCategory.underlying R Y)) 0)) f

H⁰(F) acts on morphisms by the map induced by F on degree-zero cohomology of Hom complexes.

@[simp]

theorem CategoryTheory.EnrichedFunctor.mapDGHomotopyCategory_map_homOf {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) {X Y : C} (f : TauCeti.DGHom R 0 X Y) (hf : f ∈ TauCeti.dgCycles R X Y) : F.mapDGHomotopyCategory.map (TauCeti.DGHomotopyCategory.homOf R f hf) = TauCeti.DGHomotopyCategory.homOf R ((F.dgMap 0) f) ⋯

H⁰(F) sends the class of a closed degree-zero morphism f to the class of F f.

noncomputable def CategoryTheory.EnrichedFunctor.forgetCompDgClosedToHomotopyIso {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : F.forget.comp (TauCeti.dgClosedToHomotopy R) ≅ (TauCeti.dgClosedToHomotopy R).comp F.mapDGHomotopyCategory

Taking the homotopy class of a closed morphism commutes with a DG functor.

Equations

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

@[simp]

theorem CategoryTheory.EnrichedFunctor.forgetCompDgClosedToHomotopyIso_hom_app {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (X : ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) : F.forgetCompDgClosedToHomotopyIso.hom.app X = CategoryStruct.id ((F.forget.comp (TauCeti.dgClosedToHomotopy R)).obj X)

The forward component of the comparison between Z⁰(F) followed by the quotient and the quotient followed by H⁰(F) is the identity.

@[simp]

theorem CategoryTheory.EnrichedFunctor.forgetCompDgClosedToHomotopyIso_inv_app {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (X : ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) : F.forgetCompDgClosedToHomotopyIso.inv.app X = CategoryStruct.id (((TauCeti.dgClosedToHomotopy R).comp F.mapDGHomotopyCategory).obj X)

The inverse component of the comparison between Z⁰(F) followed by the quotient and the quotient followed by H⁰(F) is the identity.

instance CategoryTheory.EnrichedFunctor.instAdditiveDGHomotopyCategoryMapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : F.mapDGHomotopyCategory.Additive

instance CategoryTheory.EnrichedFunctor.instLinearDGHomotopyCategoryMapDGHomotopyCategory {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : Functor.Linear R F.mapDGHomotopyCategory

noncomputable def CategoryTheory.EnrichedFunctor.mapDGHomotopyCategoryIdIso {R : Type v} [CommRing R] {C : Type u₁} [TauCeti.DGCategory R C] : (id (CochainComplex (ModuleCat R) ℤ) C).mapDGHomotopyCategory ≅ Functor.id (TauCeti.DGHomotopyCategory R C)

H⁰ of the identity DG functor is the identity functor.

Equations

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

noncomputable def CategoryTheory.EnrichedFunctor.mapDGHomotopyCategoryCompIso {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} {E : Type u₃} [TauCeti.DGCategory R C] [TauCeti.DGCategory R D] [TauCeti.DGCategory R E] (F : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (G : EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) D E) : (comp (CochainComplex (ModuleCat R) ℤ) F G).mapDGHomotopyCategory ≅ F.mapDGHomotopyCategory.comp G.mapDGHomotopyCategory

H⁰ of a composite of DG functors is the composite of the induced functors.

Equations

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