Suspension signs for right A-infinity module operations

This file collects the two sign calculations shared by right A∞ module identities and module-morphism identities. The first compares a composite of two suspended Taylor maps with the corresponding composite of their unsuspended components. The second compares a term in which the algebra bar differential collapses a block with the corresponding unsuspended term. Both rest on the expansions of a cofree lift and of the algebra bar differential over a pure word.

The component index is the number of algebra inputs; the distinguished module input comes first. If the inner family in a composite has degree q - n on n algebra inputs, moving from the suspended composite to the unsuspended one contributes (-1) ^ ((k + q) * (n - k)) at a cut after k algebra inputs. The formulas are stated for arbitrary source, intermediate, and target modules so that the same calculations apply both to module operations (q = 1) and to module morphisms (q = 0).

Main definitions

• TauCeti.AInfinityRightModule.unsuspend: the module-first unsuspension of a map on a fixed tensor length.

Main results

• TauCeti.AInfinityRightModule.apply_tmul_tprod_of_mem and TauCeti.AInfinityRightModule.unsuspend_mem_piece: its suspension sign and degree.
• TauCeti.AInfinityRightModule.apply_comp_subword_of_mem: the suspension sign for a composite of module-first Taylor maps.
• TauCeti.AInfinityRightModule.cofreeLift_tmul_of_tprod: the cofree lift of a map, expanded over the cuts of a pure word.
• TauCeti.AInfinityRightModule.apply_coaugmentedBarDifferential_of_tprod: the algebra bar differential expanded after an arbitrary linear map on a module tensor factor.
• TauCeti.AInfinityRightModule.apply_algebra_splice_of_mem: the suspension sign when an algebra operation is inserted into the algebra 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.

Module-first unsuspension

noncomputable def TauCeti.AInfinityRightModule.unsuspend {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) (n : ℕ) (F : TensorProduct R M (TensorPower R n A) →ₗ[R] N) : M →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) N

The module-first unsuspension of a map F : M ⊗ A^⊗n → N between suspended inputs: it evaluates F after twisting the input in position j (the module input being in position 0) by the Koszul twist of parameter n - j.

Equations

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

theorem TauCeti.AInfinityRightModule.unsuspend_apply {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) (n : ℕ) (F : TensorProduct R M (TensorPower R n A) →ₗ[R] N) (x : M) (a : Fin n → A) : ((unsuspend G GA n F) x) a = F ((G.koszulTwist ↑n) x ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : Fin n) => (GA.koszulTwist (↑n - 1 - ↑↑i)) (a i))

The unsuspension evaluates the map on Koszul-twisted inputs.

theorem TauCeti.AInfinityRightModule.apply_tmul_tprod_eq_unsuspend {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) (n : ℕ) (F : TensorProduct R M (TensorPower R n A) →ₗ[R] N) (x : M) (a : Fin n → A) : F (x ⊗ₜ[R] (PiTensorProduct.tprod R) a) = ((unsuspend G GA n F) ((G.koszulTwist ↑n) x)) fun (i : Fin n) => (GA.koszulTwist (↑n - 1 - ↑↑i)) (a i)

A map evaluates its unsuspension on Koszul-twisted inputs: the twists are involutions.

theorem TauCeti.AInfinityRightModule.apply_koszulTwist_of_mem {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) {n : ℕ} (φ : M →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) N) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (d : ℕ → ℤ) (a : ℕ → A) (ha : ∀ i < n, a i ∈ GA.piece (d i)) : ((φ ((G.koszulTwist ↑n) x)) fun (i : Fin n) => (GA.koszulTwist (↑n - 1 - ↑↑i)) (a ↑i)) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • (φ x).evalNat a

On homogeneous inputs, the Koszul twists of the module-first unsuspension multiply to the Koszul sign of suspending the module input and all algebra inputs.

theorem TauCeti.AInfinityRightModule.apply_tmul_tprod_of_mem {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) (n : ℕ) (F : TensorProduct R M (TensorPower R n A) →ₗ[R] N) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (d : ℕ → ℤ) (a : ℕ → A) (ha : ∀ i < n, a i ∈ GA.piece (d i)) : F (x ⊗ₜ[R] (PiTensorProduct.tprod R) fun (i : Fin n) => a ↑i) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • ((unsuspend G GA n F) x).evalNat a

On homogeneous inputs, a map is its module-first unsuspension multiplied by the suspension Koszul sign.

