Component equations for right A-infinity module morphisms

A morphism f : M ⟶ N of right A∞ modules is stored as a degree-zero map of suspended bar comodules commuting with their bar differentials. This file expands that condition first on a pure bar word and then in the unsuspended components of f, M, N, and the algebra.

For a cut after k of n algebra inputs, the target-module term has sign (-1) ^ (k * (n - k)), while the source-module term has sign (-1) ^ ((k + 1) * (n - k)). The difference records that a morphism component has degree -k and a module operation has degree 1 - k. Terms in which an algebra operation collapses a block carry the same insertion sign as in the module Stasheff equation.

Main results

• TauCeti.AInfinityRightModuleHom.barMap_tmul_of_tprod: the bar map expanded over all cuts.
• TauCeti.AInfinityRightModuleHom.suspendedComponentEquation: the suspended component equation.
• TauCeti.AInfinityRightModuleHom.componentEquation: the full unsuspended component equation on homogeneous inputs.

References

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

theorem TauCeti.AInfinityRightModuleHom.barMap_tmul_of_tprod {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) (n : ℕ) (x : M) (a : Fin n → A) : f.barMap (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ∑ k ∈ Finset.range (n + 1), f.taylor (x ⊗ₜ[R] TensorWords.subword R a 0 k) ⊗ₜ[R] TensorWords.subword R a k (n - k)

On a pure word, the bar map of a module morphism applies its Taylor map to every prefix and retains the corresponding suffix.

theorem TauCeti.AInfinityRightModuleHom.suspendedComponentEquation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) (n : ℕ) (x : M) (a : Fin n → A) : ∑ k ∈ Finset.range (n + 1), NN.taylor (f.taylor (x ⊗ₜ[R] TensorWords.subword R a 0 k) ⊗ₜ[R] TensorWords.subword R a k (n - k)) = ∑ k ∈ Finset.range (n + 1), f.taylor (MM.taylor (x ⊗ₜ[R] TensorWords.subword R a 0 k) ⊗ₜ[R] TensorWords.subword R a k (n - k)) + f.taylor (((MM.grading.shift 1).koszulTwist 1) x ⊗ₜ[R] AA.coaugmentedBarDifferential ((TensorWords.of R A n) ((PiTensorProduct.tprod R) a)))

The suspended component equation on a word with n algebra inputs. The target Taylor map after the morphism bar map equals the morphism Taylor map after the source bar differential.

theorem TauCeti.AInfinityRightModuleHom.componentEquation {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} (f : AInfinityRightModuleHom MM NN) (n : ℕ) {x : M} {e : ℤ} (hx : x ∈ MM.grading.piece e) (d : ℕ → ℤ) (a : ℕ → A) (ha : ∀ i < n, a i ∈ AA.grading.piece (d i)) : (∑ k ∈ Finset.range (n + 1), negOnePowCast R (↑k * (↑n - ↑k)) • ((NN.m (n - k + 1)) (((f.component k) x).evalNat a)).evalNat fun (j : ℕ) => a (k + j)) = (∑ k ∈ Finset.range (n + 1), negOnePowCast R ((↑k + 1) * (↑n - ↑k)) • ((f.component (n - k)) (((MM.m (k + 1)) x).evalNat a)).evalNat fun (j : ℕ) => a (k + j)) + ∑ p ∈ Finset.range n, ∑ s ∈ Finset.Icc 1 (n - p), negOnePowCast R (↑p + 1 + ↑s * (↑n - ↑p - ↑s) + (2 - ↑s) * (e + ∑ i ∈ Finset.range p, d i)) • ((f.component (p + 1 + (n - p - s))) x).evalNat (replaceBlock a p s ((AA.m s).evalNat fun (j : ℕ) => a (p + j)))

The unsuspended module-morphism equation with n algebra inputs. The module input x has degree e, and a 0, …, a (n - 1) have degrees d 0, …, d (n - 1).

The first sum applies a component of f and then an operation of the target module. The second applies an operation of the source module and then a component of f. The final sum applies an algebra operation to a nonempty block before applying a component of f.