The differential graded category of differential graded right modules

The right modules over a differential graded algebra form a differential graded category: the Hom complex from M to N is TauCeti.dgRightModuleHomComplex, whose degree-p cochains are the right-module maps raising internal degree by p, and composition of homogeneous cochains is composition of the underlying maps. This file installs that structure on the bundled category TauCeti.DGRightModuleCat through the explicit Hom-complex data of TauCeti/CategoryTheory/DG/HomComplexData.lean, and identifies the resulting differential graded calculus with the cochain calculus already available: 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 closed degree-zero morphisms of this differential graded category are exactly the morphisms of the linear category TauCeti.DGRightModuleCat, compatibly with identities and composition. Thus the ordinary category of differential graded modules is the Z⁰ category of the differential graded one, and its homotopy category is the H⁰ category TauCeti.DGHomotopyCategory of the differential graded one.

Main definitions

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

Main results

• TauCeti.DGRightModuleCat.dgDifferential_eq, TauCeti.DGRightModuleCat.dgId_eq and TauCeti.DGRightModuleCat.dgComp_eq: the differential graded calculus of the category is the cochain calculus, with the Koszul sign in composition.
• TauCeti.DGRightModuleCat.homLinearEquivDGCycles_id and TauCeti.DGRightModuleCat.homLinearEquivDGCycles_comp: the identification of morphisms with closed degree-zero morphisms is functorial.

Implementation notes

The Hom complex between two modules has its terms in the universe of the modules, while the enrichment fixes the universe of the ground ring, so the differential graded structure lives on DGRightModuleCat.{u, u, u} h: ground ring, algebra, and modules share one universe. The composition and identity cochains of TauCeti/Algebra/Homology/DG/Module/Right/Composition.lean are stated in that generality as well.

The linear equivalence dgHomLinearEquivCochains identifies homogeneous morphisms with right-module cochains. Under this identification, the differential is the graded commutator, the identity is the identity cochain, and composition carries the Koszul sign.

References

• B. Keller, Deriving DG categories, Sections 1 and 2.
• B. Keller, Introduction to A-infinity algebras and modules, Section 3.1.

The explicit Hom-complex data

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

The explicit Hom-complex data of the differential graded category of right modules over h: the Hom complex from M to N is TauCeti.dgRightModuleHomComplex, 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.DGRightModuleCat.homComplexData_hom {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N : DGRightModuleCat h) : homComplexData.hom M N = dgRightModuleHomComplex ⋯ ⋯

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

The differential graded category

@[instance_reducible]

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

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

Equations

• TauCeti.DGRightModuleCat.instDGCategory = TauCeti.DGRightModuleCat.homComplexData.toDGCategory

@[simp]

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

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

noncomputable def TauCeti.DGRightModuleCat.dgHomLinearEquivCochains {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N : DGRightModuleCat 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.DGRightModuleCat.dgHomLinearEquivCochains_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N : DGRightModuleCat 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.DGRightModuleCat.homComplexData_comp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N P : DGRightModuleCat 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.DGRightModuleCat.homComplexData_id {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M : DGRightModuleCat h) : (M.dgHomLinearEquivCochains M 0) (homComplexData.id M) = dgRightModuleCochains.id

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

@[simp]

theorem TauCeti.DGRightModuleCat.homComplexData_d_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N : DGRightModuleCat 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.differential n) ((M.dgHomLinearEquivCochains N n) f)

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem TauCeti.DGRightModuleCat.dgComp_eq {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N P : DGRightModuleCat 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 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.

Closed degree-zero morphisms

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

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

noncomputable def TauCeti.DGRightModuleCat.homLinearEquivDGCycles {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} (M N : DGRightModuleCat h) : (M ⟶ N) ≃ₗ[R] ↥(dgCycles R M N)

Morphisms of differential graded right modules are the closed degree-zero morphisms of the differential graded category of right modules.

Equations

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

@[simp]

theorem TauCeti.DGRightModuleCat.coe_homLinearEquivDGCycles_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {M N : DGRightModuleCat h} (f : M ⟶ N) (x : M.carrier) : ↑((M.dgHomLinearEquivCochains N 0) ↑((M.homLinearEquivDGCycles N) f)) x = f x

The closed degree-zero morphism attached to a morphism of differential graded right modules has the same underlying map.

@[simp]

theorem TauCeti.DGRightModuleCat.homLinearEquivDGCycles_symm_apply {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {M N : DGRightModuleCat h} (f : ↥(dgCycles R M N)) (x : M.carrier) : ((M.homLinearEquivDGCycles N).symm f) x = ↑((M.dgHomLinearEquivCochains N 0) ↑f) x

The morphism of differential graded right modules attached to a closed degree-zero morphism has the same underlying map.

@[simp]

theorem TauCeti.DGRightModuleCat.homLinearEquivDGCycles_id {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {M : DGRightModuleCat h} : ↑((M.homLinearEquivDGCycles M) (CategoryTheory.CategoryStruct.id M)) = dgId R M

The identity morphism corresponds to the identity of the differential graded category.

@[simp]

theorem TauCeti.DGRightModuleCat.homLinearEquivDGCycles_comp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {𝒜 : ℤ → Submodule R A} [GradedAlgebra 𝒜] {d : A →ₗ[R] A} {h : IsDGAlgebra 𝒜 d} {M N P : DGRightModuleCat h} (f : M ⟶ N) (g : N ⟶ P) : (M.homLinearEquivDGCycles P) (CategoryTheory.CategoryStruct.comp f g) = ((dgCyclesComp R M N P) ((M.homLinearEquivDGCycles N) f)) ((N.homLinearEquivDGCycles P) g)

Composition of morphisms corresponds to composition of closed degree-zero morphisms in the differential graded category.