mathlib documentation

linear_algebra.multilinear

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 multilinear_map R M₁ M₂, inherits a module structure by pointwise addition and multiplication.

Main definitions

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.curry_left and f.curry_right respectively (with inverses f.uncurry_left and f.uncurry_right). 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 multilinear_curry_left_equiv and multilinear_curry_right_equiv.

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:

structure multilinear_map (R : Type u) {ι : Type u'} (M₁ : ι → Type v) (M₂ : Type w) [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
Type (max u' v w)

Multilinear maps over the ring R, from Πi, M₁ i to M₂ where M₁ i and M₂ are modules over R.

@[instance]
def multilinear_map.has_coe_to_fun {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :

Equations
@[ext]
theorem multilinear_map.ext {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] {f f' : multilinear_map R M₁ M₂} :
(∀ (x : Π (i : ι), M₁ i), f x = f' x)f = f'

@[simp]
theorem multilinear_map.map_add {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y)

@[simp]
theorem multilinear_map.map_smul {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (function.update m i (c x)) = c f (function.update m i x)

theorem multilinear_map.map_coord_zero {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) {m : Π (i : ι), M₁ i} (i : ι) :
m i = 0f m = 0

@[simp]
theorem multilinear_map.map_zero {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) [nonempty ι] :
f 0 = 0

@[instance]
def multilinear_map.has_add {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
has_add (multilinear_map R M₁ M₂)

Equations
@[simp]
theorem multilinear_map.add_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f f' : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :
(f + f') m = f m + f' m

@[instance]
def multilinear_map.has_zero {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :

Equations
@[instance]
def multilinear_map.inhabited {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :

Equations
@[simp]
theorem multilinear_map.zero_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (m : Π (i : ι), M₁ i) :
0 m = 0

@[instance]
def multilinear_map.add_comm_monoid {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :

Equations
@[simp]
theorem multilinear_map.sum_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] {α : Type u_1} (f : α → multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) {s : finset α} :
(∑ (a : α) in s, f a) m = ∑ (a : α) in s, (f a) m

def multilinear_map.to_linear_map {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) :
M₁ i →ₗ[R] M₂

If f is a multilinear map, then f.to_linear_map m i is the linear map obtained by fixing all coordinates but i equal to those of m, and varying the i-th coordinate.

Equations
def multilinear_map.prod {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] :
multilinear_map R M₁ M₂multilinear_map R M₁ M₃multilinear_map R M₁ (M₂ × M₃)

The cartesian product of two multilinear maps, as a multilinear map.

Equations
def multilinear_map.restr {R : Type u} {M₂ : Type v₂} {M' : Type v'} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M'] [semimodule R M₂] [semimodule R M'] {k n : } (f : multilinear_map R (λ (i : fin n), M') M₂) (s : finset (fin n)) :
s.card = kM' → multilinear_map R (λ (i : fin k), M') M₂

Given a multilinear map f on n variables (parameterized by fin n) and a subset s of k of these variables, one gets a new multilinear map on fin k by varying these variables, and fixing the other ones equal to a given value z. It is denoted by f.restr s hk z, where hk is a proof that the cardinality of s is k. The implicit identification between fin k and s that we use is the canonical (increasing) bijection.

Equations
theorem multilinear_map.cons_add {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M i.succ) (x y : M 0) :
f (fin.cons (x + y) m) = f (fin.cons x m) + f (fin.cons y m)

In the specific case of multilinear maps on spaces indexed by fin (n+1), where one can build an element of Π(i : fin (n+1)), M i using cons, one can express directly the additivity of a multilinear map along the first variable.

theorem multilinear_map.cons_smul {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M i.succ) (c : R) (x : M 0) :
f (fin.cons (c x) m) = c f (fin.cons x m)

In the specific case of multilinear maps on spaces indexed by fin (n+1), where one can build an element of Π(i : fin (n+1)), M i using cons, one can express directly the multiplicativity of a multilinear map along the first variable.

theorem multilinear_map.snoc_add {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M i.cast_succ) (x y : M (fin.last n)) :
f (fin.snoc m (x + y)) = f (fin.snoc m x) + f (fin.snoc m y)

In the specific case of multilinear maps on spaces indexed by fin (n+1), where one can build an element of Π(i : fin (n+1)), M i using snoc, one can express directly the additivity of a multilinear map along the first variable.

theorem multilinear_map.snoc_smul {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M i.cast_succ) (c : R) (x : M (fin.last n)) :
f (fin.snoc m (c x)) = c f (fin.snoc m x)

In the specific case of multilinear maps on spaces indexed by fin (n+1), where one can build an element of Π(i : fin (n+1)), M i using cons, one can express directly the multiplicativity of a multilinear map along the first variable.

def multilinear_map.comp_linear_map {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] {M₁' : ι → Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), semimodule R (M₁' i)] :
multilinear_map R M₁' M₂(Π (i : ι), M₁ i →ₗ[R] M₁' i)multilinear_map R M₁ M₂

If g is a multilinear map and f is a collection of linear maps, then g (f₁ m₁, ..., fₙ mₙ) is again a multilinear map, that we call g.comp_linear_map f.

Equations
@[simp]
theorem multilinear_map.comp_linear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] {M₁' : ι → Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), semimodule R (M₁' i)] (g : multilinear_map R M₁' M₂) (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (m : Π (i : ι), M₁ i) :
(g.comp_linear_map f) m = g (λ (i : ι), (f i) (m i))

theorem multilinear_map.map_piecewise_add {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m m' : Π (i : ι), M₁ i) (t : finset ι) :
f (t.piecewise (m + m') m') = ∑ (s : finset ι) in t.powerset, f (s.piecewise m m')

If one adds to a vector m' another vector m, but only for coordinates in a finset t, then the image under a multilinear map f is the sum of f (s.piecewise m m') along all subsets s of t. This is mainly an auxiliary statement to prove the result when t = univ, given in map_add_univ, although it can be useful in its own right as it does not require the index set ι to be finite.

theorem multilinear_map.map_add_univ {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) [fintype ι] (m m' : Π (i : ι), M₁ i) :
f (m + m') = ∑ (s : finset ι), f (s.piecewise m m')

Additivity of a multilinear map along all coordinates at the same time, writing f (m + m') as the sum of f (s.piecewise m m') over all sets s.

theorem multilinear_map.map_sum_finset_aux {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} [fintype ι] (g : Π (i : ι), α iM₁ i) (A : Π (i : ι), finset (α i)) {n : } :
∑ (i : ι), (A i).card = nf (λ (i : ι), ∑ (j : α i) in A i, g i j) = ∑ (r : Π (a : ι), α a) in fintype.pi_finset A, f (λ (i : ι), g i (r i))

If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ..., r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead map_sum_finset.

theorem multilinear_map.map_sum_finset {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} [fintype ι] (g : Π (i : ι), α iM₁ i) (A : Π (i : ι), finset (α i)) :
f (λ (i : ι), ∑ (j : α i) in A i, g i j) = ∑ (r : Π (a : ι), α a) in fintype.pi_finset A, f (λ (i : ι), g i (r i))

If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ..., r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each coordinate.

theorem multilinear_map.map_sum {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} [fintype ι] (g : Π (i : ι), α iM₁ i) [Π (i : ι), fintype (α i)] :
f (λ (i : ι), ∑ (j : α i), g i j) = ∑ (r : Π (i : ι), α i), f (λ (i : ι), g i (r i))

If f is multilinear, then f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) is the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions r. This follows from multilinearity by expanding successively with respect to each coordinate.

def linear_map.comp_multilinear_map {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] :
(M₂ →ₗ[R] M₃)multilinear_map R M₁ M₂multilinear_map R M₁ M₃

Composing a multilinear map with a linear map gives again a multilinear map.

Equations
@[simp]
theorem linear_map.coe_comp_multilinear_map {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) :

theorem linear_map.comp_multilinear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :

theorem multilinear_map.map_piecewise_smul {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (c : ι → R) (m : Π (i : ι), M₁ i) (s : finset ι) :
f (s.piecewise (λ (i : ι), c i m i) m) = (∏ (i : ι) in s, c i) f m

If one multiplies by c i the coordinates in a finset s, then the image under a multilinear map is multiplied by ∏ i in s, c i. This is mainly an auxiliary statement to prove the result when s = univ, given in map_smul_univ, although it can be useful in its own right as it does not require the index set ι to be finite.

theorem multilinear_map.map_smul_univ {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) [fintype ι] (c : ι → R) (m : Π (i : ι), M₁ i) :
f (λ (i : ι), c i m i) = (∏ (i : ι), c i) f m

Multiplicativity of a multilinear map along all coordinates at the same time, writing f (λi, c i • m i) as (∏ i, c i) • f m.

@[instance]
def multilinear_map.has_scalar {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
has_scalar R (multilinear_map R M₁ M₂)

Equations
@[simp]
theorem multilinear_map.smul_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (c : R) (m : Π (i : ι), M₁ i) :
(c f) m = c f m

def multilinear_map.mk_pi_algebra (R : Type u) (ι : Type u') [decidable_eq ι] [comm_semiring R] (A : Type u_1) [comm_semiring A] [algebra R A] [fintype ι] :
multilinear_map R (λ (i : ι), A) A

Given an R-algebra A, mk_pi_algebra is the multilinear map on A^ι associating to m the product of all the m i.

See also multilinear_map.mk_pi_algebra_fin for a version that works with a non-commutative algebra A but requires ι = fin n.

Equations
@[simp]
theorem multilinear_map.mk_pi_algebra_apply {R : Type u} {ι : Type u'} [decidable_eq ι] [comm_semiring R] {A : Type u_1} [comm_semiring A] [algebra R A] [fintype ι] (m : ι → A) :
(multilinear_map.mk_pi_algebra R ι A) m = ∏ (i : ι), m i

def multilinear_map.mk_pi_algebra_fin (R : Type u) (n : ) [comm_semiring R] (A : Type u_1) [semiring A] [algebra R A] :
multilinear_map R (λ (i : fin n), A) A

Given an R-algebra A, mk_pi_algebra_fin is the multilinear map on A^n associating to m the product of all the m i.

See also multilinear_map.mk_pi_algebra for a version that assumes [comm_semiring A] but works for A^ι with any finite type ι.

Equations
@[simp]
theorem multilinear_map.mk_pi_algebra_fin_apply {R : Type u} {n : } [comm_semiring R] {A : Type u_1} [semiring A] [algebra R A] (m : fin n → A) :

theorem multilinear_map.mk_pi_algebra_fin_apply_const {R : Type u} {n : } [comm_semiring R] {A : Type u_1} [semiring A] [algebra R A] (a : A) :
(multilinear_map.mk_pi_algebra_fin R n A) (λ (_x : fin n), a) = a ^ n

def multilinear_map.smul_right {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
multilinear_map R M₁ RM₂ → multilinear_map R M₁ M₂

Given an R-multilinear map f taking values in R, f.smul_right z is the map sending m to f m • z.

Equations
@[simp]
theorem multilinear_map.smul_right_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ R) (z : M₂) (m : Π (i : ι), M₁ i) :
(f.smul_right z) m = f m z

def multilinear_map.mk_pi_ring (R : Type u) (ι : Type u') {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M₂] [semimodule R M₂] [fintype ι] :
M₂ → multilinear_map R (λ (i : ι), R) M₂

The canonical multilinear map on R^ι when ι is finite, associating to m the product of all the m i (multiplied by a fixed reference element z in the target module). See also mk_pi_algebra for a more general version.

Equations
@[simp]
theorem multilinear_map.mk_pi_ring_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M₂] [semimodule R M₂] [fintype ι] (z : M₂) (m : ι → R) :
(multilinear_map.mk_pi_ring R ι z) m = (∏ (i : ι), m i) z

theorem multilinear_map.mk_pi_ring_apply_one_eq_self {R : Type u} {ι : Type u'} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M₂] [semimodule R M₂] [fintype ι] (f : multilinear_map R (λ (i : ι), R) M₂) :
multilinear_map.mk_pi_ring R ι (f (λ (i : ι), 1)) = f

@[simp]
theorem multilinear_map.map_sub {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i) :
f (function.update m i (x - y)) = f (function.update m i x) - f (function.update m i y)

@[instance]
def multilinear_map.has_neg {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
has_neg (multilinear_map R M₁ M₂)

Equations
@[simp]
theorem multilinear_map.neg_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :
(-f) m = -f m

@[instance]
def multilinear_map.add_comm_group {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :

Equations
@[instance]
def multilinear_map.semimodule (R : Type u) (ι : Type u') (M₁ : ι → Type v₁) (M₂ : Type v₂) [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] :
semimodule R (multilinear_map R M₁ M₂)

The space of multilinear maps is a module over R, for the pointwise addition and scalar multiplication.

Equations
@[instance]
def multilinear_map.semimodule_ring (R : Type u) (ι : Type u') (M₂ : Type v₂) [decidable_eq ι] [comm_ring R] [add_comm_group M₂] [semimodule R M₂] :
semimodule R (multilinear_map R (λ (i : ι), R) M₂)

Equations
def multilinear_map.pi_ring_equiv (R : Type u) (ι : Type u') (M₂ : Type v₂) [decidable_eq ι] [comm_ring R] [add_comm_group M₂] [semimodule R M₂] [fintype ι] :
M₂ ≃ₗ[R] multilinear_map R (λ (i : ι), R) M₂

When ι is finite, multilinear maps on R^ι with values in M₂ are in bijection with M₂, as such a multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear equivalence in multilinear_map.pi_ring_equiv.

Equations

Currying

We associate to a multilinear map in n+1 variables (i.e., based on fin n.succ) two curried functions, named f.curry_left (which is a linear map on E 0 taking values in multilinear maps in n variables) and f.curry_right (wich is a multilinear map in n variables taking values in linear maps on E 0). In both constructions, the variable that is singled out is 0, to take advantage of the operations cons and tail on fin n. The inverse operations are called uncurry_left and uncurry_right.

We also register linear equiv versions of these correspondences, in multilinear_curry_left_equiv and multilinear_curry_right_equiv.

Left currying

def linear_map.uncurry_left {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
(M 0 →ₗ[R] multilinear_map R (λ (i : fin n), M i.succ) M₂)multilinear_map R M M₂

Given a linear map f from M 0 to multilinear maps on n variables, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (m 0) (tail m)

Equations
@[simp]
theorem linear_map.uncurry_left_apply {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : M 0 →ₗ[R] multilinear_map R (λ (i : fin n), M i.succ) M₂) (m : Π (i : fin n.succ), M i) :
(f.uncurry_left) m = (f (m 0)) (fin.tail m)

def multilinear_map.curry_left {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
multilinear_map R M M₂(M 0 →ₗ[R] multilinear_map R (λ (i : fin n), M i.succ) M₂)

Given a multilinear map f in n+1 variables, split the first variable to obtain a linear map into multilinear maps in n variables, given by x ↦ (m ↦ f (cons x m)).

Equations
@[simp]
theorem multilinear_map.curry_left_apply {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) (x : M 0) (m : Π (i : fin n), M i.succ) :
((f.curry_left) x) m = f (fin.cons x m)

@[simp]
theorem linear_map.curry_uncurry_left {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : M 0 →ₗ[R] multilinear_map R (λ (i : fin n), M i.succ) M₂) :

@[simp]
theorem multilinear_map.uncurry_curry_left {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) :

def multilinear_curry_left_equiv (R : Type u) {n : } (M : fin n.succType v) (M₂ : Type v₂) [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
(M 0 →ₗ[R] multilinear_map R (λ (i : fin n), M i.succ) M₂) ≃ₗ[R] multilinear_map R M M₂

The space of multilinear maps on Π(i : fin (n+1)), M i is canonically isomorphic to the space of linear maps from M 0 to the space of multilinear maps on Π(i : fin n), M i.succ, by separating the first variable. We register this isomorphism as a linear isomorphism in multilinear_curry_left_equiv R M M₂.

The direct and inverse maps are given by f.uncurry_left and f.curry_left. Use these unless you need the full framework of linear equivs.

Equations

Right currying

def multilinear_map.uncurry_right {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
multilinear_map R (λ (i : fin n), M i.cast_succ) (M (fin.last n) →ₗ[R] M₂)multilinear_map R M M₂

Given a multilinear map f in n variables to the space of linear maps from M (last n) to M₂, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n))

Equations
@[simp]
theorem multilinear_map.uncurry_right_apply {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R (λ (i : fin n), M i.cast_succ) (M (fin.last n) →ₗ[R] M₂)) (m : Π (i : fin n.succ), M i) :

def multilinear_map.curry_right {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
multilinear_map R M M₂multilinear_map R (λ (i : fin n), M i.cast_succ) (M (fin.last n) →ₗ[R] M₂)

Given a multilinear map f in n+1 variables, split the last variable to obtain a multilinear map in n variables taking values in linear maps from M (last n) to M₂, given by m ↦ (x ↦ f (snoc m x)).

Equations
@[simp]
theorem multilinear_map.curry_right_apply {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M i.cast_succ) (x : M (fin.last n)) :
((f.curry_right) m) x = f (fin.snoc m x)

@[simp]
theorem multilinear_map.curry_uncurry_right {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R (λ (i : fin n), M i.cast_succ) (M (fin.last n) →ₗ[R] M₂)) :

@[simp]
theorem multilinear_map.uncurry_curry_right {R : Type u} {n : } {M : fin n.succType v} {M₂ : Type v₂} [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) :

def multilinear_curry_right_equiv (R : Type u) {n : } (M : fin n.succType v) (M₂ : Type v₂) [comm_ring R] [Π (i : fin n.succ), add_comm_group (M i)] [add_comm_group M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
multilinear_map R (λ (i : fin n), M i.cast_succ) (M (fin.last n) →ₗ[R] M₂) ≃ₗ[R] multilinear_map R M M₂

The space of multilinear maps on Π(i : fin (n+1)), M i is canonically isomorphic to the space of linear maps from the space of multilinear maps on Π(i : fin n), M i.cast_succ to the space of linear maps on M (last n), by separating the last variable. We register this isomorphism as a linear isomorphism in multilinear_curry_right_equiv R M M₂.

The direct and inverse maps are given by f.uncurry_right and f.curry_right. Use these unless you need the full framework of linear equivs.

Equations