The differential graded category of right A-infinity modules

Right A∞ modules over a fixed algebra form a DG category. Its Hom complexes are the homogeneous maps of cofree bar comodules, with differential the graded commutator with the module bar differentials. The existing cochain composition and Leibniz rule supply the enrichment through DGCategoryData.ofKeller.

The homogeneous calculus agrees with the cochain calculus. In Mathlib's enriched factor order, composition of degrees p and q is (-1)^(p*q) times composition of bar maps in reversed order. The closed degree-zero morphisms are exactly AInfinityRightModuleHom, compatibly with identities and composition. The resulting functor from bundled modules to Mathlib's underlying category of the enrichment is full and faithful.

The functor toClosedCategory exposes its object map so that the types of its target morphisms reduce to those of the original objects of the enrichment.

Bundling allows independent universes for the base, algebra, and modules. The DG enrichment uses a common universe, as required by DGCategoryData and its ModuleCat R Hom complexes.

The construction and transport interface follow TauCeti.Algebra.Homology.DG.Module.Right.DGCategory.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.

noncomputable def TauCeti.AInfinityRightModuleCat.homComplexData {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : DGCategoryData R (AInfinityRightModuleCat AA)

The Hom complexes and Keller-ordered cochain composition of right A∞ modules, converted to Mathlib's enriched factor order.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleCat.homComplexData_hom {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) : homComplexData.hom M N = M.str.homComplex N.str

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

@[instance_reducible]

noncomputable instance TauCeti.AInfinityRightModuleCat.instDGCategory {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : DGCategory R (AInfinityRightModuleCat AA)

The differential graded enrichment of right A∞ modules over AA.

Equations

• TauCeti.AInfinityRightModuleCat.instDGCategory = TauCeti.AInfinityRightModuleCat.homComplexData.toDGCategory

@[simp]

theorem TauCeti.AInfinityRightModuleCat.dgHomComplex_eq {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) : dgHomComplex R M N = M.str.homComplex N.str

The enriched Hom complex is the module morphism complex.

noncomputable def TauCeti.AInfinityRightModuleCat.dgHomLinearEquivCochains {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) (n : ℤ) : DGHom R n M N ≃ₗ[R] ↥(M.str.homCochains N.str n)

Homogeneous DG morphisms identified with homogeneous bar-comodule maps.

Equations

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

theorem TauCeti.AInfinityRightModuleCat.dgHomLinearEquivCochains_apply {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) (n : ℤ) (f : DGHom R n M N) : (M.dgHomLinearEquivCochains N n) f = (ModuleCat.Hom.hom (CategoryTheory.eqToHom ⋯)) f

The identification with cochains transports along the equality of Hom complexes.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.dgDifferential_eq {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) (n : ℤ) (f : DGHom R n M N) : (M.dgHomLinearEquivCochains N (n + 1)) ((dgDifferential R n) f) = (M.str.homDifferential N.str n) ((M.dgHomLinearEquivCochains N n) f)

The differential transports to the graded commutator with the module bar differentials.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.dgId_eq {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M : AInfinityRightModuleCat AA) : (M.dgHomLinearEquivCochains M 0) (dgId R M) = AInfinityRightModule.homCochains.id M.str

The DG identity transports to the identity cochain.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.dgComp_eq {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N P : AInfinityRightModuleCat AA) {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 • ((AInfinityRightModule.homCochains.comp ⋯) ((N.dgHomLinearEquivCochains P q) g)) ((M.dgHomLinearEquivCochains N p) f)

DG composition transports to composition of cochains with the enriched-order Koszul sign.

theorem TauCeti.AInfinityRightModuleCat.dgCycles_eq {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) : dgCycles R M N = Submodule.comap (↑(M.dgHomLinearEquivCochains N 0)) (M.str.homDifferential N.str 0).ker

DG cycles correspond to the kernel of the cochain differential.

noncomputable def TauCeti.AInfinityRightModuleCat.homEquivDGCycles {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M N : AInfinityRightModuleCat AA) : (M ⟶ N) ≃ ↥(dgCycles R M N)

Module morphisms are exactly the closed degree-zero morphisms of the DG enrichment.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleCat.coe_homEquivDGCycles_apply {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N : AInfinityRightModuleCat AA} (f : M ⟶ N) : ↑((M.dgHomLinearEquivCochains N 0) ↑((M.homEquivDGCycles N) f)) = AInfinityRightModuleHom.barMap f

The cycle associated to a module morphism has its original bar map.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.barMap_homEquivDGCycles_symm {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N : AInfinityRightModuleCat AA} (f : ↥(dgCycles R M N)) : AInfinityRightModuleHom.barMap ((M.homEquivDGCycles N).symm f) = ↑((M.dgHomLinearEquivCochains N 0) ↑f)

The morphism associated to a DG cycle has the cycle's bar map.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.homEquivDGCycles_id {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : AInfinityRightModuleCat AA} : ↑((M.homEquivDGCycles M) (CategoryTheory.CategoryStruct.id M)) = dgId R M

The categorical identity corresponds to the DG identity.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.homEquivDGCycles_comp {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N P : AInfinityRightModuleCat AA} (f : M ⟶ N) (g : N ⟶ P) : (M.homEquivDGCycles P) (CategoryTheory.CategoryStruct.comp f g) = ((dgCyclesComp R M N P) ((M.homEquivDGCycles N) f)) ((N.homEquivDGCycles P) g)

Composition of module morphisms corresponds to composition of DG cycles.

noncomputable def TauCeti.AInfinityRightModuleCat.toClosedCategory {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : CategoryTheory.Functor (AInfinityRightModuleCat AA) (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (AInfinityRightModuleCat AA))

Identify module morphisms with the underlying morphisms of the DG enrichment.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModuleCat.toClosedCategory_obj {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M : AInfinityRightModuleCat AA) : (toClosedCategory AA).obj M = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M

The comparison functor preserves the underlying module object.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.dgClosedHom_toClosedCategory_map {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N : AInfinityRightModuleCat AA} (f : M ⟶ N) : dgClosedHom R ((toClosedCategory AA).map f) = ↑((M.homEquivDGCycles N) f)

Extracting the closed component recovers the cycle associated to the module morphism.

instance TauCeti.AInfinityRightModuleCat.instFaithfulForgetEnrichmentCochainComplexModuleCatIntToClosedCategory {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : (toClosedCategory AA).Faithful

instance TauCeti.AInfinityRightModuleCat.instFullForgetEnrichmentCochainComplexModuleCatIntToClosedCategory {R A : Type u} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : (toClosedCategory AA).Full