Taylor components of right A-infinity module morphisms

The suspended component with n algebra inputs is the restriction of the Taylor map to sM ⊗ (sA)^⊗n. Each component has degree zero. The component with no algebra inputs is the linear part; it preserves the unsuspended degree and is a chain map for the unary operations. Its identity and composition formulas allow cohomology maps to be defined from module morphisms.

The indexing counts algebra inputs, so suspendedComponent 0 is the arity-one component, not a junk arity-zero value. Cofreeness and the direct sum by word length make all these components together determine the morphism.

References

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

noncomputable def TauCeti.AInfinityRightModuleHom.suspendedComponent {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 : ℕ) : TensorProduct R M (TensorPower R n A) →ₗ[R] N

The suspended Taylor component with n algebra inputs (total arity n + 1).

Equations

• f.suspendedComponent n = f.taylor ∘ₗ LinearMap.lTensor M (TauCeti.TensorWords.of R A n)

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_def {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 : ℕ) : f.suspendedComponent n = f.taylor ∘ₗ LinearMap.lTensor M (TensorWords.of R A n)

The component is the Taylor map after the inclusion of words of the given length.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_tmul {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) (w : TensorPower R n A) : (f.suspendedComponent n) (x ⊗ₜ[R] w) = f.taylor (x ⊗ₜ[R] (TensorWords.of R A n) w)

Restricting the Taylor map to words of length n gives its component of total arity n + 1.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_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).suspendedComponent n = 0

The identity module morphism has no component with a positive number of algebra inputs.

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_tmul_tprod_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} {p : ℤ} (hx : x ∈ (MM.grading.shift 1).piece p) (a : Fin n → A) (d : Fin n → ℤ) (ha : ∀ (i : Fin n), a i ∈ (AA.grading.shift 1).piece (d i)) : (f.suspendedComponent n) (x ⊗ₜ[R] (PiTensorProduct.tprod R) a) ∈ (NN.grading.shift 1).piece (p + ∑ i : Fin n, d i)

Each suspended component has degree zero.

theorem TauCeti.AInfinityRightModuleHom.ext_suspendedComponent {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.suspendedComponent n = g.suspendedComponent n) : f = g

All suspended arity components together determine a module morphism.

theorem TauCeti.AInfinityRightModuleHom.ext_suspendedComponent_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.suspendedComponent n = g.suspendedComponent n

noncomputable def TauCeti.AInfinityRightModuleHom.linearPart {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) : M →ₗ[R] N

The linear part is the arity-one Taylor component, evaluated on the empty algebra word.

Equations

• f.linearPart = f.taylor ∘ₗ (TensorProduct.mk R M (TauCeti.TensorWords R A)).flip 1

@[simp]

theorem TauCeti.AInfinityRightModuleHom.linearPart_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) : f.linearPart x = f.taylor (x ⊗ₜ[R] 1)

@[simp]

theorem TauCeti.AInfinityRightModuleHom.suspendedComponent_zero_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) (x : M) (a : Fin 0 → A) : (f.suspendedComponent 0) (x ⊗ₜ[R] (PiTensorProduct.tprod R) a) = f.linearPart x

The component with no algebra inputs is exactly the linear part.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.barMap_tmul_one {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) : f.barMap (x ⊗ₜ[R] 1) = f.linearPart x ⊗ₜ[R] 1

A comodule morphism sends an empty algebra word to another empty algebra word.

theorem TauCeti.AInfinityRightModuleHom.linearPart_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) {x : M} {p : ℤ} (hx : x ∈ MM.grading.piece p) : f.linearPart x ∈ NN.grading.piece p

The linear part preserves unsuspended degree.

theorem TauCeti.AInfinityRightModuleHom.isHomogeneous_linearPart {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) : LinearMap.IsHomogeneous f.linearPart MM.grading.piece NN.grading.piece 0

The linear part is homogeneous of degree zero.

theorem TauCeti.AInfinityRightModuleHom.linearPart_m_one {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 c : Fin 0 → A) : f.linearPart (((MM.m 1) x) a) = ((NN.m 1) (f.linearPart x)) c

The linear part intertwines the unary module operations, hence is a chain map.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.linearPart_id {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) : (AInfinityRightModuleHom.id MM).linearPart = LinearMap.id

The identity module morphism has identity linear part.

@[simp]

theorem TauCeti.AInfinityRightModuleHom.linearPart_comp {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {AA : AInfinityAlgebra R A} {M : Type uM} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P] {MM : AInfinityRightModule AA M} {NN : AInfinityRightModule AA N} {PP : AInfinityRightModule AA P} (g : AInfinityRightModuleHom NN PP) (f : AInfinityRightModuleHom MM NN) : (g.comp f).linearPart = g.linearPart ∘ₗ f.linearPart

The linear part of a composite is the composite of the linear parts.