Multilinear maps #

We define multilinear maps as maps from ∀ (i : ι), M₁ i to M₂ which are linear in each coordinate. Here, M₁ i and M₂ are modules over a ring R, and ι is an arbitrary type (although some statements will require it to be a fintype). This space, denoted by MultilinearMap R M₁ M₂, inherits a module structure by pointwise addition and multiplication.

Main definitions #

MultilinearMap R M₁ M₂ is the space of multilinear maps from ∀ (i : ι), M₁ i to M₂.
f.map_smul is the multiplicativity of the multilinear map f along each coordinate.
f.map_add is the additivity of the multilinear map f along each coordinate.
f.map_smul_univ expresses the multiplicativity of f over all coordinates at the same time, writing f (fun i => c i • m i) as (∏ i, c i) • f m.
f.map_add_univ expresses the additivity of f over all coordinates at the same time, writing

f (m + m') as the sum over all subsets s of ι of f (s.piecewise m m').
f.map_sum expresses f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) as the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all possible functions.

We also register isomorphisms corresponding to currying or uncurrying variables, transforming a multilinear function f on n+1 variables into a linear function taking values in multilinear functions in n variables, and into a multilinear function in n variables taking values in linear functions. These operations are called f.curryLeft and f.curryRight respectively (with inverses f.uncurryLeft and f.uncurryRight). These operations induce linear equivalences between spaces of multilinear functions in n+1 variables and spaces of linear functions into multilinear functions in n variables (resp. multilinear functions in n variables taking values in linear functions), called respectively multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

Implementation notes #

Expressing that a map is linear along the i-th coordinate when all other coordinates are fixed can be done in two (equivalent) different ways:

fixing a vector m : ∀ (j : ι - i), M₁ j.val, and then choosing separately the i-th coordinate
fixing a vector m : ∀j, M₁ j, and then modifying its i-th coordinate

The second way is more artificial as the value of m at i is not relevant, but it has the advantage of avoiding subtype inclusion issues. This is the definition we use, based on Function.update that allows to change the value of m at i.

Note that the use of Function.update requires a DecidableEq ι term to appear somewhere in the statement of MultilinearMap.map_add' and MultilinearMap.map_smul'. Three possible choices are:

Requiring DecidableEq ι as an argument to MultilinearMap (as we did originally).
Using Classical.decEq ι in the statement of map_add' and map_smul'.
Quantifying over all possible DecidableEq ι instances in the statement of map_add' and map_smul'.

Option 1 works fine, but puts unnecessary constraints on the user (the zero map certainly does not need decidability). Option 2 looks great at first, but in the common case when ι = Fin n it introduces non-defeq decidability instance diamonds within the context of proving map_add' and map_smul', of the form Fin.decidableEq n = Classical.decEq (Fin n). Option 3 of course does something similar, but of the form Fin.decidableEq n = _inst, which is much easier to clean up since _inst is a free variable and so the equality can just be substituted.

Multilinear maps #

Main definitions #

Implementation notes #

Currying #

Left currying #

Right currying #