Degreewise multilinear operations

A homogeneous multilinear map between internally graded modules is equivalently a family of multilinear maps on their homogeneous pieces, with output degree the sum of the input degrees plus the degree of the operation. The input modules may differ from slot to slot, as happens for composable morphisms in a graded linear quiver.

InternalGrading.homogeneousMultilinearEquiv gives this equivalence without degree casts in its interface. Its inverse extends a degreewise family uniquely to the total modules. The extension uses Mathlib's MultilinearMap.fromDirectSumEquiv and DirectSum.decomposeLinearEquiv.

The degreewise presentation also allows changes of coordinates using Mathlib's LinearEquiv.multilinearMapCongrLeft and LinearEquiv.multilinearMapCongrRight on the relevant pieces, rather than transports of dependent functions.

References

• B. Keller, Introduction to A-infinity algebras and modules, Sections 3.1 and 7.1.

noncomputable def TauCeti.InternalGrading.multilinearFromPieces {R : Type uR} [CommSemiring R] {ι : Type uι} {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)) [Finite ι] (f : (d : ι → ℤ) → MultilinearMap R (fun (i : ι) => ↥((G i).piece (d i))) N) : MultilinearMap R M N

Extend multilinear maps on every tuple of homogeneous pieces to the total modules. No homogeneity condition on the outputs is required for this construction.

Equations

• TauCeti.InternalGrading.multilinearFromPieces G f = (MultilinearMap.fromDirectSumEquiv f).compLinearMap fun (i : ι) => ↑(DirectSum.decomposeLinearEquiv (G i).piece)

@[simp]

theorem TauCeti.InternalGrading.multilinearFromPieces_apply {R : Type uR} [CommSemiring R] {ι : Type uι} {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)) [Finite ι] (f : (d : ι → ℤ) → MultilinearMap R (fun (i : ι) => ↥((G i).piece (d i))) N) (d : ι → ℤ) (x : (i : ι) → ↥((G i).piece (d i))) : ((multilinearFromPieces G f) fun (i : ι) => ↑(x i)) = (f d) x

On homogeneous inputs, extension evaluates the specified component.

theorem TauCeti.InternalGrading.multilinearMap_ext {R : Type uR} [CommSemiring R] {ι : Type uι} {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)) [Finite ι] {f g : MultilinearMap R M N} (h : ∀ (d : ι → ℤ) (x : (i : ι) → M i), (∀ (i : ι), x i ∈ (G i).piece (d i)) → f x = g x) : f = g

Multilinear maps on total modules are determined by their values on homogeneous tuples. The modules and gradings may depend on the input slot.

theorem TauCeti.InternalGrading.multilinearMap_ext_nat {R : Type uR} [CommSemiring R] {N : Type uN} [AddCommMonoid N] [Module R N] {n : ℕ} {P : Type u_1} [AddCommMonoid P] [Module R P] (G : InternalGrading R P) {f g : MultilinearMap R (fun (x : Fin n) => P) N} (h : ∀ (d : ℕ → ℤ) (x : Fin n → P), (∀ (i : Fin n), x i ∈ G.piece (d ↑i)) → f x = g x) : f = g

Multilinear maps in finitely many slots of one graded module are determined by their values on homogeneous tuples whose degrees are recorded by a family indexed by the naturals, as for operations whose inputs are indexed by ℕ.

@[simp]

theorem TauCeti.InternalGrading.multilinearFromPieces_comp_subtype {R : Type uR} [CommSemiring R] {ι : Type uι} {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)) [Finite ι] (f : MultilinearMap R M N) : (multilinearFromPieces G fun (d : ι → ℤ) => f.compLinearMap fun (i : ι) => ((G i).piece (d i)).subtype) = f

Extending the restrictions of a multilinear map recovers the map.

theorem TauCeti.InternalGrading.isHomogeneous_multilinearFromPieces_iff {R : Type uR} [CommSemiring R] {ι : Type uι} {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) [Fintype ι] (f : (d : ι → ℤ) → MultilinearMap R (fun (i : ι) => ↥((G i).piece (d i))) N) (q : ℤ) : MultilinearMap.IsHomogeneous (multilinearFromPieces G f) (fun (i : ι) => (G i).piece) ℬ q ↔ ∀ (d : ι → ℤ) (x : (i : ι) → ↥((G i).piece (d i))), (f d) x ∈ ℬ (∑ i : ι, d i + q)

An extension is homogeneous exactly when each component has the required output degree.

noncomputable def TauCeti.InternalGrading.homogeneousMultilinearEquiv {R : Type uR} [CommSemiring R] {ι : Type uι} {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) [Fintype ι] (q : ℤ) : ↥(MultilinearMap.homogeneousSubmodule (fun (i : ι) => (G i).piece) ℬ q) ≃ₗ[R] (d : ι → ℤ) → MultilinearMap R (fun (i : ι) => ↥((G i).piece (d i))) ↥(ℬ (∑ i : ι, d i + q))

Degree-q homogeneous multilinear maps on the total modules are equivalent to arbitrary families of multilinear maps on the homogeneous pieces with output degree ∑ i, d i + q. The target needs only a family of submodules, and no compatibility condition between distinct degree tuples is needed.

Equations

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

@[simp]

theorem TauCeti.InternalGrading.coe_homogeneousMultilinearEquiv_apply {R : Type uR} [CommSemiring R] {ι : Type uι} {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) [Fintype ι] (q : ℤ) (f : ↥(MultilinearMap.homogeneousSubmodule (fun (i : ι) => (G i).piece) ℬ q)) (d : ι → ℤ) (x : (i : ι) → ↥((G i).piece (d i))) : ↑(((homogeneousMultilinearEquiv G ℬ q) f d) x) = ↑f fun (i : ι) => ↑(x i)

The forward equivalence evaluates the original map on the underlying homogeneous inputs.

@[simp]

theorem TauCeti.InternalGrading.homogeneousMultilinearEquiv_symm_apply {R : Type uR} [CommSemiring R] {ι : Type uι} {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) [Fintype ι] (q : ℤ) (f : (d : ι → ℤ) → MultilinearMap R (fun (i : ι) => ↥((G i).piece (d i))) ↥(ℬ (∑ i : ι, d i + q))) (d : ι → ℤ) (x : (i : ι) → ↥((G i).piece (d i))) : (↑((homogeneousMultilinearEquiv G ℬ q).symm f) fun (i : ι) => ↑(x i)) = ↑((f d) x)

The inverse equivalence extends the component family with its prescribed values.