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

## Main definitions #

• MultilinearMap R M₁ M₂ is the space of multilinear maps from ∀ (i : ι), M₁ i to M₂.

• f.map_smul is the multiplicativity of the multilinear map f along each coordinate.

• f.map_add is the additivity of the multilinear map f along each coordinate.

• f.map_smul_univ expresses the multiplicativity of f over all coordinates at the same time, writing f (fun i => c i • m i) as (∏ i, c i) • f m.

• f.map_add_univ expresses the additivity of f over all coordinates at the same time, writing

f (m + m') as the sum over all subsets s of ι of f (s.piecewise m m').

• f.map_sum expresses f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ) as the sum of f (g₁ (r 1), ..., gₙ (r n)) where r ranges 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.curryLeft and f.curryRight respectively (with inverses f.uncurryLeft and f.uncurryRight). 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 multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

## 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 the i-th coordinate
• fixing a vector m : ∀j, M₁ j, and then modifying its i-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 DecidableEq ι term to appear somewhere in the statement of MultilinearMap.map_add' and MultilinearMap.map_smul'. Three possible choices are:

1. Requiring DecidableEq ι as an argument to MultilinearMap (as we did originally).
2. Using Classical.decEq ι in the statement of map_add' and map_smul'.
3. Quantifying over all possible DecidableEq ι instances in the statement of map_add' and map_smul'.

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

