Multilinear maps #

We define multilinear maps as maps from Π (i : ι), M i to N which are σ-semilinear in each coordinate. Here, M i and N are modules over rings R and S, respectively, σ is a ring homomorphism R →+* S and ι is an arbitrary type (although some statements will require it to be a fintype). This space, denoted by (Π i, M i) →ₘₛₗ[σ] N, inherits a module structure by pointwise addition and multiplication.

Main definitions #

MultilinearMap σ M N ((Π i, M i) →ₘₛₗ[σ] N) is the space of σ-multisemilinear maps from (i : ι) → M i to N. Here σ is a RingHom from R to S and we recover plain multilinear maps by choosing σ to be RingHom.id R, in which case the space is denoted by (Π i, M i) →ₘₗ[R] N.
f.map_update_smul is the multiplicativity of the multilinear map f along each coordinate.
f.map_update_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.

See Mathlib/LinearAlgebra/Multilinear/Curry.lean for the currying of multilinear maps.

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_update_add' and MultilinearMap.map_update_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_update_add' and map_update_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.