Multilinear maps #
We define multilinear maps as maps from Π(i : ι), M₁ i to M₂ which are linear in each
coordinate. Here, M₁ i and M₂ are modules over a ring R, and ι is an arbitrary type
(although some statements will require it to be a fintype). This space, denoted by
multilinear_map R M₁ M₂, inherits a module structure by pointwise addition and multiplication.
Main definitions #
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 ofmatiis not relevant, but it has the advantage of avoiding subtype inclusion issues. This is the definition we use, based onfunction.updatethat allows to change the value ofmati.
structure
multilinear_map
(R : Type u)
{ι : Type u'}
(M₁ : ι → Type v)
(M₂ : Type w)
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
Type (max u' v w)
- to_fun : (Π (i : ι), M₁ i) → M₂
- map_add' : ∀ (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' : ∀ (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.
@[protected, instance]
def
multilinear_map.has_coe_to_fun
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
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_10}
@[simp]
theorem
multilinear_map.to_fun_eq_coe
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂) :
@[simp]
theorem
multilinear_map.coe_mk
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : (Π (i : ι), M₁ i) → M₂)
(h₁ : ∀ (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), f (function.update m i (x + y)) = f (function.update m i x) + f (function.update m i y))
(h₂ : ∀ (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), f (function.update m i (c • x)) = c • f (function.update m i x)) :
theorem
multilinear_map.congr_fun
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{f g : multilinear_map R M₁ M₂}
(h : f = g)
(x : Π (i : ι), M₁ i) :
theorem
multilinear_map.congr_arg
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{x y : Π (i : ι), M₁ i}
(h : x = y) :
theorem
multilinear_map.coe_injective
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
@[simp, norm_cast]
theorem
multilinear_map.coe_inj
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{f g : multilinear_map R M₁ M₂} :
@[ext]
theorem
multilinear_map.ext
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{f f' : multilinear_map R M₁ M₂}
(H : ∀ (x : Π (i : ι), M₁ i), ⇑f x = ⇑f' x) :
f = f'
theorem
multilinear_map.ext_iff
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{f g : multilinear_map R M₁ M₂} :
@[simp]
theorem
multilinear_map.mk_coe
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(h₁ : ∀ (m : Π (i : ι), M₁ i) (i : ι) (x y : M₁ i), ⇑f (function.update m i (x + y)) = ⇑f (function.update m i x) + ⇑f (function.update m i y))
(h₂ : ∀ (m : Π (i : ι), M₁ i) (i : ι) (c : R) (x : M₁ i), ⇑f (function.update m i (c • x)) = c • ⇑f (function.update m i x)) :
@[protected, simp]
theorem
multilinear_map.map_add
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι)
(x y : M₁ i) :
⇑f (function.update m i (x + y)) = ⇑f (function.update m i x) + ⇑f (function.update m i y)
@[simp]
theorem
multilinear_map.map_smul
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι)
(c : R)
(x : M₁ i) :
⇑f (function.update m i (c • x)) = c • ⇑f (function.update m i x)
theorem
multilinear_map.map_coord_zero
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{m : Π (i : ι), M₁ i}
(i : ι)
(h : m i = 0) :
@[simp]
theorem
multilinear_map.map_update_zero
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι) :
⇑f (function.update m i 0) = 0
@[simp]
theorem
multilinear_map.map_zero
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
[nonempty ι] :
@[protected, instance]
def
multilinear_map.has_add
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
has_add (multilinear_map R M₁ M₂)
@[simp]
theorem
multilinear_map.add_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f f' : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
multilinear_map.has_zero
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
has_zero (multilinear_map R M₁ M₂)
@[protected, instance]
def
multilinear_map.inhabited
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
inhabited (multilinear_map R M₁ M₂)
Equations
@[simp]
theorem
multilinear_map.zero_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
multilinear_map.has_scalar
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
{R' : Type u_1}
{A : Type u_2}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[distrib_mul_action R' M₂]
[module A M₂]
[smul_comm_class A R' M₂] :
has_scalar R' (multilinear_map A M₁ M₂)
@[simp]
theorem
multilinear_map.smul_apply
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
{R' : Type u_1}
{A : Type u_2}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[distrib_mul_action R' M₂]
[module A M₂]
[smul_comm_class A R' M₂]
(f : multilinear_map A M₁ M₂)
(c : R')
(m : Π (i : ι), M₁ i) :
theorem
multilinear_map.coe_smul
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
{R' : Type u_1}
{A : Type u_2}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[distrib_mul_action R' M₂]
[module A M₂]
[smul_comm_class A R' M₂]
(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₂}
[decidable_eq ι]
[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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{α : Type u_1}
(f : α → multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
{s : finset α} :
def
multilinear_map.to_linear_map
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι) :
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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι)
(x : 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₃}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
(f : multilinear_map R M₁ M₂)
(g : multilinear_map R M₁ M₃) :
multilinear_map R M₁ (M₂ × M₃)
The cartesian product of two multilinear maps, as a multilinear map.
@[simp]
theorem
multilinear_map.pi_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), multilinear_map R M₁ (M' i))
(m : Π (i : ι), M₁ i)
(i : ι') :
⇑(multilinear_map.pi f) m i = ⇑(f i) m
def
multilinear_map.pi
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[Π (i : ι), module R (M₁ i)]
{ι' : Type u_1}
{M' : ι' → Type u_2}
[Π (i : ι'), add_comm_monoid (M' i)]
[Π (i : ι'), module R (M' i)]
(f : Π (i : ι'), multilinear_map R M₁ (M' i)) :
multilinear_map R M₁ (Π (i : ι'), M' i)
Combine a family of multilinear maps with the same domain and codomains M' i into a
multilinear map taking values in the space of functions Π i, M' i.
@[simp]
theorem
multilinear_map.of_subsingleton_apply
(R : Type u)
{ι : Type u'}
(M₂ : Type v₂)
[decidable_eq ι]
[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₂)
[decidable_eq ι]
[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₂}
[decidable_eq ι]
[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 = {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₂}
[decidable_eq ι]
[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) = 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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(g : multilinear_map R M₁' M₂)
(f : Π (i : ι), M₁ i →ₗ[R] M₁' i) :
multilinear_map R M₁ M₂
If g is a multilinear map and f is a collection of linear maps,
then g (f₁ m₁, ..., fₙ mₙ) is again a multilinear map, that we call
g.comp_linear_map f.
@[simp]
theorem
multilinear_map.comp_linear_map_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(g : multilinear_map R M₁' M₂)
(f : Π (i : ι), M₁ i →ₗ[R] M₁' i)
(m : Π (i : ι), M₁ i) :
⇑(g.comp_linear_map f) m = ⇑g (λ (i : ι), ⇑(f i) (m i))
theorem
multilinear_map.comp_linear_map_assoc
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
{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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(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₂}
[decidable_eq ι]
[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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{M₁' : ι → Type u_1}
[Π (i : ι), add_comm_monoid (M₁' i)]
[Π (i : ι), module R (M₁' i)]
(g : multilinear_map R M₁' M₂)
(f : Π (i : ι), M₁ i ≃ₗ[R] M₁' i) :
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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m m' : Π (i : ι), M₁ i)
(t : finset ι) :
If one adds to a vector m' another vector m, but only for coordinates in a finset t, then
the image under a multilinear map f is the sum of f (s.piecewise m m') along all subsets s of
t. This is mainly an auxiliary statement to prove the result when t = univ, given in
map_add_univ, although it can be useful in its own right as it does not require the index set ι
to be finite.
theorem
multilinear_map.map_add_univ
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
[fintype ι]
(m m' : Π (i : ι), M₁ i) :
Additivity of a multilinear map along all coordinates at the same time,
writing f (m + m') as the sum of f (s.piecewise m m') over all sets s.
theorem
multilinear_map.map_sum_finset_aux
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{α : ι → Type u_1}
(g : Π (i : ι), α i → M₁ i)
(A : Π (i : ι), finset (α i))
[fintype ι]
{n : ℕ}
(h : ∑ (i : ι), (A i).card = n) :
⇑f (λ (i : ι), ∑ (j : α i) in A i, g i j) = ∑ (r : Π (a : ι), α a) in fintype.pi_finset A, ⇑f (λ (i : ι), g i (r i))
If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of
f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ...,
r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each
coordinate. Here, we give an auxiliary statement tailored for an inductive proof. Use instead
map_sum_finset.
theorem
multilinear_map.map_sum_finset
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{α : ι → Type u_1}
(g : Π (i : ι), α i → M₁ i)
(A : Π (i : ι), finset (α i))
[fintype ι] :
⇑f (λ (i : ι), ∑ (j : α i) in A i, g i j) = ∑ (r : Π (a : ι), α a) in fintype.pi_finset A, ⇑f (λ (i : ι), g i (r i))
If f is multilinear, then f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ) is the sum of
f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions with r 1 ∈ A₁, ...,
r n ∈ Aₙ. This follows from multilinearity by expanding successively with respect to each
coordinate.
theorem
multilinear_map.map_sum
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{α : ι → Type u_1}
(g : Π (i : ι), α i → M₁ i)
[fintype ι]
[Π (i : ι), fintype (α i)] :
If f is multilinear, then f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) is the sum of
f (g₁ (r 1), ..., gₙ (r n)) where r ranges over all functions r. This follows from
multilinearity by expanding successively with respect to each coordinate.
theorem
multilinear_map.map_update_sum
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
{α : Type u_1}
(t : finset α)
(i : ι)
(g : α → M₁ i)
(m : Π (i : ι), M₁ i) :
⇑f (function.update m i (∑ (a : α) in t, g a)) = ∑ (a : α) in t, ⇑f (function.update m i (g a))
def
multilinear_map.restrict_scalars
(R : Type u)
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{A : Type u_1}
[semiring A]
[has_scalar R A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[∀ (i : ι), is_scalar_tower R A (M₁ i)]
[is_scalar_tower R A M₂]
(f : multilinear_map A M₁ M₂) :
multilinear_map R M₁ M₂
Reinterpret an A-multilinear map as an R-multilinear map, if A is an algebra over R
and their actions on all involved modules agree with the action of R on A.
@[simp]
theorem
multilinear_map.coe_restrict_scalars
(R : Type u)
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{A : Type u_1}
[semiring A]
[has_scalar R A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[∀ (i : ι), is_scalar_tower R A (M₁ i)]
[is_scalar_tower R A M₂]
(f : multilinear_map A M₁ M₂) :
⇑(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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
multilinear_map R (λ (i : ι₂), M₂) M₃
Transfer the arguments to a map along an equivalence between argument indices.
The naming is derived from finsupp.dom_congr, noting that here the permutation applies to the
domain of the domain.
@[simp]
theorem
multilinear_map.dom_dom_congr_apply
{R : Type u}
{M₂ : Type v₂}
{M₃ : Type v₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(m : multilinear_map R (λ (i : ι₁), M₂) M₃)
(v : ι₂ → M₂) :
⇑(multilinear_map.dom_dom_congr σ m) v = ⇑m (λ (i : ι₁), v (⇑σ i))
theorem
multilinear_map.dom_dom_congr_trans
{R : Type u}
{M₂ : Type v₂}
{M₃ : Type v₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
{ι₃ : Type u_3}
[decidable_eq ι₁]
[decidable_eq ι₂]
[decidable_eq ι₃]
(σ₁ : ι₁ ≃ ι₂)
(σ₂ : ι₂ ≃ ι₃)
(m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
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}
[decidable_eq ι₁]
(σ₁ σ₂ : 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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(m : multilinear_map R (λ (i : ι₁), M₂) M₃) :
def
multilinear_map.dom_dom_congr_equiv
{R : Type u}
{M₂ : Type v₂}
{M₃ : Type v₃}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[module R M₂]
[module R M₃]
{ι₁ : Type u_1}
{ι₂ : Type u_2}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂) :
multilinear_map R (λ (i : ι₁), M₂) M₃ ≃+ multilinear_map R (λ (i : ι₂), M₂) M₃
multilinear_map.dom_dom_congr as an equivalence.
This is declared separately because it does not work with dot notation.
Equations
- 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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(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₃}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
(g : M₂ →ₗ[R] M₃)
(f : multilinear_map R M₁ M₂) :
multilinear_map R M₁ M₃
Composing a multilinear map with a linear map gives again a multilinear map.
@[simp]
theorem
linear_map.coe_comp_multilinear_map
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
(g : M₂ →ₗ[R] M₃)
(f : multilinear_map R M₁ M₂) :
theorem
linear_map.comp_multilinear_map_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
{M₃ : Type v₃}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[module R M₃]
(g : M₂ →ₗ[R] M₃)
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i) :
⇑(g.comp_multilinear_map f) m = ⇑g (⇑f m)
@[simp]
theorem
linear_map.comp_multilinear_map_dom_dom_congr
{R : Type u}
{M₂ : Type v₂}
{M₃ : Type v₃}
{M' : Type v'}
[semiring R]
[add_comm_monoid M₂]
[add_comm_monoid M₃]
[add_comm_monoid M']
[module R M₂]
[module R M₃]
[module R M']
{ι₁ : Type u_1}
{ι₂ : Type u_2}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(g : M₂ →ₗ[R] M₃)
(f : multilinear_map R (λ (i : ι₁), M') M₂) :
theorem
multilinear_map.map_piecewise_smul
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(c : ι → R)
(m : Π (i : ι), M₁ i)
(s : finset ι) :
If one multiplies by c i the coordinates in a finset s, then the image under a multilinear
map is multiplied by ∏ i in s, c i. This is mainly an auxiliary statement to prove the result when
s = univ, given in map_smul_univ, although it can be useful in its own right as it does not
require the index set ι to be finite.
theorem
multilinear_map.map_smul_univ
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
[fintype ι]
(c : ι → R)
(m : Π (i : ι), M₁ i) :
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₂}
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
[fintype ι]
(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₂}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
{R' : Type u_1}
{A : Type u_2}
[monoid R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[distrib_mul_action R' M₂]
[module A M₂]
[smul_comm_class A R' M₂] :
distrib_mul_action R' (multilinear_map A M₁ M₂)
Equations
- multilinear_map.distrib_mul_action = {to_mul_action := {to_has_scalar := multilinear_map.has_scalar _inst_14, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}
@[protected, instance]
def
multilinear_map.module
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
{R' : Type u_1}
{A : Type u_2}
[semiring R']
[semiring A]
[Π (i : ι), module A (M₁ i)]
[module A M₂]
[module R' M₂]
[smul_comm_class A R' M₂] :
module R' (multilinear_map A M₁ M₂)
The space of multilinear maps over an algebra over R is a module over R, for the pointwise
addition and scalar multiplication.
Equations
- multilinear_map.module = {to_distrib_mul_action := multilinear_map.distrib_mul_action _inst_18, add_smul := _, zero_smul := _}
@[protected, instance]
def
multilinear_map.no_zero_smul_divisors
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₃ : Type v₃}
[decidable_eq ι]
[Π (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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(ᾰ : 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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂)
(ᾰ : 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}
[decidable_eq ι₁]
[decidable_eq ι₂]
(σ : ι₁ ≃ ι₂) :
multilinear_map A (λ (i : ι₁), M₂) M₃ ≃ₗ[R'] multilinear_map A (λ (i : ι₂), M₂) M₃
multilinear_map.dom_dom_congr as a linear_equiv.
Equations
- 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₂)
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
(σ : ι ≃ ι')
(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₂)
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
(σ : ι ≃ ι')
(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₂)
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
(σ : ι ≃ ι') :
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₂)
[decidable_eq ι]
[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 _inst_17, 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₂)
[decidable_eq ι]
[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₂)
[decidable_eq ι]
[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')
[decidable_eq ι]
[comm_semiring R]
(A : Type u_1)
[comm_semiring A]
[algebra R A]
[fintype ι] :
multilinear_map R (λ (i : ι), A) A
Given an R-algebra A, mk_pi_algebra is the multilinear map on A^ι associating
to m the product of all the m i.
See also multilinear_map.mk_pi_algebra_fin for a version that works with a non-commutative
algebra A but requires ι = fin n.
@[simp]
theorem
multilinear_map.mk_pi_algebra_apply
{R : Type u}
{ι : Type u'}
[decidable_eq ι]
[comm_semiring R]
{A : Type u_1}
[comm_semiring A]
[algebra R A]
[fintype ι]
(m : ι → A) :
⇑(multilinear_map.mk_pi_algebra R ι A) m = ∏ (i : ι), m i
@[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₂}
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ R)
(z : M₂) :
multilinear_map R M₁ M₂
Given an R-multilinear map f taking values in R, f.smul_right z is the map
sending m to f m • z.
Equations
- 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₂}
[decidable_eq ι]
[comm_semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ R)
(z : M₂)
(m : Π (i : ι), M₁ i) :
⇑(f.smul_right z) m = ⇑f m • z
@[protected]
def
multilinear_map.mk_pi_ring
(R : Type u)
(ι : Type u')
{M₂ : Type v₂}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M₂]
[module R M₂]
[fintype ι]
(z : M₂) :
multilinear_map R (λ (i : ι), R) M₂
The canonical multilinear map on R^ι when ι is finite, associating to m the product of
all the m i (multiplied by a fixed reference element z in the target module). See also
mk_pi_algebra for a more general version.
Equations
- 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₂}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M₂]
[module R M₂]
[fintype ι]
(z : M₂)
(m : ι → R) :
⇑(multilinear_map.mk_pi_ring R ι z) m = (∏ (i : ι), m i) • z
theorem
multilinear_map.mk_pi_ring_apply_one_eq_self
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M₂]
[module R M₂]
[fintype ι]
(f : multilinear_map R (λ (i : ι), R) M₂) :
multilinear_map.mk_pi_ring R ι (⇑f (λ (i : ι), 1)) = f
@[protected, instance]
def
multilinear_map.has_neg
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
has_neg (multilinear_map R M₁ M₂)
@[simp]
theorem
multilinear_map.neg_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
multilinear_map.has_sub
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
has_sub (multilinear_map R M₁ M₂)
@[simp]
theorem
multilinear_map.sub_apply
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f g : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i) :
@[protected, instance]
def
multilinear_map.add_comm_group
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂] :
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 := λ (n : ℕ) (f : multilinear_map R M₁ M₂), {to_fun := λ (m : Π (i : ι), M₁ i), n • ⇑f m, map_add' := _, map_smul' := _}, 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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι)
(x : M₁ i) :
⇑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₂}
[decidable_eq ι]
[semiring R]
[Π (i : ι), add_comm_group (M₁ i)]
[add_comm_group M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
(f : multilinear_map R M₁ M₂)
(m : Π (i : ι), M₁ i)
(i : ι)
(x y : M₁ i) :
⇑f (function.update m i (x - y)) = ⇑f (function.update m i x) - ⇑f (function.update m i y)
@[protected]
def
multilinear_map.pi_ring_equiv
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M₂]
[module R M₂]
[fintype ι] :
M₂ ≃ₗ[R] multilinear_map R (λ (i : ι), R) M₂
When ι is finite, multilinear maps on R^ι with values in M₂ are in bijection with M₂,
as such a multilinear map is completely determined by its value on the constant vector made of ones.
We register this bijection as a linear equivalence in multilinear_map.pi_ring_equiv.
Equations
- 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_8, map_add' := _, map_smul' := _, inv_fun := multilinear_map.curry_left _inst_8, 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_8, map_add' := _, map_smul' := _, inv_fun := multilinear_map.curry_right _inst_8, left_inv := _, right_inv := _}
def
multilinear_map.curry_sum
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
{M' : Type v'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')]
(f : multilinear_map R (λ (x : ι ⊕ ι'), M') M₂) :
multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)
A multilinear map on Π i : ι ⊕ ι', M' defines a multilinear map on Π i : ι, M'
taking values in the space of multilinear maps on Π i : ι', M'.
@[simp]
theorem
multilinear_map.curry_sum_apply
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
{M' : Type v'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')]
(f : multilinear_map R (λ (x : ι ⊕ ι'), M') M₂)
(u : ι → M')
(v : ι' → M') :
def
multilinear_map.uncurry_sum
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
{M' : Type v'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')]
(f : multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)) :
multilinear_map R (λ (x : ι ⊕ ι'), M') M₂
A multilinear map on Π i : ι, M' taking values in the space of multilinear maps
on Π i : ι', M' defines a multilinear map on Π i : ι ⊕ ι', M'.
@[simp]
theorem
multilinear_map.uncurry_sum_aux_apply
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
{M' : Type v'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')]
(f : multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂))
(u : ι ⊕ ι' → M') :
def
multilinear_map.curry_sum_equiv
(R : Type u)
(ι : Type u')
(M₂ : Type v₂)
(M' : Type v')
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
(ι' : Type u_1)
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')] :
multilinear_map R (λ (x : ι ⊕ ι'), M') M₂ ≃ₗ[R] multilinear_map R (λ (x : ι), M') (multilinear_map R (λ (x : ι'), M') M₂)
Linear equivalence between the space of multilinear maps on Π i : ι ⊕ ι', M' and the space
of multilinear maps on Π i : ι, M' taking values in the space of multilinear maps
on Π i : ι', M'.
Equations
- multilinear_map.curry_sum_equiv R ι M₂ M' ι' = {to_fun := multilinear_map.curry_sum (λ (a b : ι ⊕ ι'), _inst_10 a b), map_add' := _, map_smul' := _, inv_fun := multilinear_map.uncurry_sum (λ (a b : ι ⊕ ι'), _inst_10 a b), left_inv := _, right_inv := _}
@[simp]
theorem
multilinear_map.coe_curry_sum_equiv
{R : Type u}
{ι : Type u'}
{M₂ : Type v₂}
{M' : Type v'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')] :
⇑(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'}
[decidable_eq ι]
[comm_semiring R]
[add_comm_monoid M']
[add_comm_monoid M₂]
[module R M']
[module R M₂]
{ι' : Type u_1}
[decidable_eq ι']
[decidable_eq (ι ⊕ ι')] :
⇑((multilinear_map.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₂}
[decidable_eq ι]
[ring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[nonempty ι]
(f : multilinear_map R M₁ M₂)
(p : Π (i : ι), submodule R (M₁ i)) :
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₂}
[decidable_eq ι]
[ring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[nonempty ι]
(f : multilinear_map R M₁ M₂)
(p : Π (i : ι), submodule R (M₁ i)) :
The map is always nonempty. This lemma is needed to apply sub_mul_action.zero_mem.
def
multilinear_map.range
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[ring R]
[Π (i : ι), add_comm_monoid (M₁ i)]
[add_comm_monoid M₂]
[Π (i : ι), module R (M₁ i)]
[module R M₂]
[nonempty ι]
(f : multilinear_map R M₁ M₂) :
sub_mul_action R M₂
The range of a multilinear map, closed under scalar multiplication.
@[protected, instance]
def
multilinear_map.finite_dimensional
{R : Type u}
{ι : Type u'}
{M₁ : ι → Type v₁}
{M₂ : Type v₂}
[decidable_eq ι]
[fintype ι]
[field R]
[add_comm_group M₂]
[module R M₂]
[finite_dimensional R M₂]
[Π (i : ι), add_comm_group (M₁ i)]
[Π (i : ι), module R (M₁ i)]
[∀ (i : ι), finite_dimensional R (M₁ i)] :
finite_dimensional R (multilinear_map R M₁ M₂)