The homotopy category of a differential graded category

For a differential graded category C, the morphisms in its homotopy category are the degree-zero cocycles in each Hom complex, modulo the degree-zero coboundaries. Composition is induced by differential graded composition. The Leibniz rule shows that composing a boundary with a cycle on either side is again a boundary, so composition descends to cohomology classes.

This file uses Mathlib's canonical homology object for that quotient. It records the concrete criterion that two closed degree-zero morphisms determine the same morphism precisely when their difference is the differential of a degree-minus-one morphism, and that a chain map between Hom complexes acts on homotopy classes through representatives. The resulting category is naturally preadditive and linear over the ground ring.

Main definitions

• TauCeti.dgCycles: the degree-zero cocycles in a DG Hom complex.
• TauCeti.dgBoundaries: the degree-zero coboundaries in a DG Hom complex.
• TauCeti.DGHomotopyClass: the canonical degree-zero homology of a DG Hom complex.
• TauCeti.dgHomotopyComp: composition of homotopy classes.
• TauCeti.DGHomotopyCategory: the category with the objects of a DG category and morphisms given by DGHomotopyClass.

Main results

• TauCeti.dgHomotopyClass_eq_iff: two cocycles have the same class exactly when their difference is a coboundary.
• TauCeti.dgHomotopyClass_eq_homologyπ: a homotopy class is the image of any lifting cycle under Mathlib's HomologicalComplex.homologyπ.
• TauCeti.homologyMap_dgHomotopyClass: a chain map of Hom complexes sends the class of f to the class of the image of f.

References

• B. Keller, Deriving DG categories, Section 1.
• V. Drinfeld, DG quotients of DG categories, Section 2.
• TauCeti.Algebra.Homology.AInfinity.Algebra.Cohomology, the formal template for the quotient construction and descended bilinear operation.

Cycles, boundaries, and homotopy classes

noncomputable def TauCeti.dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : Submodule R (DGHom R 0 X Y)

The degree-zero cocycles in the Hom complex from X to Y.

Equations

• TauCeti.dgCycles R X Y = (TauCeti.dgDifferential R 0).ker

@[simp]

theorem TauCeti.mem_dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f : DGHom R 0 X Y} : f ∈ dgCycles R X Y ↔ (dgDifferential R 0) f = 0

A degree-zero morphism is a cocycle exactly when its differential vanishes.

