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 #
multilinear_map R M₁ M₂is the space of multilinear maps fromΠ(i : ι), M₁ itoM₂.f.map_smulis the multiplicativity of the multilinear mapfalong each coordinate.f.map_addis the additivity of the multilinear mapfalong each coordinate.f.map_smul_univexpresses the multiplicativity offover all coordinates at the same time, writingf (λi, c i • m i)as(∏ i, c i) • f m.f.map_add_univexpresses the additivity offover all coordinates at the same time, writingf (m + m')as the sum over all subsetssofιoff (s.piecewise m m').f.map_sumexpressesf (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)as the sum off (g₁ (r 1), ..., gₙ (r n))whererranges over all possible functions.
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:
- fixing a vector
m : Π(j : ι - i), M₁ j.val, and then choosing separately thei-th coordinate - fixing a vector
m : Πj, M₁ j, and then modifying itsi-th coordinate
The second way is more artificial as the value of m at i is not relevant, but it has the
advantage of avoiding subtype inclusion issues. This is the definition we use, based on
function.update that allows to change the value of m at i.
Note that the use of function.update requires a decidable_eq ι term to appear somewhere in the
statement of multilinear_map.map_add' and multilinear_map.map_smul'. Three possible choices
are:
- Requiring
decidable_eq ιas an argument tomultilinear_map(as we did originally). - Using
classical.dec_eq ιin the statement ofmap_add'andmap_smul'. - Quantifying over all possible
decidable_eq ιinstances in the statement ofmap_add'andmap_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)
- to_fun : (Π (i : ι), M₁ i) → M₂
- map_add' : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), self.to_fun (function.update m i (x + y)) = self.to_fun (function.update m i x) + self.to_fun (function.update m i y)
- map_smul' : ∀ [_inst_1_1 : decidable_eq ι] (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), self.to_fun (function.update m i (c • x)) = c • self.to_fun (function.update m i x)
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
- multilinear_map.has_sizeof_inst
- multilinear_map.has_coe_to_fun
- multilinear_map.has_add
- multilinear_map.has_zero
- multilinear_map.inhabited
- multilinear_map.has_smul
- multilinear_map.add_comm_monoid
- multilinear_map.distrib_mul_action
- multilinear_map.module
- multilinear_map.no_zero_smul_divisors
- multilinear_map.has_neg
- multilinear_map.has_sub
- multilinear_map.add_comm_group
- alternating_map.multilinear_map.has_coe
@[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
- multilinear_map.has_coe_to_fun = {coe := multilinear_map.to_fun _inst_9}
@[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)) :
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) :
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) :
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₂} :
@[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'
@[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)) :
@[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) :
@[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 ι] :
@[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₂)
@[simp]
@[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₂] :
has_zero (multilinear_map R M₁ M₂)
@[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₂] :
inhabited (multilinear_map R M₁ M₂)
Equations
@[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₂)
@[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) :
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₂) :
@[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₂] :
add_comm_monoid (multilinear_map R M₁ M₂)
Equations
- multilinear_map.add_comm_monoid = function.injective.add_comm_monoid coe_fn multilinear_map.add_comm_monoid._proof_2 multilinear_map.add_comm_monoid._proof_3 multilinear_map.add_comm_monoid._proof_4 multilinear_map.add_comm_monoid._proof_5
@[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 α} :
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 : ι) :
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
- f.to_linear_map m i = {to_fun := λ (x : M₁ i), ⇑f (function.update m i x), map_add' := _, map_smul' := _}
@[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) :
⇑(f.to_linear_map m i) x = ⇑f (function.update m i x)
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.
@[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) :
@[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.
@[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) :
⇑(multilinear_map.of_subsingleton R M₂ i') f = function.eval i' f
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
- multilinear_map.of_subsingleton R M₂ i' = {to_fun := function.eval i', map_add' := _, map_smul' := _}
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
- multilinear_map.const_of_is_empty R M₁ m = {to_fun := function.const (Π (i : ι), M₁ i) m, map_add' := _, map_smul' := _}
@[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₂) :
⇑(multilinear_map.const_of_is_empty R M₁ m) = function.const (Π (i : ι), M₁ i) 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.
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) :
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) :
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)) :
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)) :
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.
@[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) :
0.comp_linear_map f = 0
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)) :
function.injective (λ (g : multilinear_map R M₁' M₂), g.comp_linear_map f)
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 ι) :
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) :
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) :
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 ι] :
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) :
multilinear_map R M₁ ↥p
Restrict the codomain of a multilinear map to a submodule.
This is the multilinear version of linear_map.cod_restrict.
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.
@[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₂) :
⇑(multilinear_map.restrict_scalars R f) = ⇑f
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.
@[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₃) :
multilinear_map.dom_dom_congr (σ₁.trans σ₂) m = multilinear_map.dom_dom_congr σ₂ (multilinear_map.dom_dom_congr σ₁ 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₃) :
multilinear_map.dom_dom_congr (σ₂ * σ₁) m = multilinear_map.dom_dom_congr σ₂ (multilinear_map.dom_dom_congr σ₁ 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
- multilinear_map.dom_dom_congr_equiv σ = {to_fun := multilinear_map.dom_dom_congr σ, inv_fun := multilinear_map.dom_dom_congr σ.symm, left_inv := _, right_inv := _, map_add' := _}
@[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₃) :
multilinear_map.dom_dom_congr σ f = multilinear_map.dom_dom_congr σ g ↔ f = g
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.
@[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) :
⇑(g.comp_multilinear_map f) m = ⇑g (⇑f m)
@[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) :
p.subtype.comp_multilinear_map (f.cod_restrict p h) = f
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) :
(linear_map.cod_restrict p g h).comp_multilinear_map f = (g.comp_multilinear_map f).cod_restrict 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 ι) :
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) :
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₂] :
distrib_mul_action R' (multilinear_map A M₁ M₂)
Equations
- multilinear_map.distrib_mul_action = {to_mul_action := {to_has_smul := multilinear_map.has_smul _inst_13, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}
@[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
- multilinear_map.module = {to_distrib_mul_action := multilinear_map.distrib_mul_action _inst_17, add_smul := _, zero_smul := _}
@[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₃] :
no_zero_smul_divisors R' (multilinear_map A M₁ 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₃) :
⇑((multilinear_map.dom_dom_congr_linear_equiv M₂ M₃ R' A σ).symm) ᾰ = (multilinear_map.dom_dom_congr_equiv σ).inv_fun ᾰ
@[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₃) :
⇑(multilinear_map.dom_dom_congr_linear_equiv M₂ M₃ R' A σ) ᾰ = (multilinear_map.dom_dom_congr_equiv σ).to_fun ᾰ
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
- multilinear_map.dom_dom_congr_linear_equiv M₂ M₃ R' A σ = {to_fun := (multilinear_map.dom_dom_congr_equiv σ).to_fun, map_add' := _, map_smul' := _, inv_fun := (multilinear_map.dom_dom_congr_equiv σ).inv_fun, left_inv := _, right_inv := _}
@[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
- multilinear_map.dom_dom_congr_linear_equiv' R M₁ M₂ σ = {to_fun := λ (f : multilinear_map R M₁ M₂), {to_fun := ⇑f ∘ ⇑((equiv.Pi_congr_left' M₁ σ).symm), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _, inv_fun := λ (f : multilinear_map R (λ (i : ι'), M₁ (⇑(σ.symm) i)) M₂), {to_fun := ⇑f ∘ ⇑(equiv.Pi_congr_left' M₁ σ), map_add' := _, map_smul' := _}, left_inv := _, right_inv := _}
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
- multilinear_map.const_linear_equiv_of_is_empty R M₁ M₂ = {to_fun := multilinear_map.const_of_is_empty R M₁ _inst_16, map_add' := _, map_smul' := _, inv_fun := λ (f : multilinear_map R M₁ M₂), ⇑f 0, left_inv := _, right_inv := _}
@[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₂) :
⇑((multilinear_map.const_linear_equiv_of_is_empty R M₁ M₂).symm) f = ⇑f 0
@[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₂) :
⇑(multilinear_map.const_linear_equiv_of_is_empty R M₁ M₂) m = multilinear_map.const_of_is_empty R 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
- multilinear_map.mk_pi_algebra R ι A = {to_fun := λ (m : ι → A), finset.univ.prod (λ (i : ι), m i), map_add' := _, map_smul' := _}
@[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
- multilinear_map.mk_pi_algebra_fin R n A = {to_fun := λ (m : fin n → A), (list.of_fn m).prod, map_add' := _, map_smul' := _}
@[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) :
⇑(multilinear_map.mk_pi_algebra_fin R n A) m = (list.of_fn m).prod
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
- f.smul_right z = (linear_map.id.smul_right z).comp_multilinear_map f
@[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
- multilinear_map.mk_pi_ring R ι z = (multilinear_map.mk_pi_algebra R ι R).smul_right z
@[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₂} :
multilinear_map.mk_pi_ring R ι z₁ = multilinear_map.mk_pi_ring R ι z₂ ↔ z₁ = z₂
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 ι] :
multilinear_map.mk_pi_ring R ι 0 = 0
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₂) :
multilinear_map.mk_pi_ring R ι z = 0 ↔ z = 0
@[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₂)
@[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₂)
@[simp]
@[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₂] :
add_comm_group (multilinear_map R M₁ M₂)
Equations
- multilinear_map.add_comm_group = {add := has_add.add multilinear_map.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul multilinear_map.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg multilinear_map.has_neg, sub := has_sub.sub multilinear_map.has_sub, sub_eq_add_neg := _, zsmul := λ (n : ℤ) (f : multilinear_map R M₁ M₂), {to_fun := λ (m : Π (i : ι), M₁ i), n • ⇑f m, map_add' := _, map_smul' := _}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[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) :
⇑f (function.update m i (-x)) = -⇑f (function.update m i x)
@[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
- multilinear_map.pi_ring_equiv = {to_fun := λ (z : M₂), multilinear_map.mk_pi_ring R ι z, map_add' := _, map_smul' := _, inv_fun := λ (f : multilinear_map R (λ (i : ι), R) M₂), ⇑f (λ (i : ι), 1), left_inv := _, right_inv := _}
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₂) :
multilinear_map R M M₂
Given a linear map f from M 0 to multilinear maps on n variables,
construct the corresponding multilinear map on n+1 variables obtained by concatenating
the variables, given by m ↦ f (m 0) (tail m)
@[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) :
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)).
@[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) :
@[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₂) :
f.uncurry_left.curry_left = f
@[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₂) :
f.curry_left.uncurry_left = f
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
- multilinear_curry_left_equiv R M M₂ = {to_fun := linear_map.uncurry_left _inst_7, map_add' := _, map_smul' := _, inv_fun := multilinear_map.curry_left _inst_7, left_inv := _, right_inv := _}
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₂)) :
multilinear_map R M M₂
Given a multilinear map f in n variables to the space of linear maps from M (last n) to
M₂, construct the corresponding multilinear map on n+1 variables obtained by concatenating
the variables, given by m ↦ f (init m) (m (last n))
@[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)).
@[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)) :
@[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
- multilinear_curry_right_equiv R M M₂ = {to_fun := multilinear_map.uncurry_right _inst_7, map_add' := _, map_smul' := _, inv_fun := multilinear_map.curry_right _inst_7, left_inv := _, right_inv := _}
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'.
@[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') :
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'.
@[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
- multilinear_map.curry_sum_equiv R ι M₂ M' ι' = {to_fun := multilinear_map.curry_sum ι', map_add' := _, map_smul' := _, inv_fun := multilinear_map.uncurry_sum ι', left_inv := _, right_inv := _}
@[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} :
⇑(multilinear_map.curry_sum_equiv R ι M₂ M' ι') = multilinear_map.curry_sum
@[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} :
⇑((multilinear_map.curry_sum_equiv R ι M₂ M' ι').symm) = multilinear_map.uncurry_sum
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
- multilinear_map.curry_fin_finset R M₂ M' hk hl = (multilinear_map.dom_dom_congr_linear_equiv M' M₂ R R (fin_sum_equiv_of_finset hk hl).symm).trans (multilinear_map.curry_sum_equiv R (fin k) M₂ M' (fin l))
@[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') :
@[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') :
@[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') :
@[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') :
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)) :
sub_mul_action R M₂
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.
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₂) :
sub_mul_action R M₂
The range of a multilinear map, closed under scalar multiplication.