Suspension of dependent homogeneous multilinear operations

Suspension regrades every input and the output by one. An arity-n operation of degree q + 1 - n therefore becomes an operation of degree q. The commuting suspension square also requires the tensor-map Koszul sign: input i contributes its original degree once for every input to its right.

InternalGrading.suspensionEquiv implements this square for possibly different input modules. Its inverse uses the same twists, computed from the original gradings, not the suspended ones. It applies to operations on composable morphisms as well as to algebra and module operations. The output needs only a family of submodules, not an internal direct-sum grading.

The degree calculation uses MultilinearMap.isHomogeneous_shift_const_iff; the sign uses the existing Koszul twists, hence Mathlib's integer sign character. This generalizes the Koszul-twist construction of AInfinity.suspensionTaylor in TauCeti.Algebra.Homology.AInfinity.Coderivation to dependent input modules.

References

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

@[simp]

theorem TauCeti.InternalGrading.isHomogeneous_comp_koszulTwist_iff {R : Type uR} [CommRing R] {ι : Type u_1} [Fintype ι] {M : ι → Type uM} {N : Type uN} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : ι) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (t : ι → ℤ) (q : ℤ) (f : MultilinearMap R M N) : MultilinearMap.IsHomogeneous (f.compLinearMap fun (i : ι) => (G i).koszulTwist (t i)) (fun (i : ι) => (G i).piece) ℬ q ↔ MultilinearMap.IsHomogeneous f (fun (i : ι) => (G i).piece) ℬ q

Precomposing the inputs by arbitrary Koszul twists preserves and reflects homogeneity. The input modules and twist parameters may vary from slot to slot.

noncomputable def TauCeti.InternalGrading.suspensionEquiv {R : Type uR} [CommRing R] {n : ℕ} {M : Fin n → Type uM} {N : Type uN} [(i : Fin n) → AddCommMonoid (M i)] [(i : Fin n) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (q : ℤ) : ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => (G i).piece) ℬ (q + 1 - ↑n)) ≃ₗ[R] ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => ((G i).shift 1).piece) (Graded.shift ℬ 1) q)

Suspension identifies arity-n operations of degree q + 1 - n with operations of degree q on the suspended pieces. Both directions twist input i by n - 1 - i using its original grading.

Equations

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

theorem TauCeti.InternalGrading.suspensionEquiv_val {R : Type uR} [CommRing R] {n : ℕ} {M : Fin n → Type uM} {N : Type uN} [(i : Fin n) → AddCommMonoid (M i)] [(i : Fin n) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (q : ℤ) (f : ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => (G i).piece) ℬ (q + 1 - ↑n))) : ↑((suspensionEquiv G ℬ q) f) = (↑f).compLinearMap fun (i : Fin n) => (G i).koszulTwist (↑n - 1 - ↑↑i)

The underlying suspended operation is precomposition by the suspension Koszul twists.

theorem TauCeti.InternalGrading.suspensionEquiv_symm_val {R : Type uR} [CommRing R] {n : ℕ} {M : Fin n → Type uM} {N : Type uN} [(i : Fin n) → AddCommMonoid (M i)] [(i : Fin n) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (q : ℤ) (f : ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => ((G i).shift 1).piece) (Graded.shift ℬ 1) q)) : ↑((suspensionEquiv G ℬ q).symm f) = (↑f).compLinearMap fun (i : Fin n) => (G i).koszulTwist (↑n - 1 - ↑↑i)

Unsuspension uses the same original-grading twists as suspension.

theorem TauCeti.InternalGrading.suspensionEquiv_apply_of_mem {R : Type uR} [CommRing R] {n : ℕ} {M : Fin n → Type uM} {N : Type uN} [(i : Fin n) → AddCommMonoid (M i)] [(i : Fin n) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (q : ℤ) (f : ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => (G i).piece) ℬ (q + 1 - ↑n))) (d : Fin n → ℤ) (x : (i : Fin n) → M i) (hx : ∀ (i : Fin n), x i ∈ (G i).piece (d i)) : ↑((suspensionEquiv G ℬ q) f) x = negOnePowCast R (∑ i : Fin n, (↑n - 1 - ↑↑i) * d i) • ↑f x

On homogeneous inputs the suspension square contributes exactly the tensor-map Koszul sign, computed from the original input degrees.

theorem TauCeti.InternalGrading.suspensionEquiv_symm_apply_of_mem {R : Type uR} [CommRing R] {n : ℕ} {M : Fin n → Type uM} {N : Type uN} [(i : Fin n) → AddCommMonoid (M i)] [(i : Fin n) → Module R (M i)] [AddCommMonoid N] [Module R N] (G : (i : Fin n) → InternalGrading R (M i)) (ℬ : ℤ → Submodule R N) (q : ℤ) (f : ↥(MultilinearMap.homogeneousSubmodule (fun (i : Fin n) => ((G i).shift 1).piece) (Graded.shift ℬ 1) q)) (d : Fin n → ℤ) (x : (i : Fin n) → M i) (hx : ∀ (i : Fin n), x i ∈ (G i).piece (d i)) : ↑((suspensionEquiv G ℬ q).symm f) x = negOnePowCast R (∑ i : Fin n, (↑n - 1 - ↑↑i) * d i) • ↑f x

On homogeneous inputs, unsuspension has the identical sign when degrees are measured in the original gradings.