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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module R M₂] :
Equations
@[simp]
theorem multilinear_map.to_fun_eq_coe {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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) :
@[simp]
theorem multilinear_map.coe_mk {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 : ι), module R (M₁ i)] [module R M₂] (f : (Π (i : ι), M₁ i) → M₂) (h₁ : ∀ (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)) (h₂ : ∀ (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), f (function.update m i (c x)) = c f (function.update m i x)) :
{to_fun := f, map_add' := h₁, map_smul' := h₂} = f
theorem multilinear_map.congr_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 : ι), module R (M₁ i)] [module R M₂] {f g : multilinear_map R M₁ M₂} (h : f = g) (x : Π (i : ι), M₁ i) :
f x = g x
theorem multilinear_map.congr_arg {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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {x y : Π (i : ι), M₁ i} (h : x = y) :
f x = f y
theorem multilinear_map.coe_inj {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 : ι), module R (M₁ i)] [module R M₂] ⦃f g : multilinear_map R M₁ M₂⦄ (h : f = g) :
f = g
@[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 : ι), module R (M₁ i)] [module R M₂] {f f' : multilinear_map R M₁ M₂} (H : ∀ (x : Π (i : ι), M₁ i), f x = f' x) :
f = f'
theorem multilinear_map.ext_iff {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 : ι), module R (M₁ i)] [module R M₂] {f g : multilinear_map R M₁ M₂} :
f = g ∀ (x : Π (i : ι), M₁ i), f x = g x
@[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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {m : Π (i : ι), M₁ i} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem multilinear_map.map_update_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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) :
f (function.update m i 0) = 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module R M₂] [module R M₃] (f : multilinear_map R M₁ M₂) (g : multilinear_map R M₁ M₃) :
multilinear_map R M₁ (M₂ × M₃)

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

Equations
@[simp]
theorem multilinear_map.pi_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), module R (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), module R (M' i)] (f : Π (i : ι'), multilinear_map R M₁ (M' i)) (m : Π (i : ι), M₁ i) (i : ι') :
(multilinear_map.pi f) m i = (f i) m
def multilinear_map.pi {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), module R (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2} [Π (i : ι'), add_comm_monoid (M' i)] [Π (i : ι'), module R (M' i)] (f : Π (i : ι'), multilinear_map R M₁ (M' i)) :
multilinear_map R M₁ (Π (i : ι'), M' i)

Combine a family of multilinear maps with the same domain and codomains M' i into a multilinear map taking values in the space of functions Π i, M' i.

Equations
def multilinear_map.restr {R : Type u} {M₂ : Type v₂} {M' : Type v'} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M'] [module R M₂] [module R M'] {k n : } (f : multilinear_map R (λ (i : fin n), M') M₂) (s : finset (fin n)) (hk : s.card = k) (z : M') :
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), module R (M i)] [module 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), module R (M i)] [module 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), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M (fin.cast_succ i)) (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), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M (fin.cast_succ i)) (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 : ι), module R (M₁ i)] [module R M₂] {M₁' : ι → Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), module R (M₁' i)] (g : multilinear_map R M₁' M₂) (f : Π (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 : ι), module R (M₁ i)] [module R M₂] {M₁' : ι → Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} (g : Π (i : ι), α iM₁ i) (A : Π (i : ι), finset (α i)) [fintype ι] {n : } (h : ∑ (i : ι), (A i).card = n) :
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. 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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} (g : Π (i : ι), α iM₁ i) (A : Π (i : ι), finset (α i)) [fintype ι] :
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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {α : ι → Type u_1} (g : Π (i : ι), α iM₁ i) [fintype ι] [Π (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.

theorem multilinear_map.map_update_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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) {α : Type u_1} (t : finset α) (i : ι) (g : α → M₁ i) (m : Π (i : ι), M₁ i) :
f (function.update m i (∑ (a : α) in t, g a)) = ∑ (a : α) in t, f (function.update m i (g a))
def multilinear_map.restrict_scalars (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 : ι), module R (M₁ i)] [module R M₂] {A : Type u_1} [semiring A] [has_scalar R A] [Π (i : ι), module A (M₁ i)] [module A M₂] [∀ (i : ι), is_scalar_tower R A (M₁ i)] [is_scalar_tower R A M₂] (f : multilinear_map A M₁ M₂) :
multilinear_map R M₁ M₂