noncomputable def TauCeti.dgBoundaries (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : Submodule R (DGHom R 0 X Y)

The degree-zero coboundaries in the Hom complex from X to Y.

Equations

• TauCeti.dgBoundaries R X Y = (TauCeti.dgDifferential R (-1)).range

@[simp]

theorem TauCeti.mem_dgBoundaries (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f : DGHom R 0 X Y} : f ∈ dgBoundaries R X Y ↔ ∃ (h : DGHom R (-1) X Y), (dgDifferential R (-1)) h = f

A degree-zero morphism is a coboundary exactly when it is the differential of a degree-minus-one morphism.

theorem TauCeti.dgBoundaries_le_dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : dgBoundaries R X Y ≤ dgCycles R X Y

Every degree-zero coboundary is a cocycle.

@[reducible, inline]

noncomputable abbrev TauCeti.DGHomotopyClass (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : ModuleCat R

A morphism in H⁰(C), using the canonical Mathlib homology object of the DG Hom complex.

Equations

• TauCeti.DGHomotopyClass R X Y = HomologicalComplex.homology (TauCeti.dgHomComplex R X Y) 0

noncomputable def TauCeti.dgHomotopyClassLinearMap (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : ↥(dgCycles R X Y) →ₗ[R] ↑(DGHomotopyClass R X Y)

The linear quotient map from degree-zero cocycles to homotopy classes.

Equations

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

noncomputable def TauCeti.dgHomotopyClass (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) : ↑(DGHomotopyClass R X Y)

The homotopy class represented by a closed degree-zero morphism.

Equations

• TauCeti.dgHomotopyClass R f hf = (TauCeti.dgHomotopyClassLinearMap R X Y) ⟨f, hf⟩

@[simp]

theorem TauCeti.dgHomotopyClass_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : dgHomotopyClass R 0 ⋯ = 0

Zero represents zero as a homotopy class.

@[simp]

theorem TauCeti.dgHomotopyClass_add (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (f g : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R X Y) : dgHomotopyClass R (f + g) ⋯ = dgHomotopyClass R f hf + dgHomotopyClass R g hg

The class of a sum of cocycles is the sum of their classes.

@[simp]

theorem TauCeti.dgHomotopyClass_smul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (r : R) (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) : dgHomotopyClass R (r • f) ⋯ = r • dgHomotopyClass R f hf

The class of a scalar multiple of a cocycle is the scalar multiple of its class.

theorem TauCeti.exists_dgHomotopyClass_eq (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (c : ↑(DGHomotopyClass R X Y)) : ∃ (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y), dgHomotopyClass R f hf = c

Every homotopy class has a closed degree-zero representative.

@[simp]

theorem TauCeti.dgHomotopyClass_eq_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f g : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R X Y) : dgHomotopyClass R f hf = dgHomotopyClass R g hg ↔ f - g ∈ dgBoundaries R X Y

Two closed degree-zero morphisms represent the same homotopy class exactly when their difference is a coboundary.

@[simp]

theorem TauCeti.dgHomotopyClass_eq_zero_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) : dgHomotopyClass R f hf = 0 ↔ f ∈ dgBoundaries R X Y

A closed degree-zero morphism represents zero exactly when it is a coboundary.

Comparison with Mathlib's homology projection

theorem TauCeti.dgHomotopyClass_eq_homologyπ (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) (x : ↑(HomologicalComplex.cycles (dgHomComplex R X Y) 0)) (hx : (ModuleCat.Hom.hom (HomologicalComplex.iCycles (dgHomComplex R X Y) 0)) x = f) : dgHomotopyClass R f hf = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ (dgHomComplex R X Y) 0)) x

The homotopy class of a closed degree-zero morphism f is the image, under Mathlib's projection HomologicalComplex.homologyπ from cycles to homology, of any cycle lifting f.

theorem TauCeti.map_mem_dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {C' : Type u_1} [DGCategory R C'] {X Y : C} {X' Y' : C'} (φ : dgHomComplex R X Y ⟶ dgHomComplex R X' Y') {f : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) : (ModuleCat.Hom.hom (φ.f 0)) f ∈ dgCycles R X' Y'

A closed degree-zero morphism stays closed under a chain map of Hom complexes.

@[simp]

theorem TauCeti.homologyMap_dgHomotopyClass (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {C' : Type u_1} [DGCategory R C'] {X Y : C} {X' Y' : C'} (φ : dgHomComplex R X Y ⟶ dgHomComplex R X' Y') {f : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap φ 0)) (dgHomotopyClass R f hf) = dgHomotopyClass R ((ModuleCat.Hom.hom (φ.f 0)) f) ⋯

The map induced on homotopy classes by a chain map of Hom complexes sends the class of a closed degree-zero morphism to the class of its image.

Composition on homotopy classes

noncomputable def TauCeti.dgCompZero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) : DGHom R 0 X Z

Composition of two degree-zero DG morphisms.

Equations

• TauCeti.dgCompZero R f g = TauCeti.dgComp R f g TauCeti.dgCompZero._proof_1✝

theorem TauCeti.dgCompZero_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) : dgCompZero R f g = dgComp R f g ⋯

Composition of degree-zero DG morphisms is homogeneous DG composition in degree zero.

@[simp]

theorem TauCeti.add_dgCompZero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f f' : DGHom R 0 X Y) (g : DGHom R 0 Y Z) : dgCompZero R (f + f') g = dgCompZero R f g + dgCompZero R f' g

Composition of degree-zero DG morphisms is additive in its first argument.

@[simp]

theorem TauCeti.smul_dgCompZero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (r : R) (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) : dgCompZero R (r • f) g = r • dgCompZero R f g

Composition of degree-zero DG morphisms respects scalar multiplication in its first argument.

@[simp]

theorem TauCeti.dgCompZero_add (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : DGHom R 0 X Y) (g g' : DGHom R 0 Y Z) : dgCompZero R f (g + g') = dgCompZero R f g + dgCompZero R f g'

Composition of degree-zero DG morphisms is additive in its second argument.

@[simp]

theorem TauCeti.dgCompZero_smul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (r : R) (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) : dgCompZero R f (r • g) = r • dgCompZero R f g

Composition of degree-zero DG morphisms respects scalar multiplication in its second argument.

theorem TauCeti.dgCompZero_mem_dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {f : DGHom R 0 X Y} {g : DGHom R 0 Y Z} (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R Y Z) : dgCompZero R f g ∈ dgCycles R X Z

The composite of two degree-zero cocycles is a degree-zero cocycle.

theorem TauCeti.dgCompZero_mem_dgBoundaries_of_left (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {f : DGHom R 0 X Y} {g : DGHom R 0 Y Z} (hf : f ∈ dgBoundaries R X Y) (hg : g ∈ dgCycles R Y Z) : dgCompZero R f g ∈ dgBoundaries R X Z

Composing a degree-zero boundary on the left with a degree-zero cocycle gives a boundary.

theorem TauCeti.dgCompZero_mem_dgBoundaries_of_right (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} {f : DGHom R 0 X Y} {g : DGHom R 0 Y Z} (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgBoundaries R Y Z) : dgCompZero R f g ∈ dgBoundaries R X Z

Composing a degree-zero cocycle on the left with a degree-zero boundary gives a boundary.

noncomputable def TauCeti.dgCyclesComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) : ↥(dgCycles R X Y) →ₗ[R] ↥(dgCycles R Y Z) →ₗ[R] ↥(dgCycles R X Z)

Composition restricted to degree-zero cocycles.

Equations

• TauCeti.dgCyclesComp R X Y Z = LinearMap.mk₂ R (fun (f : ↥(TauCeti.dgCycles R X Y)) (g : ↥(TauCeti.dgCycles R Y Z)) => ⟨TauCeti.dgCompZero R ↑f ↑g, ⋯⟩) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.coe_dgCyclesComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : ↥(dgCycles R X Y)) (g : ↥(dgCycles R Y Z)) : ↑(((dgCyclesComp R X Y Z) f) g) = dgCompZero R ↑f ↑g

