Right A-infinity modules: the suspended bar differential

A right A∞ module over an A∞ algebra A is stored on its cofree right bar comodule

sM ⊗ Tᶜ(sA).

Its structure map is a degree-one square-zero coderivation over the bar differential of A. The co-Leibniz law includes the Koszul sign obtained when the algebra bar differential crosses the left comodule factor. Using the coaugmented tensor coalgebra is essential: the empty word records the unary module operation.

This file packages that primary suspended definition. The Taylor map is obtained by applying the coalgebra counit after the bar differential. It is not stored separately: coderivations over a fixed coalgebra operator on a cofree comodule are determined by this component, which gives the extensionality theorem below. The square-zero law can likewise be checked after applying the counit, giving the suspended module Stasheff equation in the form taylor ∘ barDifferential = 0.

Main definitions

• TauCeti.AInfinityRightModule: a right A∞ module in suspended bar form.
• TauCeti.AInfinityRightModule.barGrading: the total grading on sM ⊗ Tᶜ(sA).
• TauCeti.AInfinityRightModule.taylor: the cogenerator component of the module bar differential.
• TauCeti.AInfinityRightModule.ofBarDifferential: construct a module by checking the square-zero law on its Taylor component.

The convention follows Getzler--Jones, A-infinity algebras and the cyclic bar complex, Sections 1--2, and Keller, Introduction to A-infinity algebras and modules, Section 4.

noncomputable def TauCeti.AInfinityRightModule.barGrading {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] (AA : AInfinityAlgebra R A) (G : InternalGrading R M) : InternalGrading R (TensorProduct R M (TensorWords R A))

The total suspended grading on the cofree bar comodule sM ⊗ Tᶜ(sA).

Equations

• TauCeti.AInfinityRightModule.barGrading AA G = (G.shift 1).tensorProduct (TauCeti.TensorWords.grading (AA.grading.shift 1))

@[simp]

theorem TauCeti.AInfinityRightModule.barGrading_piece {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] (AA : AInfinityAlgebra R A) (G : InternalGrading R M) (p : ℤ) : (barGrading AA G).piece p = ((G.shift 1).tensorProduct (TensorWords.grading (AA.grading.shift 1))).piece p

The degree-p part of the bar-comodule grading is the total-degree part of the suspended module grading and the suspended tensor-word grading.

structure TauCeti.AInfinityRightModule {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] : Type (max (max uA uM) uR)

A right A∞ module over AA, stored as a square-zero degree-one coderivation on the cofree right bar comodule sM ⊗ Tᶜ(sA) over the bar coderivation of AA.

The carrier types model suspension by shifting their internal gradings; no new carrier type is introduced. Thus barDifferential acts on M ⊗ Tᶜ(A), while barGrading interprets that carrier as sM ⊗ Tᶜ(sA).

• grading : InternalGrading R M

  The internal cohomological grading of the module carrier.

• barDifferential : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)

  The suspended module bar differential on the cofree right bar comodule.

• isHomogeneous_barDifferential : LinearMap.IsHomogeneous self.barDifferential (barGrading AA self.grading).piece (barGrading AA self.grading).piece 1

  The module bar differential has degree one for the total suspended grading.

• isGradedCoderivation_barDifferential : Comodule.IsGradedCoderivationOver (barGrading AA self.grading) 1 AA.coaugmentedBarDifferential self.barDifferential

  The module bar differential is a coderivation over the algebra bar differential.

• bar_square_zero : self.barDifferential ∘ₗ self.barDifferential = 0

  The module bar differential squares to zero.

noncomputable def TauCeti.AInfinityRightModule.taylor {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) : TensorProduct R M (TensorWords R A) →ₗ[R] M

The Taylor map of a right A∞ module, obtained by applying the tensor-coalgebra counit to the output of its bar differential. On the summand sM ⊗ (sA)^⊗n, this is the suspended arity-n + 1 module operation.

Equations

• MM.taylor = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ MM.barDifferential

theorem TauCeti.AInfinityRightModule.taylor_def {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) : MM.taylor = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ MM.barDifferential

The Taylor map is the counit component of the module bar differential.

@[simp]

theorem TauCeti.AInfinityRightModule.taylor_apply {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) (x : TensorProduct R M (TensorWords R A)) : MM.taylor x = (TensorProduct.rid R M) ((LinearMap.lTensor M CoalgebraStruct.counit) (MM.barDifferential x))

Evaluating the Taylor map means applying the bar differential, then the coalgebra counit, and finally the right unitor.

