Multilinear maps in coordinates #
The value of a multilinear map f on arguments m i, each in a module M i with a finite basis
b i, is the sum, over all choices s of one basis index for each argument, of the products of
the coordinates (b i).repr (m i) (s i) times the value of f on the basis vectors b i (s i)
(MultilinearMap.apply_eq_sum_prod_repr_smul). This expresses f through finitely many scalar
coefficients, which is how pairings of multilinear maps with families of vectors reduce to scalar
pairings.
theorem
MultilinearMap.apply_eq_sum_prod_repr_smul
{R : Type u_1}
{ι : Type u_2}
{N : Type u_3}
{κ : ι → Type u_4}
{M : ι → Type u_5}
[CommSemiring R]
[Fintype ι]
[DecidableEq ι]
[(i : ι) → Fintype (κ i)]
[(i : ι) → AddCommMonoid (M i)]
[(i : ι) → Module R (M i)]
[AddCommMonoid N]
[Module R N]
(f : (Π (a : ι), M a) →ₘₗ[R] N)
(b : (i : ι) → Module.Basis (κ i) R (M i))
(m : (i : ι) → M i)
:
Multilinear maps in coordinates. For finite bases b i of the modules M i,
f m = ∑ s, (∏ i, (b i).repr (m i) (s i)) • f (fun i ↦ b i (s i)).