Reinterpret an A-multilinear map as an R-multilinear map, if A is an algebra over R and their actions on all involved modules agree with the action of R on A.

Equations
@[simp]
theorem multilinear_map.coe_restrict_scalars (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 : ι), module R (M₁ i)] [module R M₂] {A : Type u_1} [semiring A] [has_scalar R A] [Π (i : ι), module A (M₁ i)] [module A M₂] [∀ (i : ι), is_scalar_tower R A (M₁ i)] [is_scalar_tower R A M₂] (f : multilinear_map A M₁ M₂) :
def multilinear_map.dom_dom_congr {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
multilinear_map R (λ (i : ι₂), M₂) M₃

Transfer the arguments to a map along an equivalence between argument indices.

The naming is derived from finsupp.dom_congr, noting that here the permutation applies to the domain of the domain.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (m : multilinear_map R (λ (i : ι₁), M₂) M₃) (v : ι₂ → M₂) :
(multilinear_map.dom_dom_congr σ m) v = m (λ (i : ι₁), v (σ i))
theorem multilinear_map.dom_dom_congr_trans {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} [decidable_eq ι₁] [decidable_eq ι₂] [decidable_eq ι₃] (σ₁ : ι₁ ι₂) (σ₂ : ι₂ ι₃) (m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
theorem multilinear_map.dom_dom_congr_mul {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} [decidable_eq ι₁] (σ₁ σ₂ : equiv.perm ι₁) (m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
@[simp]
theorem multilinear_map.dom_dom_congr_equiv_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
def multilinear_map.dom_dom_congr_equiv {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) :
multilinear_map R (λ (i : ι₁), M₂) M₃ ≃+ multilinear_map R (λ (i : ι₂), M₂) M₃

multilinear_map.dom_dom_congr as an equivalence.

This is declared separately because it does not work with dot notation.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_equiv_symm_apply {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [module R M₂] [module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (m : multilinear_map R (λ (i : ι₂), M₂) M₃) :
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 : ι), module R (M₁ i)] [module R M₂] [module R M₃] (g : M₂ →ₗ[R] M₃) (f : 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 : ι), module R (M₁ i)] [module R M₂] [module 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 : ι), module R (M₁ i)] [module R M₂] [module R M₃] (g : M₂ →ₗ[R] M₃) (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :
@[simp]
theorem linear_map.comp_multilinear_map_dom_dom_congr {R : Type u} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'} [semiring R] [add_comm_monoid M₂] [add_comm_monoid M₃] [add_comm_monoid M'] [module R M₂] [module R M₃] [module R M'] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (g : M₂ →ₗ[R] M₃) (f : multilinear_map R (λ (i : ι₁), M') M₂) :
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 : ι), module R (M₁ i)] [module 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 : ι), module R (M₁ i)] [module 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 {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), module A (M₁ i)] [distrib_mul_action R' M₂] [module A M₂] [smul_comm_class A R' M₂] :
has_scalar R' (multilinear_map A M₁ M₂)
Equations
@[simp]
theorem multilinear_map.smul_apply {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), module A (M₁ i)] [distrib_mul_action R' M₂] [module A M₂] [smul_comm_class A R' M₂] (f : multilinear_map A M₁ M₂) (c : R') (m : Π (i : ι), M₁ i) :
(c f) m = c f m
@[instance]
def multilinear_map.distrib_mul_action {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [monoid R'] [semiring A] [Π (i : ι), module A (M₁ i)] [distrib_mul_action R' M₂] [module A M₂] [smul_comm_class A R' M₂] :
Equations
@[instance]
def multilinear_map.module {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), module A (M₁ i)] [module A M₂] [module R' M₂] [smul_comm_class A R' M₂] :
module R' (multilinear_map A M₁ M₂)

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

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv_symm_apply (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [module A M₂] [add_comm_monoid M₃] [module R' M₃] [module A M₃] [smul_comm_class A R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (ᾰ : multilinear_map A (λ (i : ι₂), M₂) M₃) :
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv_apply (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [module A M₂] [add_comm_monoid M₃] [module R' M₃] [module A M₃] [smul_comm_class A R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) (ᾰ : multilinear_map A (λ (i : ι₁), M₂) M₃) :
def multilinear_map.dom_dom_congr_linear_equiv (M₂ : Type v₂) (M₃ : Type v₃) [add_comm_monoid M₂] (R' : Type u_1) (A : Type u_2) [semiring R'] [semiring A] [module A M₂] [add_comm_monoid M₃] [module R' M₃] [module A M₃] [smul_comm_class A R' M₃] {ι₁ : Type u_3} {ι₂ : Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] (σ : ι₁ ι₂) :
multilinear_map A (λ (i : ι₁), M₂) M₃ ≃ₗ[R'] multilinear_map A (λ (i : ι₂), M₂) M₃

multilinear_map.dom_dom_congr as a linear_equiv.

Equations
def multilinear_map.dom_coprod {R : Type u} [comm_semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_5} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_6} [add_comm_monoid N₂] [module R N₂] {N : Type u_7} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) :
multilinear_map R (λ (_x : ι₁ ι₂), N) (N₁ N₂)

Given two multilinear maps (ι₁ → N) → N₁ and (ι₂ → N) → N₂, this produces the map (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂ by taking the coproduct of the domain and the tensor product of the codomain.

This can be thought of as combining equiv.sum_arrow_equiv_prod_arrow.symm with tensor_product.map, noting that the two operations can't be separated as the intermediate result is not a multilinear_map.

While this can be generalized to work for dependent Π i : ι₁, N'₁ i instead of ι₁ → N, doing so introduces sum.elim N'₁ N'₂ types in the result which are difficult to work with and not defeq to the simple case defined here. See this zulip thread.

Equations
@[simp]
theorem multilinear_map.dom_coprod_apply {R : Type u} [comm_semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_5} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_6} [add_comm_monoid N₂] [module R N₂] {N : Type u_7} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) (v : ι₁ ι₂ → N) :
(a.dom_coprod b) v = a (λ (i : ι₁), v (sum.inl i)) ⊗ₜ[R] b (λ (i : ι₂), v (sum.inr i))
def multilinear_map.dom_coprod' {R : Type u} [comm_semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_5} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_6} [add_comm_monoid N₂] [module R N₂] {N : Type u_7} [add_comm_monoid N] [module R N] :
multilinear_map R (λ (_x : ι₁), N) N₁ multilinear_map R (λ (_x : ι₂), N) N₂ →ₗ[R] multilinear_map R (λ (_x : ι₁ ι₂), N) (N₁ N₂)

A more bundled version of multilinear_map.dom_coprod that maps ((ι₁ → N) → N₁) ⊗ ((ι₂ → N) → N₂) to (ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂.

Equations
@[simp]
theorem multilinear_map.dom_coprod'_apply {R : Type u} [comm_semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} [decidable_eq ι₁] [decidable_eq ι₂] {N₁ : Type u_5} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_6} [add_comm_monoid N₂] [module R N₂] {N : Type u_7} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) :
theorem multilinear_map.dom_coprod_dom_dom_congr_sum_congr {R : Type u} [comm_semiring R] {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {ι₄ : Type u_4} [decidable_eq ι₁] [decidable_eq ι₂] [decidable_eq ι₃] [decidable_eq ι₄] {N₁ : Type u_5} [add_comm_monoid N₁] [module R N₁] {N₂ : Type u_6} [add_comm_monoid N₂] [module R N₂] {N : Type u_7} [add_comm_monoid N] [module R N] (a : multilinear_map R (λ (_x : ι₁), N) N₁) (b : multilinear_map R (λ (_x : ι₂), N) N₂) (σa : ι₁ ι₃) (σb : ι₂ ι₄) :

When passed an equiv.sum_congr, multilinear_map.dom_dom_congr distributes over multilinear_map.dom_coprod.

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 : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ R) (z : M₂) :
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 : ι), module R (M₁ i)] [module 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₂] [module R M₂] [fintype ι] (z : 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₂] [module 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₂] [module R M₂] [fintype ι] (f : multilinear_map R (λ (i : ι), R) M₂) :
multilinear_map.mk_pi_ring R ι (f (λ (i : ι), 1)) = f
@[instance]
def multilinear_map.has_neg {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module 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 ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :
(-f) m = -f m
@[instance]
def multilinear_map.has_sub {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] :
has_sub (multilinear_map R M₁ M₂)
Equations
@[simp]
theorem multilinear_map.sub_apply {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] (f g : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) :
(f - g) m = f m - g m
@[instance]
def multilinear_map.add_comm_group {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] :
Equations
@[simp]
theorem multilinear_map.map_neg {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] (f : multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) (x : M₁ i) :
@[simp]
theorem multilinear_map.map_sub {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), module R (M₁ i)] [module 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)
def multilinear_map.pi_ring_equiv {R : Type u} {ι : Type u'} {M₂ : Type v₂} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M₂] [module 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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₂) :

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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R (λ (i : fin n), M (fin.cast_succ i)) (M (fin.last n) →ₗ[R] 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R (λ (i : fin n), M (fin.cast_succ i)) (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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) :
multilinear_map R (λ (i : fin n), M (fin.cast_succ i)) (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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R M M₂) (m : Π (i : fin n), M (fin.cast_succ i)) (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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] (f : multilinear_map R (λ (i : fin n), M (fin.cast_succ i)) (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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid 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_semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), module R (M i)] [module R M₂] :
multilinear_map R (λ (i : fin n), M (fin.cast_succ i)) (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
def multilinear_map.curry_sum {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] (f : multilinear_map R (λ (x : ι ι'), M') M₂) :
multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)

A multilinear map on Π i : ι ⊕ ι', M' defines a multilinear map on Π i : ι, M' taking values in the space of multilinear maps on Π i : ι', M'.

Equations
@[simp]
theorem multilinear_map.curry_sum_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] (f : multilinear_map R (λ (x : ι ι'), M') M₂) (u : ι → M') (v : ι' → M') :
((f.curry_sum) u) v = f (sum.elim u v)
def multilinear_map.uncurry_sum {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] (f : multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)) :
multilinear_map R (λ (x : ι ι'), M') M₂

A multilinear map on Π i : ι, M' taking values in the space of multilinear maps on Π i : ι', M' defines a multilinear map on Π i : ι ⊕ ι', M'.

Equations
@[simp]
theorem multilinear_map.uncurry_sum_aux_apply {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] (f : multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)) (u : ι ι' → M') :
def multilinear_map.curry_sum_equiv (R : Type u) (ι : Type u') (M₂ : Type v₂) (M' : Type v') [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] (ι' : Type u_1) [decidable_eq ι'] [decidable_eq ι')] :
multilinear_map R (λ (x : ι ι'), M') M₂ ≃ₗ[R] multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)

Linear equivalence between the space of multilinear maps on Π i : ι ⊕ ι', M' and the space of multilinear maps on Π i : ι, M' taking values in the space of multilinear maps on Π i : ι', M'.

Equations
@[simp]
theorem multilinear_map.coe_curry_sum_equiv {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] :
@[simp]
theorem multilinear_map.coe_curr_sum_equiv_symm {R : Type u} {ι : Type u'} {M₂ : Type v₂} {M' : Type v'} [decidable_eq ι] [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} [decidable_eq ι'] [decidable_eq ι')] :
def multilinear_map.curry_fin_finset (R : Type u) (M₂ : Type v₂) (M' : Type v') [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) :
multilinear_map R (λ (x : fin n), M') M₂ ≃ₗ[R] multilinear_map R (λ (x : fin k), M') (multilinear_map R (λ (x : fin l), M') M₂)

If s : finset (fin n) is a finite set of cardinality k and its complement has cardinality l, then the space of multilinear maps on λ i : fin n, M' is isomorphic to the space of multilinear maps on λ i : fin k, M' taking values in the space of multilinear maps on λ i : fin l, M'.

Equations
@[simp]
theorem multilinear_map.curry_fin_finset_apply {R : Type u} {M₂ : Type v₂} {M' : Type v'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : multilinear_map R (λ (x : fin n), M') M₂) (mk : fin k → M') (ml : fin l → M') :
(((multilinear_map.curry_fin_finset R M₂ M' hk hl) f) mk) ml = f (λ (i : fin n), sum.elim mk ml (((fin_sum_equiv_of_finset hk hl).symm) i))
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply {R : Type u} {M₂ : Type v₂} {M' : Type v'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : multilinear_map R (λ (x : fin k), M') (multilinear_map R (λ (x : fin l), M') M₂)) (m : fin n → M') :
(((multilinear_map.curry_fin_finset R M₂ M' hk hl).symm) f) m = (f (λ (i : fin k), m ((fin_sum_equiv_of_finset hk hl) (sum.inl i)))) (λ (i : fin l), m ((fin_sum_equiv_of_finset hk hl) (sum.inr i)))
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply_piecewise_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : multilinear_map R (λ (x : fin k), M') (multilinear_map R (λ (x : fin l), M') M₂)) (x y : M') :
(((multilinear_map.curry_fin_finset R M₂ M' hk hl).symm) f) (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y)) = (f (λ (_x : fin k), x)) (λ (_x : fin l), y)
@[simp]
theorem multilinear_map.curry_fin_finset_symm_apply_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : multilinear_map R (λ (x : fin k), M') (multilinear_map R (λ (x : fin l), M') M₂)) (x : M') :
(((multilinear_map.curry_fin_finset R M₂ M' hk hl).symm) f) (λ (_x : fin n), x) = (f (λ (_x : fin k), x)) (λ (_x : fin l), x)
@[simp]
theorem multilinear_map.curry_fin_finset_apply_const {R : Type u} {M₂ : Type v₂} {M' : Type v'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {k l n : } {s : finset (fin n)} (hk : s.card = k) (hl : s.card = l) (f : multilinear_map R (λ (x : fin n), M') M₂) (x y : M') :
(((multilinear_map.curry_fin_finset R M₂ M' hk hl) f) (λ (_x : fin k), x)) (λ (_x : fin l), y) = f (s.piecewise (λ (_x : fin n), x) (λ (_x : fin n), y))
def multilinear_map.map {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [nonempty ι] (f : multilinear_map R M₁ M₂) (p : Π (i : ι), submodule R (M₁ i)) :

The pushforward of an indexed collection of submodule p i ⊆ M₁ i by f : M₁ → M₂.

Note that this is not a submodule - it is not closed under addition.

Equations
theorem multilinear_map.map_nonempty {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [nonempty ι] (f : multilinear_map R M₁ M₂) (p : Π (i : ι), submodule R (M₁ i)) :

The map is always nonempty. This lemma is needed to apply sub_mul_action.zero_mem.

def multilinear_map.range {R : Type u} {ι : Type u'} {M₁ : ι → Type v₁} {M₂ : Type v₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [nonempty ι] (f : multilinear_map R M₁ M₂) :

The range of a multilinear map, closed under scalar multiplication.

Equations