DG natural transformations on homotopy categories

A DG natural transformation has closed degree-zero components that commute with every homogeneous arrow. Mathlib's unit-graded GradedNatTrans supplies closed degree-zero components and naturality on all degrees. Passing the components to cohomology gives a natural transformation between the induced functors on H⁰.

Reference

• B. Keller, Deriving DG categories, Section 1.

@[reducible, inline]

abbrev TauCeti.DGNatTrans {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F G : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : Type (max u₁ v)

Closed degree-zero DG natural transformations, using Mathlib's graded enriched natural transformations at the monoidal unit.

Equations

• TauCeti.DGNatTrans F G = TauCeti.UnitGradedNatTrans F G

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

The identity DG natural transformation.

Equations

• TauCeti.DGNatTrans.id F = TauCeti.UnitGradedNatTrans.id F

noncomputable def TauCeti.DGNatTrans.comp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (α : DGNatTrans F G) (β : DGNatTrans G H) : DGNatTrans F H

Composition of DG natural transformations.

Equations

• α.comp β = TauCeti.UnitGradedNatTrans.unitComp α β

@[simp]

theorem TauCeti.DGNatTrans.id_app {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) (X : C) : (id F).app X = CategoryTheory.eId (CochainComplex (ModuleCat R) ℤ) (F.obj X)

The component of the identity DG natural transformation.

@[simp]

theorem TauCeti.DGNatTrans.comp_app {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (α : DGNatTrans F G) (β : DGNatTrans G H) (X : C) : (α.comp β).app X = (CategoryTheory.eHomEquiv (CochainComplex (ModuleCat R) ℤ)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (α.app X)) (CategoryTheory.ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (β.app X)))

The component of a composite DG natural transformation.

structure TauCeti.DGFunctor (R : Type v) [CommRing R] (C : Type u₁) (D : Type u₂) [DGCategory R C] [DGCategory R D] : Type (max (max u₁ u₂) v)

DG functors with closed degree-zero DG natural transformations as morphisms.

• toEnrichedFunctor : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D

  The underlying functor enriched in cochain complexes.

theorem TauCeti.DGFunctor.ext_iff {R : Type v} {inst✝ : CommRing R} {C : Type u₁} {D : Type u₂} {inst✝¹ : DGCategory R C} {inst✝² : DGCategory R D} {x y : DGFunctor R C D} : x = y ↔ x.toEnrichedFunctor = y.toEnrichedFunctor

theorem TauCeti.DGFunctor.ext {R : Type v} {inst✝ : CommRing R} {C : Type u₁} {D : Type u₂} {inst✝¹ : DGCategory R C} {inst✝² : DGCategory R D} {x y : DGFunctor R C D} (toEnrichedFunctor : x.toEnrichedFunctor = y.toEnrichedFunctor) : x = y

@[instance_reducible]

noncomputable instance TauCeti.instCategoryDGFunctor {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] : CategoryTheory.Category.{max u₁ v, max (max u₂ u₁) v} (DGFunctor R C D)

Equations

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

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

The component of a DG natural transformation on the homotopy category is the homotopy class of its closed degree-zero component.

Equations

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

@[simp]

theorem TauCeti.DGNatTrans.mapDGHomotopyCategory_app {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (α : DGNatTrans F G) (X : C) : α.mapDGHomotopyCategory.app (DGHomotopyCategory.of R X) = DGHomotopyCategory.homOf R (dgClosedHom R (CategoryTheory.ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (α.app X))) ⋯

On an object, the induced transformation is the homotopy class of the closed component.

theorem TauCeti.DGNatTrans.mapDGHomotopyCategory_app_eq_zero_iff {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (α : DGNatTrans F G) (X : C) : α.mapDGHomotopyCategory.app (DGHomotopyCategory.of R X) = 0 ↔ dgClosedHom R (CategoryTheory.ForgetEnrichment.homOf (CochainComplex (ModuleCat R) ℤ) (α.app X)) ∈ dgBoundaries R (F.obj X) (G.obj X)

A component of the induced transformation vanishes exactly when the corresponding closed degree-zero DG morphism is a boundary.

@[simp]

theorem TauCeti.DGNatTrans.mapDGHomotopyCategory_id {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D) : (id F).mapDGHomotopyCategory = CategoryTheory.CategoryStruct.id F.mapDGHomotopyCategory

Passing the identity DG transformation to H⁰ gives the identity transformation.

@[simp]

theorem TauCeti.DGNatTrans.mapDGHomotopyCategory_comp {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G H : CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) ℤ) C D} (α : DGNatTrans F G) (β : DGNatTrans G H) : (α.comp β).mapDGHomotopyCategory = CategoryTheory.CategoryStruct.comp α.mapDGHomotopyCategory β.mapDGHomotopyCategory

Passing a composite of DG transformations to H⁰ composes their images.

noncomputable def TauCeti.mapDGHomotopyCategoryFunctor {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] : CategoryTheory.Functor (DGFunctor R C D) (CategoryTheory.Functor (DGHomotopyCategory R C) (DGHomotopyCategory R D))

Taking H⁰ sends DG functors and DG natural transformations to ordinary functors and natural transformations.

Equations

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

@[simp]

theorem TauCeti.mapDGHomotopyCategoryFunctor_obj {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] (F : DGFunctor R C D) : mapDGHomotopyCategoryFunctor.obj F = F.toEnrichedFunctor.mapDGHomotopyCategory

On objects, the functor takes a DG functor to its induced functor on H⁰.

@[simp]

theorem TauCeti.mapDGHomotopyCategoryFunctor_map {R : Type v} [CommRing R] {C : Type u₁} {D : Type u₂} [DGCategory R C] [DGCategory R D] {F G : DGFunctor R C D} (α : F ⟶ G) : mapDGHomotopyCategoryFunctor.map α = DGNatTrans.mapDGHomotopyCategory α

On morphisms, the functor takes a DG transformation to its induced transformation on H⁰.