An A∞ algebra as a right module over itself

An A∞ algebra A is a right A∞ module over itself, the free module of rank one, whose operations are those of the algebra: m_n^A(x, a₁, …, a_{n-1}) = m_n(x, a₁, …, a_{n-1}).

The construction is made on the suspended bar side. Concatenation x ⊗ w ↦ x w, the uncurried TauCeti.TensorWords.prepend, maps the cofree right bar comodule sA ⊗ Tᶜ(sA) to the reduced bar construction ReducedTensorWords R A. The Taylor map of the module is the Taylor map of the algebra read through concatenation. Concatenation then carries the coderivation this Taylor map generates over the bar differential of A to the bar differential of A itself (TauCeti.AInfinityAlgebra.lift_prepend_comp_barDifferential_toRightModule): a block collapsed by the module structure either starts at the module input or lies in the word to its right, and the Koszul twist of the module input is the sign with which the bar differential passes the first letter. The module square-zero law is therefore the square-zero law of the algebra.

Main definitions

• TauCeti.AInfinityAlgebra.toRightModule: an A∞ algebra as a right module over itself.

Main results

• TauCeti.AInfinityAlgebra.lift_prepend_comp_barDifferential_toRightModule: concatenation intertwines the module bar differential with the algebra bar differential.
• TauCeti.AInfinityAlgebra.m_toRightModule: the unsuspended module operations are the algebra operations, with the module input first.
• TauCeti.AInfinityAlgebra.differential_toRightModule: in particular, the module differential is the differential of the algebra.

References

• B. Keller, Introduction to A-infinity algebras and modules, Section 4.1.
• E. Getzler and J. D. S. Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2.

noncomputable def TauCeti.AInfinityAlgebra.toRightModule {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : AInfinityRightModule AA A

An A∞ algebra as a right A∞ module over itself, the free module of rank one. Its Taylor map evaluates the Taylor map of the algebra on the concatenated word x a₁ ⋯ aₙ, so that its operations are the algebra operations (TauCeti.AInfinityAlgebra.m_toRightModule).

Equations

• AA.toRightModule = TauCeti.AInfinityRightModule.ofTaylor AA.grading (AA.taylor ∘ₗ TensorProduct.lift (TauCeti.TensorWords.prepend R A)) ⋯ ⋯

@[simp]

theorem TauCeti.AInfinityAlgebra.toRightModule_grading {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : AA.toRightModule.grading = AA.grading

The free module of rank one carries the grading of the algebra.

theorem TauCeti.AInfinityAlgebra.toRightModule_taylor {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : AA.toRightModule.taylor = AA.taylor ∘ₗ TensorProduct.lift (TensorWords.prepend R A)

The Taylor map of the free module of rank one is the Taylor map of the algebra after concatenation.

theorem TauCeti.AInfinityAlgebra.toRightModule_taylor_tmul {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) (x : A) (w : TensorWords R A) : AA.toRightModule.taylor (x ⊗ₜ[R] w) = AA.taylor (((TensorWords.prepend R A) x) w)

The Taylor map of the free module of rank one on x ⊗ w is the Taylor map of the algebra on the word x w.

theorem TauCeti.AInfinityAlgebra.lift_prepend_comp_barDifferential_toRightModule {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : TensorProduct.lift (TensorWords.prepend R A) ∘ₗ AA.toRightModule.barDifferential = AA.barDifferential ∘ₗ TensorProduct.lift (TensorWords.prepend R A)

Concatenation intertwines the bar differential of the free module of rank one with the bar differential of the algebra: it is a chain map from the cofree bar comodule sA ⊗ Tᶜ(sA) of the module to the reduced bar construction ReducedTensorWords R A of the algebra.

theorem TauCeti.AInfinityAlgebra.m_toRightModule {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) (n : ℕ) (x : A) (a : Fin n → A) : ((AA.toRightModule.m (n + 1)) x) a = (AA.m (n + 1)) (Fin.cons x a)

The operations of the free module of rank one are the operations of the algebra, with the module input first: m_{n+1}^A(x, a₁, …, aₙ) = m_{n+1}(x, a₁, …, aₙ).

@[simp]

theorem TauCeti.AInfinityAlgebra.differential_toRightModule {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] (AA : AInfinityAlgebra R A) : AA.toRightModule.differential = AA.differential

The differential of the free module of rank one is the differential of the algebra.