The differential graded category of curved differential graded right modules

The right modules over a curved differential graded algebra (A, d, w) form a differential graded category. The Hom complex from M to N is TauCeti.curvedDGRightModuleHomComplex, whose degree-p cochains are the right-module maps raising internal degree by p, with the graded commutator f ↦ dN ∘ f - (-1) ^ p f ∘ dM as differential; composition of homogeneous cochains is composition of the underlying maps. An individual curved module has no cohomology in general, since its differential squares to the curvature action rather than to zero, but the Hom differential squares to zero because source and target have the same curvature, and the graded Leibniz rule for composition holds verbatim. This file installs the differential graded structure on the bundled curved right modules TauCeti.CurvedDGRightModuleCat through the explicit Hom-complex data of TauCeti/CategoryTheory/DG/HomComplexData.lean, and identifies its calculus with the cochain calculus: the differential is the graded commutator with the module differentials, the identity is the identity cochain, and composition in Mathlib's enriched factor order is composition of cochains twisted by the Koszul sign (-1) ^ (p * q).

The generic constructions on a differential graded category then supply the closed morphisms and the homotopy category of curved modules. The closed degree-zero morphisms TauCeti.dgCycles are the right-module maps commuting with the differentials; they are the morphisms of the closed degree-zero category, Mathlib's underlying category CategoryTheory.ForgetEnrichment of the enrichment, and this file identifies those morphisms with the zero-cocycles of the curved Hom complex. The degree-zero boundaries TauCeti.dgBoundaries are the maps dN ∘ k + k ∘ dM for an odd homotopy k, a right-module map of degree -1: this is the degree -1 case of the graded commutator, whose Koszul sign (-1) ^ (-1) = -1 turns the subtraction into an addition. The curved homotopy category is TauCeti.DGHomotopyCategory R (CurvedDGRightModuleCat h): it has the curved modules as objects and homotopy classes of closed degree-zero morphisms as morphisms, two closed morphisms being identified exactly when their difference is the boundary of an odd homotopy. No homology enters: a curved module has no cohomology in general, and the homotopy category is the quotient by boundaries alone.

Main definitions

• TauCeti.CurvedDGRightModuleCat.homComplexData: the Hom complexes, composition, and identities of curved differential graded right modules as explicit Hom-complex data.
• TauCeti.CurvedDGRightModuleCat.instDGCategory: the differential graded category of curved differential graded right modules.
• TauCeti.CurvedDGRightModuleCat.dgHomLinearEquivCochains: the explicit identification of homogeneous morphisms with right-module cochains.
• TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles: morphisms of the closed degree-zero category of curved right modules are the zero-cocycles of the curved Hom complex.

Main results

• TauCeti.CurvedDGRightModuleCat.dgDifferential_eq, TauCeti.CurvedDGRightModuleCat.dgId_eq and TauCeti.CurvedDGRightModuleCat.dgComp_eq: the differential graded calculus of the category is the cochain calculus, with the Koszul sign in composition.
• TauCeti.CurvedDGRightModuleCat.mem_dgCycles_iff: the closed degree-zero morphisms are the maps commuting with the module differentials.
• TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles_id and TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles_comp: the identification of closed morphisms with zero-cocycles is functorial.
• TauCeti.CurvedDGRightModuleCat.mem_dgBoundaries_iff: the degree-zero boundaries are the boundaries dN ∘ k + k ∘ dM of odd homotopies.
• TauCeti.CurvedDGRightModuleCat.homOf_eq_iff_exists_homotopy: two closed morphisms agree in the curved homotopy category exactly when they are homotopic through an odd homotopy.

Implementation notes

This module is closely adapted, declaration by declaration, from the uncurved construction in TauCeti/Algebra/Homology/DG/Module/Right/DGCategory.lean: the curved Hom complex and its differential replace the ordinary ones, and the closed degree-zero category is Mathlib's underlying category of the enrichment rather than an independently defined linear category.

As for TauCeti.DGRightModuleCat, the enrichment fixes the universe of the ground ring while the Hom complexes live in the universe of the modules, so the differential graded structure lives on CurvedDGRightModuleCat.{u, u, u} h: ground ring, algebra, and modules share one universe.

References

• L. Positselski, Two kinds of derived categories, Koszul duality, and comodule-contramodule correspondence, Section 3.1, for curved DG modules and their homotopy category.
• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 6.2. His curvature is the negative of the right-module curvature used here.
• B. Keller, Deriving DG categories, Sections 1 and 2, for the differential graded category of modules.