theorem TauCeti.AInfinityRightModule.isHomogeneous_taylor {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) : LinearMap.IsHomogeneous MM.taylor (barGrading AA MM.grading).piece (MM.grading.shift 1).piece 1

The Taylor map has degree one from the total suspended bar-comodule grading to the suspended module grading.

@[simp]

theorem TauCeti.AInfinityRightModule.barDifferential_sq {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) : MM.barDifferential ∘ₗ MM.barDifferential = 0

The stored module bar differential squares to zero.

@[simp]

theorem TauCeti.AInfinityRightModule.taylor_comp_barDifferential {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (MM : AInfinityRightModule AA M) : MM.taylor ∘ₗ MM.barDifferential = 0

The Taylor component of the square of the module bar differential vanishes. This is the suspended form of all right-module Stasheff identities.

theorem TauCeti.AInfinityRightModule.barDifferential_sq_iff_taylor_comp_eq_zero {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (G : InternalGrading R M) (D : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)) (hD : LinearMap.IsHomogeneous D (barGrading AA G).piece (barGrading AA G).piece 1) (hcod : Comodule.IsGradedCoderivationOver (barGrading AA G) 1 AA.coaugmentedBarDifferential D) : D ∘ₗ D = 0 ↔ (↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D) ∘ₗ D = 0

A degree-one coderivation over the algebra bar differential squares to zero if and only if its Taylor component after one further application vanishes.

noncomputable def TauCeti.AInfinityRightModule.ofBarDifferential {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (G : InternalGrading R M) (D : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)) (hD : LinearMap.IsHomogeneous D (barGrading AA G).piece (barGrading AA G).piece 1) (hcod : Comodule.IsGradedCoderivationOver (barGrading AA G) 1 AA.coaugmentedBarDifferential D) (hsq : (↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D) ∘ₗ D = 0) : AInfinityRightModule AA M

Construct a right A∞ module from a homogeneous coderivation over the algebra bar differential. By cofreeness, it suffices to check the square-zero law on the Taylor component.

Equations

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

@[simp]

theorem TauCeti.AInfinityRightModule.ofBarDifferential_grading {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (G : InternalGrading R M) (D : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)) (hD : LinearMap.IsHomogeneous D (barGrading AA G).piece (barGrading AA G).piece 1) (hcod : Comodule.IsGradedCoderivationOver (barGrading AA G) 1 AA.coaugmentedBarDifferential D) (hsq : (↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D) ∘ₗ D = 0) : (ofBarDifferential G D hD hcod hsq).grading = G

@[simp]

theorem TauCeti.AInfinityRightModule.ofBarDifferential_barDifferential {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (G : InternalGrading R M) (D : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)) (hD : LinearMap.IsHomogeneous D (barGrading AA G).piece (barGrading AA G).piece 1) (hcod : Comodule.IsGradedCoderivationOver (barGrading AA G) 1 AA.coaugmentedBarDifferential D) (hsq : (↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D) ∘ₗ D = 0) : (ofBarDifferential G D hD hcod hsq).barDifferential = D

@[simp]

theorem TauCeti.AInfinityRightModule.ofBarDifferential_taylor {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} (G : InternalGrading R M) (D : TensorProduct R M (TensorWords R A) →ₗ[R] TensorProduct R M (TensorWords R A)) (hD : LinearMap.IsHomogeneous D (barGrading AA G).piece (barGrading AA G).piece 1) (hcod : Comodule.IsGradedCoderivationOver (barGrading AA G) 1 AA.coaugmentedBarDifferential D) (hsq : (↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D) ∘ₗ D = 0) : (ofBarDifferential G D hD hcod hsq).taylor = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M CoalgebraStruct.counit ∘ₗ D

theorem TauCeti.AInfinityRightModule.ext {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} {MM NN : AInfinityRightModule AA M} (hG : MM.grading = NN.grading) (htaylor : MM.taylor = NN.taylor) : MM = NN

Right A∞ modules on a fixed carrier are determined by their grading and Taylor map. In particular, the stored bar differential contains no data beyond its cogenerator component.

theorem TauCeti.AInfinityRightModule.ext_iff {R : Type uR} {A : Type uA} {M : Type uM} [CommRing R] [AddCommGroup A] [Module R A] [AddCommGroup M] [Module R M] {AA : AInfinityAlgebra R A} {MM NN : AInfinityRightModule AA M} : MM = NN ↔ MM.grading = NN.grading ∧ MM.taylor = NN.taylor