mathlib3 documentation

linear_algebra.multilinear.basic

Multilinear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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 decidable_eq ι term to appear somewhere in the statement of multilinear_map.map_add' and multilinear_map.map_smul'. Three possible choices are:

  1. Requiring decidable_eq ι as an argument to multilinear_map (as we did originally).
  2. Using classical.dec_eq ι in the statement of map_add' and map_smul'.
  3. Quantifying over all possible decidable_eq ι instances in the statement of map_add' and map_smul'.

Option 1 works fine, but puts unecessary 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.decidable_eq n = classical.dec_eq (fin n). Option 3 of course does something similar, but of the form fin.decidable_eq n = _inst, which is much easier to clean up since _inst is a free variable and so the equality can just be substituted.

structure multilinear_map (R : Type u) {ι : Type u'} (M₁ : ι Type v) (M₂ : Type w) [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.

Instances for multilinear_map
@[protected, instance]
def multilinear_map.has_coe_to_fun {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] :
has_coe_to_fun (multilinear_map R M₁ M₂) (λ (f : multilinear_map R M₁ M₂), (Π (i : ι), M₁ i) M₂)
Equations
@[simp]
theorem multilinear_map.to_fun_eq_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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₁ : [_inst_1 : decidable_eq ι] (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₂ : [_inst_1_1 : decidable_eq ι] (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₂} [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₂} [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_injective {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] :
@[simp, norm_cast]
theorem multilinear_map.coe_inj {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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 f = g
@[ext]
theorem multilinear_map.ext {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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.mk_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) (h₁ : [_inst_1_1 : decidable_eq ι] (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₂ : [_inst_1_1 : decidable_eq ι] (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
@[protected, simp]
theorem multilinear_map.map_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] (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)
@[protected, simp]
theorem multilinear_map.map_smul {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] (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₂} [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₂} [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₂) [decidable_eq ι] (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₂} [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
@[protected, instance]
def multilinear_map.has_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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
@[protected, instance]
def multilinear_map.has_zero {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] :
Equations
@[protected, instance]
def multilinear_map.inhabited {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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
@[protected, instance]
def multilinear_map.has_smul {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (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_smul R' (multilinear_map A M₁ M₂)
Equations
@[simp]
theorem multilinear_map.smul_apply {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (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
theorem multilinear_map.coe_smul {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (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₂] (c : R') (f : multilinear_map A M₁ M₂) :
(c f) = c f
@[protected, instance]
def multilinear_map.add_comm_monoid {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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 α} :
(s.sum (λ (a : α), f a)) m = s.sum (λ (a : α), (f a) m)
def multilinear_map.to_linear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] (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
@[simp]
theorem multilinear_map.to_linear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x : M₁ i) :
def multilinear_map.prod {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [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.prod_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [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₃) (m : Π (i : ι), M₁ i) :
(f.prod g) m = (f m, g m)
@[simp]
theorem multilinear_map.pi_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} [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₁} [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
@[simp]
theorem multilinear_map.of_subsingleton_apply (R : Type u) {ι : Type u'} (M₂ : Type v₂) [semiring R] [add_comm_monoid M₂] [module R M₂] [subsingleton ι] (i' : ι) (f : Π (x : ι), (λ (i : ι), M₂) x) :
def multilinear_map.of_subsingleton (R : Type u) {ι : Type u'} (M₂ : Type v₂) [semiring R] [add_comm_monoid M₂] [module R M₂] [subsingleton ι] (i' : ι) :
multilinear_map R (λ (_x : ι), M₂) M₂

The evaluation map from ι → M₂ to M₂ is multilinear at a given i when ι is subsingleton.

Equations
def multilinear_map.const_of_is_empty (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [is_empty ι] (m : M₂) :
multilinear_map R M₁ M₂

The constant map is multilinear when ι is empty.

Equations
@[simp]
theorem multilinear_map.const_of_is_empty_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) {M₂ : Type v₂} [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [is_empty ι] (m : M₂) :
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.succ Type 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.succ Type 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.succ Type 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.succ Type 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₂} [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₂} [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.comp_linear_map_assoc {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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)] {M₁'' : ι Type u_2} [Π (i : ι), add_comm_monoid (M₁'' i)] [Π (i : ι), module R (M₁'' i)] (g : multilinear_map R M₁'' M₂) (f₁ : Π (i : ι), M₁' i →ₗ[R] M₁'' i) (f₂ : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
(g.comp_linear_map f₁).comp_linear_map f₂ = g.comp_linear_map (λ (i : ι), (f₁ i).comp (f₂ i))

Composing a multilinear map twice with a linear map in each argument is the same as composing with their composition.

@[simp]
theorem multilinear_map.zero_comp_linear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) :

Composing the zero multilinear map with a linear map in each argument.

@[simp]
theorem multilinear_map.comp_linear_map_id {R : Type u} {ι : Type u'} {M₂ : Type v₂} [semiring R] [add_comm_monoid M₂] [module R M₂] {M₁' : ι Type u_1} [Π (i : ι), add_comm_monoid (M₁' i)] [Π (i : ι), module R (M₁' i)] (g : multilinear_map R M₁' M₂) :
g.comp_linear_map (λ (i : ι), linear_map.id) = g

Composing a multilinear map with the identity linear map in each argument.

theorem multilinear_map.comp_linear_map_injective {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (hf : (i : ι), function.surjective (f i)) :

Composing with a family of surjective linear maps is injective.

theorem multilinear_map.comp_linear_map_inj {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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)] (f : Π (i : ι), M₁ i →ₗ[R] M₁' i) (hf : (i : ι), function.surjective (f i)) (g₁ g₂ : multilinear_map R M₁' M₂) :
g₁.comp_linear_map f = g₂.comp_linear_map f g₁ = g₂
@[simp]
theorem multilinear_map.comp_linear_equiv_eq_zero_iff {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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) :
g.comp_linear_map (λ (i : ι), (f i)) = 0 g = 0

Composing a multilinear map with a linear equiv on each argument gives the zero map if and only if the multilinear map is the zero map.

theorem multilinear_map.map_piecewise_add {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] (m m' : Π (i : ι), M₁ i) (t : finset ι) :
f (t.piecewise (m + m') m') = t.powerset.sum (λ (s : finset ι), 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₂} [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₂) [decidable_eq ι] [fintype ι] (m m' : Π (i : ι), M₁ i) :
f (m + m') = finset.univ.sum (λ (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₂} [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 : ι), α i M₁ i) (A : Π (i : ι), finset (α i)) [decidable_eq ι] [fintype ι] {n : } (h : finset.univ.sum (λ (i : ι), (A i).card) = n) :
f (λ (i : ι), (A i).sum (λ (j : α i), g i j)) = (fintype.pi_finset A).sum (λ (r : Π (a : ι), α 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₂} [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 : ι), α i M₁ i) (A : Π (i : ι), finset (α i)) [decidable_eq ι] [fintype ι] :
f (λ (i : ι), (A i).sum (λ (j : α i), g i j)) = (fintype.pi_finset A).sum (λ (r : Π (a : ι), α 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₂} [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 : ι), α i M₁ i) [decidable_eq ι] [fintype ι] [Π (i : ι), fintype (α i)] :
f (λ (i : ι), finset.univ.sum (λ (j : α i), g i j)) = finset.univ.sum (λ (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₂} [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} [decidable_eq ι] (t : finset α) (i : ι) (g : α M₁ i) (m : Π (i : ι), M₁ i) :
f (function.update m i (t.sum (λ (a : α), g a))) = t.sum (λ (a : α), f (function.update m i (g a)))
@[simp]
theorem multilinear_map.cod_restrict_apply_coe {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) (p : submodule R M₂) (h : (v : Π (i : ι), M₁ i), f v p) (v : Π (i : ι), M₁ i) :
((f.cod_restrict p h) v) = f v
def multilinear_map.cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) (p : submodule R M₂) (h : (v : Π (i : ι), M₁ i), f v p) :

Restrict the codomain of a multilinear map to a submodule.

This is the multilinear version of linear_map.cod_restrict.

Equations
def multilinear_map.restrict_scalars (R : Type u) {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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_smul 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₂} [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_smul 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} (σ : ι₁ ι₂) (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} (σ : ι₁ ι₂) (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} (σ₁ : ι₁ ι₂) (σ₂ : ι₂ ι₃) (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} (σ₁ σ₂ : 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} (σ : ι₁ ι₂) (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} (σ : ι₁ ι₂) :
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} (σ : ι₁ ι₂) (m : multilinear_map R (λ (i : ι₂), M₂) M₃) :
@[simp]
theorem multilinear_map.dom_dom_congr_eq_iff {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} (σ : ι₁ ι₂) (f g : multilinear_map R (λ (i : ι₁), M₂) M₃) :

The results of applying dom_dom_congr to two maps are equal if and only if those maps are.

def linear_map.comp_multilinear_map {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [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₃} [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₂) :
@[simp]
theorem linear_map.comp_multilinear_map_apply {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [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.subtype_comp_multilinear_map_cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) (p : submodule R M₂) (h : (v : Π (i : ι), M₁ i), f v p) :

The multilinear version of linear_map.subtype_comp_cod_restrict

@[simp]
theorem linear_map.comp_multilinear_map_cod_restrict {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [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₂) (p : submodule R M₃) (h : (c : M₂), g c p) :

The multilinear version of linear_map.comp_cod_restrict

@[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} (σ : ι₁ ι₂) (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₂} [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₂) [decidable_eq ι] (c : ι R) (m : Π (i : ι), M₁ i) (s : finset ι) :
f (s.piecewise (λ (i : ι), c i m i) m) = s.prod (λ (i : ι), 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₂} [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) = finset.univ.prod (λ (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.

@[simp]
theorem multilinear_map.map_update_smul {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂) [decidable_eq ι] [fintype ι] (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (function.update (c m) i x) = c ^ (fintype.card ι - 1) f (function.update m i x)
@[protected, instance]
def multilinear_map.distrib_mul_action {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (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
@[protected, instance]
def multilinear_map.module {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [Π (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
@[protected, instance]
def multilinear_map.no_zero_smul_divisors {ι : Type u'} {M₁ : ι Type v₁} {M₃ : Type v₃} [Π (i : ι), add_comm_monoid (M₁ i)] {R' : Type u_1} {A : Type u_2} [semiring R'] [semiring A] [Π (i : ι), module A (M₁ i)] [add_comm_monoid M₃] [module R' M₃] [module A M₃] [smul_comm_class A R' M₃] [no_zero_smul_divisors R' M₃] :
@[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} (σ : ι₁ ι₂) (ᾰ : 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} (σ : ι₁ ι₂) (ᾰ : 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} (σ : ι₁ ι₂) :
multilinear_map A (λ (i : ι₁), M₂) M₃ ≃ₗ[R'] multilinear_map A (λ (i : ι₂), M₂) M₃

multilinear_map.dom_dom_congr as a linear_equiv.

Equations
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv'_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_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₂) :
@[simp]
theorem multilinear_map.dom_dom_congr_linear_equiv'_symm_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_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 (λ (i : ι'), M₁ ((σ.symm) i)) M₂) :
def multilinear_map.dom_dom_congr_linear_equiv' (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] {ι' : Type u_1} (σ : ι ι') :
multilinear_map R M₁ M₂ ≃ₗ[R] multilinear_map R (λ (i : ι'), M₁ ((σ.symm) i)) M₂

The dependent version of multilinear_map.dom_dom_congr_linear_equiv.

Equations
def multilinear_map.const_linear_equiv_of_is_empty (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [is_empty ι] :
M₂ ≃ₗ[R] multilinear_map R M₁ M₂

The space of constant maps is equivalent to the space of maps that are multilinear with respect to an empty family.

Equations
@[simp]
theorem multilinear_map.const_linear_equiv_of_is_empty_symm_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [is_empty ι] (f : multilinear_map R M₁ M₂) :
@[simp]
theorem multilinear_map.const_linear_equiv_of_is_empty_apply (R : Type u) {ι : Type u'} (M₁ : ι Type v₁) (M₂ : Type v₂) [comm_semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), module R (M₁ i)] [module R M₂] [is_empty ι] (m : M₂) :
@[protected]
def multilinear_map.mk_pi_algebra (R : Type u) (ι : Type u') [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'} [comm_semiring R] {A : Type u_1} [comm_semiring A] [algebra R A] [fintype ι] (m : ι A) :
(multilinear_map.mk_pi_algebra R ι A) m = finset.univ.prod (λ (i : ι), m i)
@[protected]
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_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₂} [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₂} [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
@[protected]
def multilinear_map.mk_pi_ring (R : Type u) (ι : Type u') {M₂ : Type v₂} [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₂} [comm_semiring R] [add_comm_monoid M₂] [module R M₂] [fintype ι] (z : M₂) (m : ι R) :
(multilinear_map.mk_pi_ring R ι z) m = finset.univ.prod (λ (i : ι), m i) z
theorem multilinear_map.mk_pi_ring_apply_one_eq_self {R : Type u} {ι : Type u'} {M₂ : Type v₂} [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
theorem multilinear_map.mk_pi_ring_eq_iff {R : Type u} {ι : Type u'} {M₂ : Type v₂} [comm_semiring R] [add_comm_monoid M₂] [module R M₂] [fintype ι] {z₁ z₂ : M₂} :
theorem multilinear_map.mk_pi_ring_zero {R : Type u} {ι : Type u'} {M₂ : Type v₂} [comm_semiring R] [add_comm_monoid M₂] [module R M₂] [fintype ι] :
theorem multilinear_map.mk_pi_ring_eq_zero_iff {R : Type u} {ι : Type u'} {M₂ : Type v₂} [comm_semiring R] [add_comm_monoid M₂] [module R M₂] [fintype ι] (z : M₂) :
@[protected, instance]
def multilinear_map.has_neg {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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
@[protected, instance]
def multilinear_map.has_sub {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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
@[protected, instance]
def multilinear_map.add_comm_group {R : Type u} {ι : Type u'} {M₁ : ι Type v₁} {M₂ : Type v₂} [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₂} [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₂) [decidable_eq ι] (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₂} [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₂) [decidable_eq ι] (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)
@[protected]
def multilinear_map.pi_ring_equiv {R : Type u} {ι : Type u'} {M₂ : Type v₂} [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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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.succ Type 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'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} (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'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} (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'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} (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'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} (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') [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] (ι' : Type u_1) :
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'} [comm_semiring R] [add_comm_monoid M'] [add_comm_monoid M₂] [module R M'] [module R M₂] {ι' : Type u_1} :
@[simp]
theorem multilinear_map.coe_curr_sum_equiv_symm {R : Type u} {ι : 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₂] {ι' : Type u_1} :
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₂} [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₂} [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₂} [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