The explicit Hom-complex data

noncomputable def TauCeti.CurvedDGRightModuleCat.homComplexData {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : DGCategoryData R (CurvedDGRightModuleCat h)

The explicit Hom-complex data of the differential graded category of curved right modules over h: the Hom complex from M to N is TauCeti.curvedDGRightModuleHomComplex, composition of homogeneous cochains is composition of the underlying maps, in Keller's order, and the identity is the identity cochain.

Equations

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

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homComplexData_hom {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) : homComplexData.hom M N = curvedDGRightModuleHomComplex ⋯ ⋯

The Hom complex of the explicit data is the curved Hom complex of the two modules.

The differential graded category

@[instance_reducible]

noncomputable instance TauCeti.CurvedDGRightModuleCat.instDGCategory {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} : DGCategory R (CurvedDGRightModuleCat h)

The differential graded category of curved differential graded right modules over h.

Equations

• TauCeti.CurvedDGRightModuleCat.instDGCategory = TauCeti.CurvedDGRightModuleCat.homComplexData.toDGCategory

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgHomComplex_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) : dgHomComplex R M N = curvedDGRightModuleHomComplex ⋯ ⋯

The Hom complex of the differential graded category of curved right modules is the curved Hom complex of the two modules.

noncomputable def TauCeti.CurvedDGRightModuleCat.dgHomLinearEquivCochains {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (n : ℤ) : DGHom R n M N ≃ₗ[R] ↥(dgRightModuleCochains n)

Homogeneous morphisms of the differential graded category, identified with right-module cochains through the equality of their Hom complexes.

Equations

• M.dgHomLinearEquivCochains N n = (CategoryTheory.eqToIso ⋯).toLinearEquiv

theorem TauCeti.CurvedDGRightModuleCat.dgHomLinearEquivCochains_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (n : ℤ) (f : DGHom R n M N) : (M.dgHomLinearEquivCochains N n) f = (ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) f

The identification with cochains acts by transport along the equality of the degree-n terms of the Hom complexes.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homComplexData_comp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N P : CurvedDGRightModuleCat h) {p q n : ℤ} (hpq : p + q = n) (f : DGHom R p M N) (g : DGHom R q N P) : (M.dgHomLinearEquivCochains P n) (((homComplexData.comp p q n hpq) f) g) = (p * q).negOnePow • dgRightModuleCochains.comp ((N.dgHomLinearEquivCochains P q) g) ((M.dgHomLinearEquivCochains N p) f) ⋯

Transported composition in the explicit Hom-complex data is composition of cochains in reversed order, with the Koszul sign converting Keller's factor order into Mathlib's.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homComplexData_id {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M : CurvedDGRightModuleCat h) : (M.dgHomLinearEquivCochains M 0) (homComplexData.id M) = dgRightModuleCochains.id

The transported identity of the explicit data is the identity cochain.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.homComplexData_d_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (n : ℤ) (f : DGHom R n M N) : (M.dgHomLinearEquivCochains N (n + 1)) ((ModuleCat.Hom.hom ((homComplexData.hom M N).d n (n + 1))) f) = (dgRightModuleCochains.curvedDifferential n) ((M.dgHomLinearEquivCochains N n) f)

The transported differential of the explicit data is the graded commutator with the module differentials.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgDifferential_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (n : ℤ) (f : DGHom R n M N) : (M.dgHomLinearEquivCochains N (n + 1)) ((dgDifferential R n) f) = (dgRightModuleCochains.curvedDifferential n) ((M.dgHomLinearEquivCochains N n) f)

The differential of the differential graded category of curved right modules is the graded commutator with the module differentials, after transport to cochains.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgId_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M : CurvedDGRightModuleCat h) : (M.dgHomLinearEquivCochains M 0) (dgId R M) = dgRightModuleCochains.id

The identity of the differential graded category of curved right modules transports to the identity cochain.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgComp_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N P : CurvedDGRightModuleCat h) {p q n : ℤ} (f : DGHom R p M N) (g : DGHom R q N P) (hpq : p + q = n) : (M.dgHomLinearEquivCochains P n) (dgComp R f g hpq) = (p * q).negOnePow • dgRightModuleCochains.comp ((N.dgHomLinearEquivCochains P q) g) ((M.dgHomLinearEquivCochains N p) f) ⋯

Composition in the differential graded category of curved right modules is composition of cochains, carrying the Koszul sign which converts Mathlib's enriched factor order into composition of the underlying maps, after transport to cochains.

