Unsuspended components of right A-infinity module morphisms

A morphism of right A∞ modules is stored as a map of suspended bar comodules. This file unsuspends its Taylor components to maps

f_{n+1}^M : M ⊗ A^⊗n ⟶ N

of cohomological degree -n. The indexing counts algebra inputs: component 0 is the unary linear part. The component is the module-first unsuspension TauCeti.AInfinityRightModule.unsuspend of the suspended Taylor component, the same one used to unsuspend the operations of a right A∞ module.

The suspension formula makes the signs executable on homogeneous elements, while component extensionality lets later constructions work entirely with the unsuspended maps. The expanded morphism equations and composition signs can therefore be stated without exposing bar words.

Main definitions

• TauCeti.AInfinityRightModuleHom.component: the unsuspended component with n algebra inputs.

Main results

• TauCeti.AInfinityRightModuleHom.suspendedComponent_tmul_tprod_of_mem: the suspension sign on homogeneous inputs.
• TauCeti.AInfinityRightModuleHom.component_mem_piece: the component with n algebra inputs has degree -n.
• TauCeti.AInfinityRightModuleHom.ext_component: unsuspended components determine a morphism.

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.

noncomputable def TauCeti.AInfinityRightModuleHom.component {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 : ℕ) : M →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) N

The unsuspended component with n algebra inputs. It has total arity n + 1, with the module input first, and cohomological degree -n.

Equations

• f.component n = TauCeti.AInfinityRightModule.unsuspend MM.grading AA.grading n (f.suspendedComponent n)

theorem TauCeti.AInfinityRightModuleHom.component_apply {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.component n) x) a = (f.suspendedComponent n) ((MM.grading.koszulTwist ↑n) x ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : Fin n) => (AA.grading.koszulTwist (↑n - 1 - ↑↑i)) (a i))

The unsuspended component evaluates the suspended component on Koszul-twisted inputs.

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_tmul_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.suspendedComponent n) (x ⊗ₜ[R] (PiTensorProduct.tprod R) a) = ((f.component n) ((MM.grading.koszulTwist ↑n) x)) fun (i : Fin n) => (AA.grading.koszulTwist (↑n - 1 - ↑↑i)) (a i)

The suspended component evaluates the unsuspended component on Koszul-twisted inputs.

theorem TauCeti.AInfinityRightModuleHom.taylor_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.taylor (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ((f.component n) ((MM.grading.koszulTwist ↑n) x)) fun (i : Fin n) => (AA.grading.koszulTwist (↑n - 1 - ↑↑i)) (a i)

On a pure bar word, the Taylor map evaluates the unsuspended component on Koszul-twisted inputs.

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_tmul_tprod_of_mem {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)) : (f.suspendedComponent n) (x ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : Fin n) => a ↑i) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • ((f.component n) x).evalNat a

On homogeneous inputs, the suspended component is the unsuspended component multiplied by the Koszul sign of suspending the module input and all algebra inputs.

theorem TauCeti.AInfinityRightModuleHom.taylor_tmul_of_tprod_of_mem {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)) : f.taylor (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) fun (i : Fin n) => a ↑i)) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • ((f.component n) x).evalNat a

On homogeneous inputs, the Taylor map is the unsuspended component multiplied by the Koszul sign of suspending the module input and all algebra inputs.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.component_zero_apply {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) (x : M) (a : Fin 0 → A) : ((f.component 0) x) a = f.linearPart x

The component with no algebra inputs is the linear part.

theorem TauCeti.AInfinityRightModuleHom.component_mem_piece {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) (a : Fin n → A) (d : Fin n → ℤ) (ha : ∀ (i : Fin n), a i ∈ AA.grading.piece (d i)) : ((f.component n) x) a ∈ NN.grading.piece (e + ∑ i : Fin n, d i - ↑n)

The component with n algebra inputs has cohomological degree -n.

theorem TauCeti.AInfinityRightModuleHom.ext_component {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 g : AInfinityRightModuleHom MM NN} (h : ∀ (n : ℕ), f.component n = g.component n) : f = g

Two module morphisms are equal when all their unsuspended components agree.

theorem TauCeti.AInfinityRightModuleHom.ext_component_iff {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 g : AInfinityRightModuleHom MM NN} : f = g ↔ ∀ (n : ℕ), f.component n = g.component n

@[simp]

theorem TauCeti.AInfinityRightModuleHom.component_id_of_pos {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) {n : ℕ} (hn : 0 < n) : (AInfinityRightModuleHom.id MM).component n = 0

The identity morphism has zero unsuspended components with a positive number of algebra inputs.