structure MultilinearMap (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Type (max (max uι v₁) v₂)

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

• toFun : ((i : ι) → M₁ i)M₂

The underlying multivariate function of a multilinear map.

• map_add' : ∀ [inst : ] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i), self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)

A multilinear map is additive in every argument.

• map_smul' : ∀ [inst : ] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), self.toFun (Function.update m i (c x)) = c self.toFun (Function.update m i x)

A multilinear map is compatible with scalar multiplication in every argument.

Instances For
theorem MultilinearMap.map_add' {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (self : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
self.toFun (Function.update m i (x + y)) = self.toFun (Function.update m i x) + self.toFun (Function.update m i y)

A multilinear map is additive in every argument.

theorem MultilinearMap.map_smul' {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (self : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
self.toFun (Function.update m i (c x)) = c self.toFun (Function.update m i x)

A multilinear map is compatible with scalar multiplication in every argument.

instance MultilinearMap.instFunLikeForall {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
FunLike (MultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
Equations
• MultilinearMap.instFunLikeForall = { coe := fun (f : MultilinearMap R M₁ M₂) => f.toFun, coe_injective' := }
@[simp]
theorem MultilinearMap.toFun_eq_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) :
f.toFun = f
@[simp]
theorem MultilinearMap.coe_mk {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : ((i : ι) → M₁ i)M₂) (h₁ : ∀ [inst : ] (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 : ] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c x)) = c f (Function.update m i x)) :
{ toFun := f, map_add' := h₁, map_smul' := h₂ } = f
theorem MultilinearMap.congr_fun {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {g : MultilinearMap R M₁ M₂} (h : f = g) (x : (i : ι) → M₁ i) :
f x = g x
theorem MultilinearMap.congr_arg {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {x : (i : ι) → M₁ i} {y : (i : ι) → M₁ i} (h : x = y) :
f x = f y
theorem MultilinearMap.coe_injective {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Function.Injective DFunLike.coe
theorem MultilinearMap.coe_inj {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {g : MultilinearMap R M₁ M₂} :
f = g f = g
theorem MultilinearMap.ext_iff {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {f' : MultilinearMap R M₁ M₂} :
f = f' ∀ (x : (i : ι) → M₁ i), f x = f' x
theorem MultilinearMap.ext {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {f : MultilinearMap R M₁ M₂} {f' : MultilinearMap R M₁ M₂} (H : ∀ (x : (i : ι) → M₁ i), f x = f' x) :
f = f'
@[simp]
theorem MultilinearMap.mk_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (h₁ : ∀ [inst : ] (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 : ] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (Function.update m i (c x)) = c f (Function.update m i x)) :
{ toFun := f, map_add' := h₁, map_smul' := h₂ } = f
@[simp]
theorem MultilinearMap.map_add {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
@[simp]
theorem MultilinearMap.map_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap 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 MultilinearMap.map_coord_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {m : (i : ι) → M₁ i} (i : ι) (h : m i = 0) :
f m = 0
@[simp]
theorem MultilinearMap.map_update_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) :
f (Function.update m i 0) = 0
@[simp]
theorem MultilinearMap.map_zero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] :
f 0 = 0
instance MultilinearMap.instAdd {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Equations
• MultilinearMap.instAdd = { add := fun (f f' : MultilinearMap R M₁ M₂) => { toFun := fun (x : (i : ι) → M₁ i) => f x + f' x, map_add' := , map_smul' := } }
@[simp]
theorem MultilinearMap.add_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (f' : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
(f + f') m = f m + f' m
instance MultilinearMap.instZero {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Zero (MultilinearMap R M₁ M₂)
Equations
• MultilinearMap.instZero = { zero := { toFun := fun (x : (i : ι) → M₁ i) => 0, map_add' := , map_smul' := } }
instance MultilinearMap.instInhabited {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Equations
• MultilinearMap.instInhabited = { default := 0 }
@[simp]
theorem MultilinearMap.zero_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (m : (i : ι) → M₁ i) :
0 m = 0
instance MultilinearMap.instSMul {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [] {R' : Type u_1} {A : Type u_2} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] :
SMul R' (MultilinearMap A M₁ M₂)
Equations
• MultilinearMap.instSMul = { smul := fun (c : R') (f : MultilinearMap A M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => c f m, map_add' := , map_smul' := } }
@[simp]
theorem MultilinearMap.smul_apply {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [] {R' : Type u_1} {A : Type u_2} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] (f : MultilinearMap A M₁ M₂) (c : R') (m : (i : ι) → M₁ i) :
(c f) m = c f m
theorem MultilinearMap.coe_smul {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [(i : ι) → AddCommMonoid (M₁ i)] [] {R' : Type u_1} {A : Type u_2} [Monoid R'] [] [(i : ι) → Module A (M₁ i)] [DistribMulAction R' M₂] [Module A M₂] [SMulCommClass A R' M₂] (c : R') (f : MultilinearMap A M₁ M₂) :
(c f) = c f
instance MultilinearMap.addCommMonoid {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Equations
@[simp]
theorem MultilinearMap.coeAddMonoidHom_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
∀ (a : MultilinearMap R M₁ M₂) (a_1 : (i : ι) → M₁ i), MultilinearMap.coeAddMonoidHom a a_1 = a a_1
def MultilinearMap.coeAddMonoidHom {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
MultilinearMap R M₁ M₂ →+ ((i : ι) → M₁ i)M₂

Coercion of a multilinear map to a function as an additive monoid homomorphism.

Equations
• MultilinearMap.coeAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
@[simp]
theorem MultilinearMap.coe_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {α : Type u_1} (f : αMultilinearMap R M₁ M₂) (s : ) :
(∑ as, f a) = as, (f a)
theorem MultilinearMap.sum_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {α : Type u_1} (f : αMultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) {s : } :
(∑ as, f a) m = as, (f a) m
@[simp]
theorem MultilinearMap.toLinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) :
(f.toLinearMap m i) x = f (Function.update m i x)
def MultilinearMap.toLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) :
M₁ i →ₗ[R] M₂

If f is a multilinear map, then f.toLinearMap 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.toLinearMap m i = { toFun := fun (x : M₁ i) => f (Function.update m i x), map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.prod_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) (m : (i : ι) → M₁ i) :
(f.prod g) m = (f m, g m)
def MultilinearMap.prod {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₃) :
MultilinearMap R M₁ (M₂ × M₃)

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

Equations
• f.prod g = { toFun := fun (m : (i : ι) → M₁ i) => (f m, g m), map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.pi_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → MultilinearMap R M₁ (M' i)) (m : (i : ι) → M₁ i) (i : ι') :
m i = (f i) m
def MultilinearMap.pi {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] {ι' : Type u_1} {M' : ι'Type u_2} [(i : ι') → AddCommMonoid (M' i)] [(i : ι') → Module R (M' i)] (f : (i : ι') → MultilinearMap R M₁ (M' i)) :
MultilinearMap R M₁ ((i : ι') → M' i)

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

Equations
• = { toFun := fun (m : (i : ι) → M₁ i) (i : ι') => (f i) m, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.ofSubsingleton_symm_apply_apply (R : Type uR) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [] [Module R M₂] [Module R M₃] [] (i : ι) (f : MultilinearMap R (fun (x : ι) => M₂) M₃) (x : M₂) :
((MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f) x = f fun (x_1 : ι) => x
@[simp]
theorem MultilinearMap.ofSubsingleton_apply_apply (R : Type uR) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [] [Module R M₂] [Module R M₃] [] (i : ι) (f : M₂ →ₗ[R] M₃) (x : ιM₂) :
((MultilinearMap.ofSubsingleton R M₂ M₃ i) f) x = f (x i)
def MultilinearMap.ofSubsingleton (R : Type uR) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [] [Module R M₂] [Module R M₃] [] (i : ι) :
(M₂ →ₗ[R] M₃) MultilinearMap R (fun (x : ι) => M₂) M₃

Equivalence between linear maps M₂ →ₗ[R] M₃ and one-multilinear maps.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MultilinearMap.constOfIsEmpty_apply (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (m : M₂) :
= Function.const ((i : ι) → M₁ i) m
def MultilinearMap.constOfIsEmpty (R : Type uR) {ι : Type uι} (M₁ : ιType v₁) {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (m : M₂) :
MultilinearMap R M₁ M₂

The constant map is multilinear when ι is empty.

Equations
• = { toFun := Function.const ((i : ι) → M₁ i) m, map_add' := , map_smul' := }
Instances For
def MultilinearMap.restr {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M₂] [Module R M'] {k : } {n : } (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (s : Finset (Fin n)) (hk : s.card = k) (z : M') :
MultilinearMap R (fun (x : Fin k) => M') M₂

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

Equations
• f.restr s hk z = { toFun := fun (v : Fin kM') => f fun (j : Fin n) => if h : j s then v ((s.orderIsoOfFin hk).symm j, h) else z, map_add' := , map_smul' := }
Instances For
theorem MultilinearMap.cons_add {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (x : M 0) (y : M 0) :
f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)

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

theorem MultilinearMap.cons_smul {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (c : R) (x : M 0) :
f (Fin.cons (c x) m) = c f (Fin.cons x m)

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

theorem MultilinearMap.snoc_add {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.castSucc) (x : M (Fin.last n)) (y : M (Fin.last n)) :
f (Fin.snoc m (x + y)) = f (Fin.snoc m x) + f (Fin.snoc m y)

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

theorem MultilinearMap.snoc_smul {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.castSucc) (c : R) (x : M (Fin.last n)) :
f (Fin.snoc m (c x)) = c f (Fin.snoc m x)

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

def MultilinearMap.compLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :
MultilinearMap 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.compLinearMap f.

Equations
• g.compLinearMap f = { toFun := fun (m : (i : ι) → M₁ i) => g fun (i : ι) => (f i) (m i), map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.compLinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (m : (i : ι) → M₁ i) :
(g.compLinearMap f) m = g fun (i : ι) => (f i) (m i)
theorem MultilinearMap.compLinearMap_assoc {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] {M₁'' : ιType u_2} [(i : ι) → AddCommMonoid (M₁'' i)] [(i : ι) → Module R (M₁'' i)] (g : MultilinearMap R M₁'' M₂) (f₁ : (i : ι) → M₁' i →ₗ[R] M₁'' i) (f₂ : (i : ι) → M₁ i →ₗ[R] M₁' i) :
(g.compLinearMap f₁).compLinearMap f₂ = g.compLinearMap fun (i : ι) => f₁ i ∘ₗ f₂ i

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

@[simp]
theorem MultilinearMap.zero_compLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :

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

@[simp]
theorem MultilinearMap.compLinearMap_id {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) :
(g.compLinearMap fun (x : ι) => LinearMap.id) = g

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

theorem MultilinearMap.compLinearMap_injective {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (hf : ∀ (i : ι), Function.Surjective (f i)) :
Function.Injective fun (g : MultilinearMap R M₁' M₂) => g.compLinearMap f

Composing with a family of surjective linear maps is injective.

theorem MultilinearMap.compLinearMap_inj {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (hf : ∀ (i : ι), Function.Surjective (f i)) (g₁ : MultilinearMap R M₁' M₂) (g₂ : MultilinearMap R M₁' M₂) :
g₁.compLinearMap f = g₂.compLinearMap f g₁ = g₂
@[simp]
theorem MultilinearMap.comp_linearEquiv_eq_zero_iff {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) (f : (i : ι) → M₁ i ≃ₗ[R] M₁' i) :
(g.compLinearMap fun (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 MultilinearMap.map_piecewise_add {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) (t : ) :
f (t.piecewise (m + m') m') = st.powerset, f (s.piecewise m m')

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

theorem MultilinearMap.map_add_univ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] [] (m : (i : ι) → M₁ i) (m' : (i : ι) → M₁ i) :
f (m + m') = s : , f (s.piecewise m m')

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

theorem MultilinearMap.map_sum_finset_aux {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) (A : (i : ι) → Finset (α i)) [] [] {n : } (h : i : ι, (A i).card = n) :
(f fun (i : ι) => jA i, g i j) = r, f fun (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 MultilinearMap.map_sum_finset {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) (A : (i : ι) → Finset (α i)) [] [] :
(f fun (i : ι) => jA i, g i j) = r, f fun (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 MultilinearMap.map_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : ιType u_1} (g : (i : ι) → α iM₁ i) [] [] [(i : ι) → Fintype (α i)] :
(f fun (i : ι) => j : α i, g i j) = r : (i : ι) → α i, f fun (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 MultilinearMap.map_update_sum {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) {α : Type u_2} [] (t : ) (i : ι) (g : αM₁ i) (m : (i : ι) → M₁ i) :
f (Function.update m i (∑ at, g a)) = at, f (Function.update m i (g a))
@[simp]
theorem MultilinearMap.codRestrict_apply_coe {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) (v : (i : ι) → M₁ i) :
((f.codRestrict p h) v) = f v
def MultilinearMap.codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :
MultilinearMap R M₁ { x : M₂ // x p }

Restrict the codomain of a multilinear map to a submodule.

This is the multilinear version of LinearMap.codRestrict.

Equations
• f.codRestrict p h = { toFun := fun (v : (i : ι) → M₁ i) => f v, , map_add' := , map_smul' := }
Instances For
def MultilinearMap.restrictScalars (R : Type uR) {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {A : Type u_1} [] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : MultilinearMap A M₁ M₂) :
MultilinearMap R M₁ M₂

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

Equations
• = { toFun := f, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.coe_restrictScalars (R : Type uR) {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {A : Type u_1} [] [SMul R A] [(i : ι) → Module A (M₁ i)] [Module A M₂] [∀ (i : ι), IsScalarTower R A (M₁ i)] [IsScalarTower R A M₂] (f : MultilinearMap A M₁ M₂) :
= f
@[simp]
theorem MultilinearMap.domDomCongr_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun (x : ι₁) => M₂) M₃) (v : ι₂M₂) :
v = m fun (i : ι₁) => v (σ i)
def MultilinearMap.domDomCongr {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun (x : ι₁) => M₂) M₃) :
MultilinearMap R (fun (x : ι₂) => M₂) M₃

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

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

Equations
• = { toFun := fun (v : ι₂M₂) => m fun (i : ι₁) => v (σ i), map_add' := , map_smul' := }
Instances For
theorem MultilinearMap.domDomCongr_trans {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (σ₁ : ι₁ ι₂) (σ₂ : ι₂ ι₃) (m : MultilinearMap R (fun (x : ι₁) => M₂) M₃) :
MultilinearMap.domDomCongr (σ₁.trans σ₂) m =
theorem MultilinearMap.domDomCongr_mul {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} (σ₁ : ) (σ₂ : ) (m : MultilinearMap R (fun (x : ι₁) => M₂) M₃) :
MultilinearMap.domDomCongr (σ₂ * σ₁) m =
@[simp]
theorem MultilinearMap.domDomCongrEquiv_symm_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun (x : ι₂) => M₂) M₃) :
.symm m = MultilinearMap.domDomCongr σ.symm m
@[simp]
theorem MultilinearMap.domDomCongrEquiv_apply {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (m : MultilinearMap R (fun (x : ι₁) => M₂) M₃) :
def MultilinearMap.domDomCongrEquiv {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
MultilinearMap R (fun (x : ι₁) => M₂) M₃ ≃+ MultilinearMap R (fun (x : ι₂) => M₂) M₃

MultilinearMap.domDomCongr as an equivalence.

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

Equations
• = { toFun := , invFun := , left_inv := , right_inv := , map_add' := }
Instances For
@[simp]
theorem MultilinearMap.domDomCongr_eq_iff {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} [] [] [] [Module R M₂] [Module R M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (f : MultilinearMap R (fun (x : ι₁) => M₂) M₃) (g : MultilinearMap R (fun (x : ι₁) => M₂) M₃) :
f = g

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

If {a // P a} is a subtype of ι and if we fix an element z of (i : {a // ¬ P a}) → M₁ i, then a multilinear map on M₁ defines a multilinear map on the restriction of M₁ to {a // P a}, by fixing the arguments out of {a // P a} equal to the values of z.

theorem MultilinearMap.domDomRestrict_aux {ι : Sort u_2} [] (P : ιProp) [] {M₁ : ιType u_1} [DecidableEq { a : ι // P a }] (x : (i : { a : ι // P a }) → M₁ i) (z : (i : { a : ι // ¬P a }) → M₁ i) (i : { a : ι // P a }) (c : M₁ i) :
(fun (j : ι) => if h : P j then Function.update x i c j, h else z j, h) = Function.update (fun (j : ι) => if h : P j then x j, h else z j, h) (↑i) c
theorem MultilinearMap.domDomRestrict_aux_right {ι : Sort u_2} [] (P : ιProp) [] {M₁ : ιType u_1} [DecidableEq { a : ι // ¬P a }] (x : (i : { a : ι // P a }) → M₁ i) (z : (i : { a : ι // ¬P a }) → M₁ i) (i : { a : ι // ¬P a }) (c : M₁ i) :
(fun (j : ι) => if h : P j then x j, h else Function.update z i c j, h) = Function.update (fun (j : ι) => if h : P j then x j, h else z j, h) (↑i) c
def MultilinearMap.domDomRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (P : ιProp) [] (z : (i : { a : ι // ¬P a }) → M₁ i) :
MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂

Given a multilinear map f on (i : ι) → M i, a (decidable) predicate P on ι and an element z of (i : {a // ¬ P a}) → M₁ i, construct a multilinear map on (i : {a // P a}) → M₁ i) whose value at x is f evaluated at the vector with ith coordinate x i if P i and z i otherwise.

The naming is similar to MultilinearMap.domDomCongr: here we are applying the restriction to the domain of the domain.

For a linear map version, see MultilinearMap.domDomRestrictₗ.

Equations
• f.domDomRestrict P z = { toFun := fun (x : (i : { a : ι // P a }) → M₁ i) => f fun (j : ι) => if h : P j then x j, h else z j, h, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.domDomRestrict_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (P : ιProp) [] (x : (i : { a : ι // P a }) → M₁ i) (z : (i : { a : ι // ¬P a }) → M₁ i) :
(f.domDomRestrict P z) x = f fun (j : ι) => if h : P j then x j, h else z j, h
def MultilinearMap.linearDeriv {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] [] (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i) :
((i : ι) → M₁ i) →ₗ[R] M₂

The "derivative" of a multilinear map, as a linear map from (i : ι) → M₁ i to M₂. For continuous multilinear maps, this will indeed be the derivative.

Equations
• f.linearDeriv x = i : ι, f.toLinearMap x i ∘ₗ
Instances For
@[simp]
theorem MultilinearMap.linearDeriv_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] [] (f : MultilinearMap R M₁ M₂) (x : (i : ι) → M₁ i) (y : (i : ι) → M₁ i) :
(f.linearDeriv x) y = i : ι, f (Function.update x i (y i))
def LinearMap.compMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
MultilinearMap R M₁ M₃

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

Equations
• g.compMultilinearMap f = { toFun := g f, map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.coe_compMultilinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
(g.compMultilinearMap f) = g f
@[simp]
theorem LinearMap.compMultilinearMap_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
(g.compMultilinearMap f) m = g (f m)
@[simp]
theorem LinearMap.subtype_compMultilinearMap_codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (p : Submodule R M₂) (h : ∀ (v : (i : ι) → M₁ i), f v p) :
p.subtype.compMultilinearMap (f.codRestrict p h) = f

The multilinear version of LinearMap.subtype_comp_codRestrict

@[simp]
theorem LinearMap.compMultilinearMap_codRestrict {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} {M₃ : Type v₃} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [Module R M₃] (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (p : Submodule R M₃) (h : ∀ (c : M₂), g c p) :
.compMultilinearMap f = (g.compMultilinearMap f).codRestrict p

The multilinear version of LinearMap.comp_codRestrict

@[simp]
theorem LinearMap.compMultilinearMap_domDomCongr {R : Type uR} {M₂ : Type v₂} {M₃ : Type v₃} {M' : Type v'} [] [] [] [] [Module R M₂] [Module R M₃] [Module R M'] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R (fun (x : ι₁) => M') M₂) :
MultilinearMap.domDomCongr σ (g.compMultilinearMap f) = g.compMultilinearMap
instance MultilinearMap.instDistribMulActionOfSMulCommClass {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [] [] [Module R M₂] [SMulCommClass R S M₂] :
Equations
instance MultilinearMap.instModule {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] :
Module S (MultilinearMap R 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
instance MultilinearMap.instNoZeroSMulDivisors {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] [] :
Equations
• =
@[simp]
theorem MultilinearMap.ofSubsingletonₗ_symm_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃] [] (i : ι) :
∀ (a : MultilinearMap R (fun (x : ι) => M₂) M₃), (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i).symm a = (MultilinearMap.ofSubsingleton R M₂ M₃ i).symm a
@[simp]
theorem MultilinearMap.ofSubsingletonₗ_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃] [] (i : ι) :
∀ (a : M₂ →ₗ[R] M₃), (MultilinearMap.ofSubsingletonₗ R S M₂ M₃ i) a = (MultilinearMap.ofSubsingleton R M₂ M₃ i) a
def MultilinearMap.ofSubsingletonₗ (R : Type uR) (S : Type uS) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃] [] (i : ι) :
(M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun (x : ι) => M₂) M₃

Linear equivalence between linear maps M₂ →ₗ[R] M₃ and one-multilinear maps MultilinearMap R (fun _ : ι ↦ M₂) M₃.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MultilinearMap.domDomCongrLinearEquiv'_symm_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') (f : MultilinearMap R (fun (i : ι') => M₁ (σ.symm i)) M₂) :
.symm f = { toFun := f (Equiv.piCongrLeft' M₁ σ), map_add' := , map_smul' := }
@[simp]
theorem MultilinearMap.domDomCongrLinearEquiv'_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') (f : MultilinearMap R M₁ M₂) :
f = { toFun := f (Equiv.piCongrLeft' M₁ σ).symm, map_add' := , map_smul' := }
def MultilinearMap.domDomCongrLinearEquiv' (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] {ι' : Type u_1} (σ : ι ι') :
MultilinearMap R M₁ M₂ ≃ₗ[S] MultilinearMap R (fun (i : ι') => M₁ (σ.symm i)) M₂

The dependent version of MultilinearMap.domDomCongrLinearEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MultilinearMap.constLinearEquivOfIsEmpty_symm_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] [] (f : MultilinearMap R M₁ M₂) :
.symm f = f 0
@[simp]
theorem MultilinearMap.constLinearEquivOfIsEmpty_apply (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] [] (m : M₂) :
m =
def MultilinearMap.constLinearEquivOfIsEmpty (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ιType v₁) (M₂ : Type v₂) [] [(i : ι) → AddCommMonoid (M₁ i)] [(i : ι) → Module R (M₁ i)] [] [Module R M₂] [] [Module S M₂] [SMulCommClass R S M₂] [] :
M₂ ≃ₗ[S] MultilinearMap 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
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MultilinearMap.domDomCongrLinearEquiv_apply (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
∀ (a : MultilinearMap R (fun (x : ι₁) => M₂) M₃), a = .toFun a
@[simp]
theorem MultilinearMap.domDomCongrLinearEquiv_symm_apply (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
∀ (a : MultilinearMap R (fun (x : ι₂) => M₂) M₃), .symm a = .invFun a
def MultilinearMap.domDomCongrLinearEquiv (R : Type uR) (S : Type uS) (M₂ : Type v₂) (M₃ : Type v₃) [] [] [Module R M₂] [] [] [Module R M₃] [Module S M₃] [SMulCommClass R S M₃] {ι₁ : Type u_1} {ι₂ : Type u_2} (σ : ι₁ ι₂) :
MultilinearMap R (fun (x : ι₁) => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun (x : ι₂) => M₂) M₃

MultilinearMap.domDomCongr as a LinearEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MultilinearMap.domDomRestrictₗ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (P : ιProp) [] :
MultilinearMap R (fun (i : { a : ι // ¬P a }) => M₁ i) (MultilinearMap R (fun (i : { a : ι // P a }) => M₁ i) M₂)

Given a predicate P, one may associate to a multilinear map f a multilinear map from the elements satisfying P to the multilinear maps on elements not satisfying P. In other words, splitting the variables into two subsets one gets a multilinear map into multilinear maps. This is a linear map version of the function MultilinearMap.domDomRestrict.

Equations
• f.domDomRestrictₗ P = { toFun := fun (z : (i : { a : ι // ¬P a }) → M₁ i) => f.domDomRestrict P z, map_add' := , map_smul' := }
Instances For
theorem MultilinearMap.iteratedFDeriv_aux {ι : Type u_4} {M₁ : ιType u_2} {α : Type u_3} [] (s : Set ι) [DecidableEq { x : ι // x s }] (e : α s) (m : α(i : ι) → M₁ i) (a : α) (z : (i : ι) → M₁ i) :
(fun (i : s) => Function.update m a z (e.symm i) i) = fun (i : s) => Function.update (fun (j : s) => m (e.symm j) j) (e a) (z (e a)) i
noncomputable def MultilinearMap.iteratedFDerivComponent {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {α : Type u_2} (f : MultilinearMap R M₁ M₂) {s : Set ι} (e : α s) [DecidablePred fun (x : ι) => x s] :
MultilinearMap R (fun (i : { a : ι // as }) => M₁ i) (MultilinearMap R (fun (x : α) => (i : ι) → M₁ i) M₂)

One of the components of the iterated derivative of a multilinear map. Given a bijection e between a type α (typically Fin k) and a subset s of ι, this component is a multilinear map of k vectors v₁, ..., vₖ, mapping them to f (x₁, (v_{e.symm 2})₂, x₃, ...), where at indices i in s one uses the i-th coordinate of the vector v_{e.symm i} and otherwise one uses the i-th coordinate of a reference vector x. This is multilinear in the components of x outside of s, and in the v_j.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def MultilinearMap.iteratedFDeriv {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (f : MultilinearMap R M₁ M₂) (k : ) (x : (i : ι) → M₁ i) :
MultilinearMap R (fun (x : Fin k) => (i : ι) → M₁ i) M₂

The k-th iterated derivative of a multilinear map f at the point x. It is a multilinear map of k vectors v₁, ..., vₖ (with the same type as x), mapping them to ∑ f (x₁, (v_{i₁})₂, x₃, ...), where at each index j one uses either xⱼ or one of the (vᵢ)ⱼ, and each vᵢ has to be used exactly once. The sum is parameterized by the embeddings of Fin k in the index type ι (or, equivalently, by the subsets s of ι of cardinality k and then the bijections between Fin k and s).

For the continuous version, see ContinuousMultilinearMap.iteratedFDeriv.

Equations
• f.iteratedFDeriv k x = e : Fin k ι, (f.iteratedFDerivComponent e.toEquivRange) fun (i : { a : ι // a }) => x i
Instances For
@[simp]
theorem MultilinearMap.compLinearMapₗ_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) (g : MultilinearMap R M₁' M₂) :
= g.compLinearMap f
def MultilinearMap.compLinearMapₗ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :
MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂

If f is a collection of linear maps, then the construction MultilinearMap.compLinearMap sending a multilinear map g to g (f₁ ⬝ , ..., fₙ ⬝ ) is linear in g.

Equations
• = { toFun := fun (g : MultilinearMap R M₁' M₂) => g.compLinearMap f, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.compLinearMapMultilinear_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (f : (i : ι) → M₁ i →ₗ[R] M₁' i) :
MultilinearMap.compLinearMapMultilinear f =
def MultilinearMap.compLinearMapMultilinear {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] :
MultilinearMap R (fun (i : ι) => M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)

If f is a collection of linear maps, then the construction MultilinearMap.compLinearMap sending a multilinear map g to g (f₁ ⬝ , ..., fₙ ⬝ ) is linear in g and multilinear in f₁, ..., fₙ.

Equations
• MultilinearMap.compLinearMapMultilinear = { toFun := MultilinearMap.compLinearMapₗ, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.piLinearMap_apply_apply_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] (g : MultilinearMap R M₁' M₂) :
∀ (a : (i : ι) → (fun (i : ι) => M₁ i →ₗ[R] M₁' i) i) (m : (i : ι) → M₁ i), ((MultilinearMap.piLinearMap g) a) m = g fun (i : ι) => (a i) (m i)
def MultilinearMap.piLinearMap {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] {M₁' : ιType u_1} [(i : ι) → AddCommMonoid (M₁' i)] [(i : ι) → Module R (M₁' i)] :
MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R (fun (i : ι) => M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂)

Let M₁ᵢ and M₁ᵢ' be two families of R-modules and M₂ an R-module. Let us denote Π i, M₁ᵢ and Π i, M₁ᵢ' by M and M' respectively. If g is a multilinear map M' → M₂, then g can be reinterpreted as a multilinear map from Π i, M₁ᵢ ⟶ M₁ᵢ' to M ⟶ M₂ via (fᵢ) ↦ v ↦ g(fᵢ vᵢ).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem MultilinearMap.map_piecewise_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (c : ιR) (m : (i : ι) → M₁ i) (s : ) :
f (s.piecewise (fun (i : ι) => c i m i) m) = (∏ is, c i) f m

If one multiplies by c i the coordinates in a finset s, then the image under a multilinear map is multiplied by ∏ i ∈ 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 MultilinearMap.map_smul_univ {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (c : ιR) (m : (i : ι) → M₁ i) :
(f fun (i : ι) => c i m i) = (∏ i : ι, c i) f m

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

@[simp]
theorem MultilinearMap.map_update_smul {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] [] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i) :
f (Function.update (c m) i x) = c ^ ( - 1) f (Function.update m i x)
def MultilinearMap.mkPiAlgebra (R : Type uR) (ι : Type uι) [] (A : Type u_1) [] [Algebra R A] [] :
MultilinearMap R (fun (x : ι) => A) A

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

See also MultilinearMap.mkPiAlgebraFin for a version that works with a non-commutative algebra A but requires ι = Fin n.

Equations
• = { toFun := fun (m : ιA) => i : ι, m i, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.mkPiAlgebra_apply {R : Type uR} {ι : Type uι} [] {A : Type u_1} [] [Algebra R A] [] (m : ιA) :
m = i : ι, m i
def MultilinearMap.mkPiAlgebraFin (R : Type uR) (n : ) [] (A : Type u_1) [] [Algebra R A] :
MultilinearMap R (fun (x : Fin n) => A) A

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

See also MultilinearMap.mkPiAlgebra for a version that assumes [CommSemiring A] but works for A^ι with any finite type ι.

Equations
• = { toFun := fun (m : Fin nA) => (List.ofFn m).prod, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.mkPiAlgebraFin_apply {R : Type uR} {n : } [] {A : Type u_1} [] [Algebra R A] (m : Fin nA) :
m = (List.ofFn m).prod
theorem MultilinearMap.mkPiAlgebraFin_apply_const {R : Type uR} {n : } [] {A : Type u_1} [] [Algebra R A] (a : A) :
( fun (x : Fin n) => a) = a ^ n
def MultilinearMap.smulRight {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ R) (z : M₂) :
MultilinearMap R M₁ M₂

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

Equations
• f.smulRight z = (LinearMap.id.smulRight z).compMultilinearMap f
Instances For
@[simp]
theorem MultilinearMap.smulRight_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ R) (z : M₂) (m : (i : ι) → M₁ i) :
(f.smulRight z) m = f m z
def MultilinearMap.mkPiRing (R : Type uR) (ι : Type uι) {M₂ : Type v₂} [] [] [Module R M₂] [] (z : M₂) :
MultilinearMap R (fun (x : ι) => 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 mkPiAlgebra for a more general version.

Equations
• = .smulRight z
Instances For
@[simp]
theorem MultilinearMap.mkPiRing_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] (z : M₂) (m : ιR) :
m = (∏ i : ι, m i) z
theorem MultilinearMap.mkPiRing_apply_one_eq_self {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] (f : MultilinearMap R (fun (x : ι) => R) M₂) :
MultilinearMap.mkPiRing R ι (f fun (x : ι) => 1) = f
theorem MultilinearMap.mkPiRing_eq_iff {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] {z₁ : M₂} {z₂ : M₂} :
= z₁ = z₂
theorem MultilinearMap.mkPiRing_zero {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] :
= 0
theorem MultilinearMap.mkPiRing_eq_zero_iff {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] (z : M₂) :
= 0 z = 0
instance MultilinearMap.instNeg {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Neg (MultilinearMap R M₁ M₂)
Equations
• MultilinearMap.instNeg = { neg := fun (f : MultilinearMap R M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => -f m, map_add' := , map_smul' := } }
@[simp]
theorem MultilinearMap.neg_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
(-f) m = -f m
instance MultilinearMap.instSub {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Sub (MultilinearMap R M₁ M₂)
Equations
• MultilinearMap.instSub = { sub := fun (f g : MultilinearMap R M₁ M₂) => { toFun := fun (m : (i : ι) → M₁ i) => f m - g m, map_add' := , map_smul' := } }
@[simp]
theorem MultilinearMap.sub_apply {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) (g : MultilinearMap R M₁ M₂) (m : (i : ι) → M₁ i) :
(f - g) m = f m - g m
instance MultilinearMap.instAddCommGroup {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] :
Equations
@[simp]
theorem MultilinearMap.map_neg {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap 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 MultilinearMap.map_sub {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (m : (i : ι) → M₁ i) (i : ι) (x : M₁ i) (y : M₁ i) :
f (Function.update m i (x - y)) = f (Function.update m i x) - f (Function.update m i y)
theorem MultilinearMap.map_update {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (x : (i : ι) → M₁ i) (i : ι) (v : M₁ i) :
f (Function.update x i v) = f x - f (Function.update x i (x i - v))
theorem MultilinearMap.map_sub_map_piecewise {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (a : (i : ι) → M₁ i) (b : (i : ι) → M₁ i) (s : ) :
f a - f (s.piecewise b a) = is, f fun (j : ι) => if j sj < i then a j else if i = j then a j - b j else b j
theorem MultilinearMap.map_piecewise_sub_map_piecewise {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] (a : (i : ι) → M₁ i) (b : (i : ι) → M₁ i) (v : (i : ι) → M₁ i) (s : ) :
f (s.piecewise a v) - f (s.piecewise b v) = is, f fun (j : ι) => if j s then if j < i then a j else if j = i then a j - b j else b j else v j

This calculates the differences between the values of a multilinear map at two arguments that differ on a finset s of ι. It requires a linear order on ι in order to express the result.

theorem MultilinearMap.map_add_eq_map_add_linearDeriv_add {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] [] (x : (i : ι) → M₁ i) (h : (i : ι) → M₁ i) :
f (x + h) = f x + (f.linearDeriv x) h + sFinset.filter (fun (x : ) => 2 x.card) Finset.univ.powerset, f (s.piecewise h x)
theorem MultilinearMap.map_add_sub_map_add_sub_linearDeriv {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [] [(i : ι) → AddCommGroup (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] (f : MultilinearMap R M₁ M₂) [] [] (x : (i : ι) → M₁ i) (h : (i : ι) → M₁ i) (h' : (i : ι) → M₁ i) :
f (x + h) - f (x + h') - (f.linearDeriv x) (h - h') = sFinset.filter (fun (x : ) => 2 x.card) Finset.univ.powerset, (f (s.piecewise h x) - f (s.piecewise h' x))

This expresses the difference between the values of a multilinear map at two points "close to x" in terms of the "derivative" of the multilinear map at x and of "second-order" terms.

def MultilinearMap.piRingEquiv {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [] [] [Module R M₂] [] :
M₂ ≃ₗ[R] MultilinearMap R (fun (x : ι) => 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 MultilinearMap.piRingEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For

### Currying #

We associate to a multilinear map in n+1 variables (i.e., based on Fin n.succ) two curried functions, named f.curryLeft (which is a linear map on E 0 taking values in multilinear maps in n variables) and f.curryRight (which 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 uncurryLeft and uncurryRight.

We also register linear equiv versions of these correspondences, in multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

#### Left currying #

def LinearMap.uncurryLeft {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) :

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

Equations
• f.uncurryLeft = { toFun := fun (m : (i : Fin n.succ) → M i) => (f (m 0)) (Fin.tail m), map_add' := , map_smul' := }
Instances For
@[simp]
theorem LinearMap.uncurryLeft_apply {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) (m : (i : Fin n.succ) → M i) :
f.uncurryLeft m = (f (m 0)) (Fin.tail m)
def MultilinearMap.curryLeft {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂

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

Equations
• f.curryLeft = { toFun := fun (x : M 0) => { toFun := fun (m : (i : Fin n) → M i.succ) => f (Fin.cons x m), map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.curryLeft_apply {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (x : M 0) (m : (i : Fin n) → M i.succ) :
(f.curryLeft x) m = f (Fin.cons x m)
@[simp]
theorem LinearMap.curry_uncurryLeft {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) :
f.uncurryLeft.curryLeft = f
@[simp]
theorem MultilinearMap.uncurry_curryLeft {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
f.curryLeft.uncurryLeft = f
def multilinearCurryLeftEquiv (R : Type uR) {n : } (M : Fin n.succType v) (M₂ : Type v₂) [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] :
MultilinearMap R M M₂ ≃ₗ[R] M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) 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 multilinearCurryLeftEquiv R M M₂.

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

Equations
• = { toFun := MultilinearMap.curryLeft, map_add' := , map_smul' := , invFun := LinearMap.uncurryLeft, left_inv := , right_inv := }
Instances For

#### Right currying #

def MultilinearMap.uncurryRight {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) :

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

Equations
• f.uncurryRight = { toFun := fun (m : (i : Fin n.succ) → M i) => (f (Fin.init m)) (m (Fin.last n)), map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.uncurryRight_apply {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) (m : (i : Fin n.succ) → M i) :
f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))
def MultilinearMap.curryRight {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MultilinearMap.curryRight_apply {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.castSucc) (x : M (Fin.last n)) :
(f.curryRight m) x = f (Fin.snoc m x)
@[simp]
theorem MultilinearMap.curry_uncurryRight {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) :
f.uncurryRight.curryRight = f
@[simp]
theorem MultilinearMap.uncurry_curryRight {R : Type uR} {n : } {M : Fin n.succType v} {M₂ : Type v₂} [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) :
f.curryRight.uncurryRight = f
def multilinearCurryRightEquiv (R : Type uR) {n : } (M : Fin n.succType v) (M₂ : Type v₂) [] [(i : Fin n.succ) → AddCommMonoid (M i)] [] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] :
MultilinearMap R M M₂ ≃ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] 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 (castSucc i) to the space of linear maps on M (last n), by separating the last variable. We register this isomorphism as a linear isomorphism in multilinearCurryRightEquiv R M M₂.

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

Equations
• = { toFun := MultilinearMap.curryRight, map_add' := , map_smul' := , invFun := MultilinearMap.uncurryRight, left_inv := , right_inv := }
Instances For
def MultilinearMap.currySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι ι') => M') M₂) :
MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)

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

Equations
• f.currySum = { toFun := fun (u : ιM') => { toFun := fun (v : ι'M') => f (Sum.elim u v), map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.currySum_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι ι') => M') M₂) (u : ιM') (v : ι'M') :
(f.currySum u) v = f (Sum.elim u v)
def MultilinearMap.uncurrySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)) :
MultilinearMap R (fun (x : ι ι') => M') M₂

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

Equations
• f.uncurrySum = { toFun := fun (u : ι ι'M') => (f (u Sum.inl)) (u Sum.inr), map_add' := , map_smul' := }
Instances For
@[simp]
theorem MultilinearMap.uncurrySum_aux_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)) (u : ι ι'M') :
f.uncurrySum u = (f (u Sum.inl)) (u Sum.inr)
def MultilinearMap.currySumEquiv (R : Type uR) (ι : Type uι) (M₂ : Type v₂) (M' : Type v') [] [] [] [Module R M'] [Module R M₂] (ι' : Type u_1) :
MultilinearMap R (fun (x : ι ι') => M') M₂ ≃ₗ[R] MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (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
• MultilinearMap.currySumEquiv R ι M₂ M' ι' = { toFun := MultilinearMap.currySum, map_add' := , map_smul' := , invFun := MultilinearMap.uncurrySum, left_inv := , right_inv := }
Instances For
@[simp]
theorem MultilinearMap.coe_currySumEquiv {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} :
(MultilinearMap.currySumEquiv R ι M₂ M' ι') = MultilinearMap.currySum
@[simp]
theorem MultilinearMap.coe_currySumEquiv_symm {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {ι' : Type u_1} :
(MultilinearMap.currySumEquiv R ι M₂ M' ι').symm = MultilinearMap.uncurrySum
def MultilinearMap.curryFinFinset (R : Type uR) (M₂ : Type v₂) (M' : Type v') [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) :
MultilinearMap R (fun (x : Fin n) => M') M₂ ≃ₗ[R] MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (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 fun i : Fin n => M' is isomorphic to the space of multilinear maps on fun i : Fin k => M' taking values in the space of multilinear maps on fun i : Fin l => M'.

Equations
Instances For
@[simp]
theorem MultilinearMap.curryFinFinset_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (mk : Fin kM') (ml : Fin lM') :
(((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) mk) ml = f fun (i : Fin n) => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)
@[simp]
theorem MultilinearMap.curryFinFinset_symm_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (m : Fin nM') :
((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) m = (f fun (i : Fin k) => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun (i : Fin l) => m ((finSumEquivOfFinset hk hl) (Sum.inr i))
theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (x : M') (y : M') :
((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y) = (f fun (x_1 : Fin k) => x) fun (x : Fin l) => y
@[simp]
theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const_aux {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (x : M') (y : M') :
((f fun (x_1 : Fin k) => x) fun (i : Fin l) => s.piecewise (fun (x_1 : Fin n) => x) (fun (x : Fin n) => y) ((s.orderEmbOfFin hl) i)) = (f fun (x_1 : Fin k) => x) fun (x : Fin l) => y
@[simp]
theorem MultilinearMap.curryFinFinset_symm_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (x : M') :
(((MultilinearMap.curryFinFinset R M₂ M' hk hl).symm f) fun (x_1 : Fin n) => x) = (f fun (x_1 : Fin k) => x) fun (x_1 : Fin l) => x
theorem MultilinearMap.curryFinFinset_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (x : M') (y : M') :
((((MultilinearMap.curryFinFinset R M₂ M' hk hl) f) fun (x_1 : Fin k) => x) fun (x : Fin l) => y) = f (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)
@[simp]
theorem MultilinearMap.curryFinFinset_apply_const_aux {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [] [] [] [Module R M'] [Module R M₂] {k : } {l : } {n : } {s : Finset (Fin n)} (hk : s.card = k) (hl : s.card = l) (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (x : M') (y : M') :
(f fun (i : Fin n) => Sum.elim (fun (x_1 : Fin k) => x) (fun (x : Fin l) => y) ((finSumEquivOfFinset hk hl).symm i)) = f (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)
def MultilinearMap.map {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)) :

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

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

Equations
• f.map p = { carrier := f '' {v : (i : ι) → M₁ i | ∀ (i : ι), v i p i}, smul_mem' := }
Instances For
theorem MultilinearMap.map_nonempty {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)) :
(↑(f.map p)).Nonempty

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

def MultilinearMap.range {R : Type uR} {ι : Type uι} {M₁ : ιType v₁} {M₂ : Type v₂} [Ring R] [(i : ι) → AddCommMonoid (M₁ i)] [] [(i : ι) → Module R (M₁ i)] [Module R M₂] [] (f : MultilinearMap R M₁ M₂) :

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

Equations
• f.range = f.map fun (x : ι) =>
Instances For