The closed degree-zero category

theorem TauCeti.CurvedDGRightModuleCat.dgCycles_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) : dgCycles R M N = Submodule.comap (↑(M.dgHomLinearEquivCochains N 0)) (dgRightModuleCochains.curvedDifferential 0).ker

The closed degree-zero morphisms are the preimage of the zero-cocycles of the curved Hom complex under the explicit identification with cochains.

theorem TauCeti.CurvedDGRightModuleCat.mem_dgCycles_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (f : DGHom R 0 M N) : f ∈ dgCycles R M N ↔ ∀ (x : M.carrier), N.differential (↑((M.dgHomLinearEquivCochains N 0) f) x) = ↑((M.dgHomLinearEquivCochains N 0) f) (M.differential x)

A degree-zero morphism of the differential graded category of curved right modules is closed exactly when its underlying map commutes with the module differentials.

noncomputable def TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) : (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) ≃ ↥(dgRightModuleCochains.curvedDifferential 0).ker

Morphisms of the closed degree-zero category of curved right modules are the zero-cocycles of the curved Hom complex. The closed degree-zero category is Mathlib's underlying category CategoryTheory.ForgetEnrichment of the differential graded enrichment, whose morphisms are the closed degree-zero morphisms TauCeti.dgCycles.

Equations

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

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coe_dgClosedHomEquivZeroCocycles_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) (x : M.carrier) : ↑↑((M.dgClosedHomEquivZeroCocycles N) f) x = ↑((M.dgHomLinearEquivCochains N 0) (dgClosedHom R f)) x

The zero-cocycle attached to a morphism of the closed degree-zero category has the underlying map of its closed degree-zero component.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgClosedHom_dgClosedHomEquivZeroCocycles_symm_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {M N : CurvedDGRightModuleCat h} (f : ↥(dgRightModuleCochains.curvedDifferential 0).ker) : dgClosedHom R ((M.dgClosedHomEquivZeroCocycles N).symm f) = (M.dgHomLinearEquivCochains N 0).symm ↑f

The closed degree-zero component of the morphism attached to a zero-cocycle is the corresponding homogeneous morphism.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles_id {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {M : CurvedDGRightModuleCat h} : ↑((M.dgClosedHomEquivZeroCocycles M) (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M))) = dgRightModuleCochains.id

The identity of the closed degree-zero category corresponds to the identity cochain.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.dgClosedHomEquivZeroCocycles_comp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} {M N P : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P) : ↑((M.dgClosedHomEquivZeroCocycles P) (CategoryTheory.CategoryStruct.comp f g)) = dgRightModuleCochains.comp ↑((N.dgClosedHomEquivZeroCocycles P) g) ↑((M.dgClosedHomEquivZeroCocycles N) f) ⋯

Composition in the closed degree-zero category corresponds to composition of cochains.

Odd homotopies and the curved homotopy category

theorem TauCeti.CurvedDGRightModuleCat.mem_dgBoundaries_iff {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) (f : DGHom R 0 M N) : f ∈ dgBoundaries R M N ↔ ∃ (k : ↥(dgRightModuleCochains (-1))), ∀ (x : M.carrier), ↑((M.dgHomLinearEquivCochains N 0) f) x = N.differential (↑k x) + ↑k (M.differential x)

A degree-zero morphism of the differential graded category of curved right modules is a boundary exactly when its underlying map is the boundary dN ∘ k + k ∘ dM of an odd homotopy k, a right-module map lowering the internal degree by one.

theorem TauCeti.CurvedDGRightModuleCat.homOf_eq_iff_exists_homotopy {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {w : A} {h : IsCurvedDGAlgebra 𝒜 d w} (M N : CurvedDGRightModuleCat h) {f g : DGHom R 0 M N} (hf : f ∈ dgCycles R M N) (hg : g ∈ dgCycles R M N) : DGHomotopyCategory.homOf R f hf = DGHomotopyCategory.homOf R g hg ↔ ∃ (k : ↥(dgRightModuleCochains (-1))), ∀ (x : M.carrier), ↑((M.dgHomLinearEquivCochains N 0) f) x - ↑((M.dgHomLinearEquivCochains N 0) g) x = N.differential (↑k x) + ↑k (M.differential x)

The curved homotopy category. Two closed degree-zero morphisms of curved right modules represent the same morphism of the homotopy category TauCeti.DGHomotopyCategory exactly when they are homotopic: their difference is the boundary dN ∘ k + k ∘ dM of an odd homotopy k.