Closed morphisms and the underlying category of a DG category

Mathlib's ForgetEnrichment regards a morphism of an enriched category as a map from the tensor unit to a Hom object. For a DG category, such a map is exactly a closed morphism of degree zero. This file makes the comparison explicit and sends a closed morphism to its class in H⁰.

The underlying category is used rather than introducing a second category of cocycles. This allows Mathlib's enriched functors and natural transformations to act on closed morphisms without copying their definitions.

References

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

noncomputable def TauCeti.dgClosedHom (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : DGHom R 0 (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y)

The degree-zero component of a morphism in the underlying category of a DG category.

Equations

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

theorem TauCeti.dgClosedHom_def (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : dgClosedHom R f = (ModuleCat.Hom.hom ((CategoryTheory.ForgetEnrichment.homTo (CochainComplex (ModuleCat R) ℤ) f).f 0)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R))).inv) 1)

Extracting a closed morphism evaluates the degree-zero component of the enriched map on the tensor unit.

theorem TauCeti.dgClosedHom_mem_dgCycles (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : dgClosedHom R f ∈ dgCycles R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y)

The degree-zero component of an underlying morphism is closed.

noncomputable def TauCeti.dgClosedHomOf (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) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) X ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) Y

A closed degree-zero morphism, regarded as a morphism in Mathlib's underlying category of the DG enrichment.

Equations

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

@[simp]

theorem TauCeti.dgClosedHom_dgClosedHomOf (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) : dgClosedHom R (dgClosedHomOf R f hf) = f

Extracting the closed morphism from dgClosedHomOf recovers its input.

theorem TauCeti.dgClosedHom_injective (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} : Function.Injective (dgClosedHom R)

Every underlying morphism of a DG category is determined by its closed degree-zero component.

@[simp]

theorem TauCeti.dgClosedHomOf_dgClosedHom (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : dgClosedHomOf R (dgClosedHom R f) ⋯ = f

Constructing an underlying morphism from the closed component of an underlying morphism recovers that morphism.

noncomputable def TauCeti.dgClosedHomEquiv (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) : (X ⟶ Y) ≃ ↥(dgCycles R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y))

Morphisms in Mathlib's underlying category of a DG category are precisely the closed degree-zero morphisms of its Hom complexes.

Equations

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

@[simp]

theorem TauCeti.dgClosedHomEquiv_apply_coe (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : ↑((dgClosedHomEquiv R X Y) f) = dgClosedHom R f

The equivalence from underlying morphisms to cycles evaluates by taking the degree-zero component.

@[simp]

theorem TauCeti.dgClosedHomEquiv_symm_apply (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : ↥(dgCycles R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y))) : (dgClosedHomEquiv R X Y).symm f = dgClosedHomOf R ↑f ⋯

The inverse equivalence constructs the underlying morphism represented by a cocycle.

@[simp]

theorem TauCeti.dgClosedHom_id (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) : dgClosedHom R (CategoryTheory.CategoryStruct.id X) = dgId R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X)

The identity at an object of Mathlib's underlying category has the DG identity as its closed component.

@[simp]

theorem TauCeti.dgClosedHom_comp (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) (g : Y ⟶ Z) : dgClosedHom R (CategoryTheory.CategoryStruct.comp f g) = dgCompZero R (dgClosedHom R f) (dgClosedHom R g)

Composition in the underlying category is DG composition of closed degree-zero morphisms.

@[simp]

theorem TauCeti.dgClosedHomOf_dgId (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : C) : dgClosedHomOf R (dgId R X) ⋯ = CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) X)

The underlying morphism constructed from the DG identity is the identity.

@[simp]

theorem TauCeti.dgClosedHomOf_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) (hf : f ∈ dgCycles R X Y) (hg : g ∈ dgCycles R Y Z) : dgClosedHomOf R (dgCompZero R f g) ⋯ = CategoryTheory.CategoryStruct.comp (dgClosedHomOf R f hf) (dgClosedHomOf R g hg)

The underlying morphism constructed from a composite of cocycles is their composite.

noncomputable def TauCeti.dgClosedToHomotopy (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : CategoryTheory.Functor (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) (DGHomotopyCategory R C)

The canonical functor from closed degree-zero morphisms to their classes in H⁰. It is the identity on the underlying objects.

Equations

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

@[simp]

theorem TauCeti.dgClosedToHomotopy_obj (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C) : (dgClosedToHomotopy R).obj X = DGHomotopyCategory.of R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X)

The quotient functor fixes the objects of the DG category.

@[simp]

theorem TauCeti.dgClosedToHomotopy_map (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : (dgClosedToHomotopy R).map f = DGHomotopyCategory.homOf R (dgClosedHom R f) ⋯

The quotient functor takes an underlying morphism to the class of its closed component.

theorem TauCeti.dgClosedToHomotopy_map_dgClosedHomOf (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) : (dgClosedToHomotopy R).map (dgClosedHomOf R f hf) = DGHomotopyCategory.homOf R f hf

The quotient functor sends a closed morphism to its homotopy class.

instance TauCeti.full_dgClosedToHomotopy (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] : (dgClosedToHomotopy R).Full

Every morphism in H⁰(C) has a representative in the underlying closed category.

theorem TauCeti.dgClosedToHomotopy_map_eq_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f g : X ⟶ Y) : (dgClosedToHomotopy R).map f = (dgClosedToHomotopy R).map g ↔ dgClosedHom R f - dgClosedHom R g ∈ dgBoundaries R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y)

Two underlying closed morphisms have the same class in H⁰ precisely when their difference is a boundary.

theorem TauCeti.dgClosedToHomotopy_map_eq_zero_iff (R : Type v) [CommRing R] {C : Type u} [DGCategory R C] {X Y : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) C} (f : X ⟶ Y) : (dgClosedToHomotopy R).map f = 0 ↔ dgClosedHom R f ∈ dgBoundaries R (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) X) (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) ℤ) Y)

A closed morphism becomes zero in H⁰ exactly when it is a boundary.