The category of right A-infinity modules

AInfinityRightModuleCat AA bundles right A∞ modules over a fixed algebra AA. Its morphisms are the existing bar-comodule morphisms AInfinityRightModuleHom, and composition is composition of bar maps. This is the category before taking homotopy classes or inverting quasi-isomorphisms. Its differential graded enrichment is constructed in TauCeti.Algebra.Homology.AInfinity.Module.Right.DGCategory.

The constructor of is an abbreviation so that its carrier is the supplied module type.

References

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

structure TauCeti.AInfinityRightModuleCat {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : Type (max (max uA (uM + 1)) uR)

A bundled right A∞ module over AA.

• carrier : Type uM

  The underlying module carrier.

• addCommGroup : AddCommGroup self.carrier
• moduleBase : Module R self.carrier
• str : AInfinityRightModule AA self.carrier

  The right A∞ module structure on the carrier.

@[instance_reducible]

instance TauCeti.AInfinityRightModuleCat.instCoeSortType {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : CoeSort (AInfinityRightModuleCat AA) (Type uM)

Equations

• TauCeti.AInfinityRightModuleCat.instCoeSortType = { coe := TauCeti.AInfinityRightModuleCat.carrier }

@[reducible, inline]

abbrev TauCeti.AInfinityRightModuleCat.of {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} [AddCommGroup M] [Module R M] (MM : AInfinityRightModule AA M) : AInfinityRightModuleCat AA

Bundle a right A∞ module with its existing module structures.

Equations

• TauCeti.AInfinityRightModuleCat.of MM = { carrier := M, addCommGroup := inst✝¹, moduleBase := inst✝, str := MM }

@[instance_reducible]

noncomputable instance TauCeti.AInfinityRightModuleCat.instCategory {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} : CategoryTheory.Category.{max (max uM uA) uR, max (max uA (uM + 1)) uR} (AInfinityRightModuleCat AA)

Equations

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

theorem TauCeti.AInfinityRightModuleCat.hom_ext {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N : AInfinityRightModuleCat AA} {f g : M ⟶ N} (h : AInfinityRightModuleHom.barMap f = AInfinityRightModuleHom.barMap g) : f = g

Morphisms of bundled modules are determined by their bar maps.

theorem TauCeti.AInfinityRightModuleCat.hom_ext_iff {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N : AInfinityRightModuleCat AA} {f g : M ⟶ N} : f = g ↔ AInfinityRightModuleHom.barMap f = AInfinityRightModuleHom.barMap g

@[simp]

theorem TauCeti.AInfinityRightModuleCat.barMap_id {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} (M : AInfinityRightModuleCat AA) : AInfinityRightModuleHom.barMap (CategoryTheory.CategoryStruct.id M) = LinearMap.id

The bar map of the categorical identity is the identity map.

@[simp]

theorem TauCeti.AInfinityRightModuleCat.barMap_comp {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M N P : AInfinityRightModuleCat AA} (f : M ⟶ N) (g : N ⟶ P) : AInfinityRightModuleHom.barMap (CategoryTheory.CategoryStruct.comp f g) = AInfinityRightModuleHom.barMap g ∘ₗ AInfinityRightModuleHom.barMap f

Categorical composition is composition of the underlying bar maps.