The underlying morphism of the composite of two cocycles is their DG composition.

noncomputable def TauCeti.dgHomotopyComp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y Z : C) : ↑(DGHomotopyClass R X Y) →ₗ[R] ↑(DGHomotopyClass R Y Z) →ₗ[R] ↑(DGHomotopyClass R X Z)

The bilinear composition of homotopy classes induced by DG composition.

Equations

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

@[simp]

theorem TauCeti.dgHomotopyComp_dgHomotopyClass (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R Y Z) : ((dgHomotopyComp R X Y Z) (dgHomotopyClass R f hf)) (dgHomotopyClass R g hg) = dgHomotopyClass R (dgCompZero R f g) ⋯

The composite of classes is represented by the DG composite of their representatives.

theorem TauCeti.dgHomotopyComp_assoc (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {W X Y Z : C} (f : ↑(DGHomotopyClass R W X)) (g : ↑(DGHomotopyClass R X Y)) (h : ↑(DGHomotopyClass R Y Z)) : ((dgHomotopyComp R W Y Z) (((dgHomotopyComp R W X Y) f) g)) h = ((dgHomotopyComp R W X Z) f) (((dgHomotopyComp R X Y Z) g) h)

Composition of homotopy classes is associative.

The category H⁰(C)

structure TauCeti.DGHomotopyCategory (R : Type v) (C : Type u) : Type u

The homotopy category of a differential graded category. It has the same objects as C and the zeroth cohomology of each DG Hom complex as its morphisms.

• obj : C

  The underlying object of the differential graded category.

def TauCeti.DGHomotopyCategory.of (R : Type v) {C : Type u} (X : C) : DGHomotopyCategory R C

Regard an object of a DG category as an object of its homotopy category.

Equations

• TauCeti.DGHomotopyCategory.of R X = { obj := X }

def TauCeti.DGHomotopyCategory.underlying (R : Type v) {C : Type u} (X : DGHomotopyCategory R C) : C

Regard an object of a DG homotopy category as an object of the underlying DG category.

Equations

• TauCeti.DGHomotopyCategory.underlying R X = X.obj

@[simp]

theorem TauCeti.DGHomotopyCategory.underlying_of (R : Type v) {C : Type u} (X : C) : underlying R (of R X) = X

@[simp]

theorem TauCeti.DGHomotopyCategory.of_underlying (R : Type v) {C : Type u} (X : DGHomotopyCategory R C) : of R (underlying R X) = X

theorem TauCeti.DGHomotopyCategory.ext (R : Type v) {C : Type u} {X Y : DGHomotopyCategory R C} (h : underlying R X = underlying R Y) : X = Y

Objects of the DG homotopy category are equal when their underlying DG objects are equal.

theorem TauCeti.DGHomotopyCategory.ext_iff {R : Type v} {C : Type u} {X Y : DGHomotopyCategory R C} : X = Y ↔ underlying R X = underlying R Y

@[instance_reducible]

instance TauCeti.DGHomotopyCategory.instQuiver (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : Quiver (DGHomotopyCategory R C)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DGHomotopyCategory.instCategory (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.Category.{v, u} (DGHomotopyCategory R C)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DGHomotopyCategory.instPreadditive (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.Preadditive (DGHomotopyCategory R C)

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.DGHomotopyCategory.instLinear (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.Linear R (DGHomotopyCategory R C)

Equations

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

theorem TauCeti.DGHomotopyCategory.comp_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : DGHomotopyCategory R C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = ((dgHomotopyComp R (underlying R X) (underlying R Y) (underlying R Z)) f) g

Composition in the homotopy category is the composition TauCeti.dgHomotopyComp of homotopy classes.

theorem TauCeti.DGHomotopyCategory.id_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : DGHomotopyCategory R C) : CategoryTheory.CategoryStruct.id X = dgHomotopyClass R (dgId R (underlying R X)) ⋯

The identity of the homotopy category is the homotopy class of the DG identity.

noncomputable def TauCeti.DGHomotopyCategory.homOf (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) : of R X ⟶ of R Y

A closed degree-zero DG morphism, regarded as a morphism in the homotopy category.

Equations

• TauCeti.DGHomotopyCategory.homOf R f hf = TauCeti.dgHomotopyClass R f hf

theorem TauCeti.DGHomotopyCategory.homOf_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) : homOf R f hf = dgHomotopyClass R f hf

A closed degree-zero DG morphism, regarded in the homotopy category, is its homotopy class.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_zero (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : C) : homOf R 0 ⋯ = 0

The zero DG morphism represents the zero morphism in the homotopy category.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_add (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (f g : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R X Y) : homOf R (f + g) ⋯ = homOf R f hf + homOf R g hg

Taking a morphism to the homotopy category preserves addition.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_smul (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} (r : R) (f : DGHom R 0 X Y) (hf : f ∈ dgCycles R X Y) : homOf R (r • f) ⋯ = r • homOf R f hf

Taking a morphism to the homotopy category preserves scalar multiplication.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_eq_zero_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) : homOf R f hf = 0 ↔ f ∈ dgBoundaries R X Y

A closed degree-zero DG morphism represents zero precisely when it is a boundary.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : homOf R (dgId R X) ⋯ = CategoryTheory.CategoryStruct.id (of R X)

The DG identity represents the identity in the homotopy category.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_eq_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : C} {f g : DGHom R 0 X Y} (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R X Y) : homOf R f hf = homOf R g hg ↔ f - g ∈ dgBoundaries R X Y

Two closed degree-zero DG morphisms define the same morphism in the homotopy category exactly when their difference is a coboundary.

@[simp]

theorem TauCeti.DGHomotopyCategory.homOf_comp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : C} (f : DGHom R 0 X Y) (g : DGHom R 0 Y Z) (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R Y Z) : CategoryTheory.CategoryStruct.comp (homOf R f hf) (homOf R g hg) = homOf R (dgCompZero R f g) ⋯

Composition in the homotopy category is represented by DG composition.