theorem TauCeti.AInfinityRightModule.unsuspend_mem_piece {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (G : InternalGrading R M) (GA : InternalGrading R A) {GN : InternalGrading R N} (n : ℕ) {F : TensorProduct R M (TensorPower R n A) →ₗ[R] N} (k : ℤ) (hF : ∀ {x : M} {p : ℤ}, x ∈ (G.shift 1).piece p → ∀ (a : Fin n → A) (d : Fin n → ℤ), (∀ (i : Fin n), a i ∈ (GA.shift 1).piece (d i)) → F (x ⊗ₜ[R] (PiTensorProduct.tprod R) a) ∈ GN.piece (p + ∑ i : Fin n, d i + k)) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (a : Fin n → A) (d : Fin n → ℤ) (ha : ∀ (i : Fin n), a i ∈ GA.piece (d i)) : ((unsuspend G GA n F) x) a ∈ GN.piece (e + ∑ i : Fin n, d i - ↑n + (k - 1))

If a map of suspended inputs raises total suspended degree by k, its module-first unsuspension has degree k - 1 - n on n algebra inputs.

Bar-word expansions, composites, and algebra insertions

theorem TauCeti.AInfinityRightModule.apply_comp_subword_of_mem {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module 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] {GA : InternalGrading R A} {GM : InternalGrading R M} {GN : InternalGrading R N} {F : TensorProduct R M (TensorWords R A) →ₗ[R] N} {H : TensorProduct R N (TensorWords R A) →ₗ[R] P} {f : (n : ℕ) → M →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) N} {h : (n : ℕ) → N →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) P} {q : ℤ} (hFf : ∀ (n : ℕ) (x : M) (a : Fin n → A), F (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ((f n) ((GM.koszulTwist ↑n) x)) fun (i : Fin n) => (GA.koszulTwist (↑n - 1 - ↑↑i)) (a i)) (hf : ∀ (n : ℕ) {x : M} {p : ℤ}, x ∈ GM.piece p → ∀ (a : Fin n → A) (d : Fin n → ℤ), (∀ (i : Fin n), a i ∈ GA.piece (d i)) → ((f n) x) a ∈ GN.piece (p + ∑ i : Fin n, d i + (q - ↑n))) (hHh : ∀ (n : ℕ) (x : N) (a : Fin n → A), H (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ((h n) ((GN.koszulTwist ↑n) x)) fun (i : Fin n) => (GA.koszulTwist (↑n - 1 - ↑↑i)) (a i)) {n k : ℕ} (hk : k ≤ n) {x : M} {e : ℤ} (hx : x ∈ GM.piece e) (d : ℕ → ℤ) (a : ℕ → A) (ha : ∀ i < n, a i ∈ GA.piece (d i)) : H (F (x ⊗ₜ[R] TensorWords.subword R (fun (i : Fin n) => a ↑i) 0 k) ⊗ₜ[R] TensorWords.subword R (fun (i : Fin n) => a ↑i) k (n - k)) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • negOnePowCast R ((↑k + q) * (↑n - ↑k)) • ((h (n - k)) (((f k) x).evalNat a)).evalNat fun (j : ℕ) => a (k + j)

A composite of suspended module-first Taylor maps on homogeneous inputs, expressed through their unsuspended components. The inner components have degree q - k on k algebra inputs; the outer degree is irrelevant to the suspension sign.

theorem TauCeti.AInfinityRightModule.cofreeLift_tmul_of_tprod {R : Type uR} {A : Type uA} [CommRing R] [AddCommGroup A] [Module R A] {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (F : TensorProduct R M (TensorWords R A) →ₗ[R] N) (n : ℕ) (x : M) (a : Fin n → A) : (Comodule.Hom.cofreeLift F).toLinearMap (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ∑ k ∈ Finset.range (n + 1), F (x ⊗ₜ[R] TensorWords.subword R a 0 k) ⊗ₜ[R] TensorWords.subword R a k (n - k)

On a pure word, the cofree lift of F applies F to every prefix and retains the corresponding suffix.

theorem TauCeti.AInfinityRightModule.apply_coaugmentedBarDifferential_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] (F : TensorProduct R M (TensorWords R A) →ₗ[R] N) (n : ℕ) (x : M) (a : Fin n → A) : F (x ⊗ₜ[R] AA.coaugmentedBarDifferential ((TensorWords.of R A n) ((PiTensorProduct.tprod R) a))) = ∑ p ∈ Finset.range n, ∑ s ∈ Finset.Icc 1 (n - p), F (x ⊗ₜ[R] (TensorWords.reducedInclusion R A) (ReducedTensorWords.splice R ((AA.grading.shift 1).twistedTuple 1 a 0 p) 0 n p s (AA.taylor (ReducedTensorWords.subword R a p s))))

Applying a linear map after tensoring a module element with the algebra bar differential expands as the sum over all nonempty blocks collapsed by the algebra Taylor map.

theorem TauCeti.AInfinityRightModule.apply_algebra_splice_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] {G : InternalGrading R M} {F : TensorProduct R M (TensorWords R A) →ₗ[R] N} {f : (n : ℕ) → M →ₗ[R] MultilinearMap R (fun (x : Fin n) => A) N} (hFf : ∀ (n : ℕ) (x : M) (a : Fin n → A), F (x ⊗ₜ[R] (TensorWords.of R A n) ((PiTensorProduct.tprod R) a)) = ((f n) ((G.koszulTwist ↑n) x)) fun (i : Fin n) => (AA.grading.koszulTwist (↑n - 1 - ↑↑i)) (a i)) {n p s : ℕ} (hs : 0 < s) (hps : p + s ≤ n) {x : M} {e : ℤ} (hx : x ∈ G.piece e) (d : ℕ → ℤ) (a : ℕ → A) (ha : ∀ i < n, a i ∈ AA.grading.piece (d i)) : F (((G.shift 1).koszulTwist 1) x ⊗ₜ[R] (TensorWords.reducedInclusion R A) (ReducedTensorWords.splice R ((AA.grading.shift 1).twistedTuple 1 (fun (i : Fin n) => a ↑i) 0 p) 0 n p s (AA.taylor (ReducedTensorWords.subword R (fun (i : Fin n) => a ↑i) p s)))) = negOnePowCast R (↑n * e + MultilinearMap.suspExp n d) • negOnePowCast R (↑p + 1 + ↑s * (↑n - ↑p - ↑s) + (2 - ↑s) * (e + ∑ i ∈ Finset.range p, d i)) • ((f (p + 1 + (n - p - s))) x).evalNat (replaceBlock a p s ((AA.m s).evalNat fun (j : ℕ) => a (p + j)))

A suspended term in which the algebra bar differential collapses a block of homogeneous algebra inputs, expressed through the unsuspended module-first component and algebra operation.