mathlib documentation

topology.algebra.multilinear

Continuous multilinear maps

We define continuous multilinear maps as maps from Π(i : ι), M₁ i to M₂ which are multilinear and continuous, by extending the space of multilinear maps with a continuity assumption. Here, M₁ i and M₂ are modules over a ring R, and ι is an arbitrary type, and all these spaces are also topological spaces.

Main definitions

Implementation notes

We mostly follow the API of multilinear maps.

Notation

We introduce the notation M [×n]→L[R] M' for the space of continuous n-multilinear maps from M^n to M'. This is a particular case of the general notion (where we allow varying dependent types as the arguments of our continuous multilinear maps), but arguably the most important one, especially when defining iterated derivatives.

structure continuous_multilinear_map (R : Type u) {ι : Type v} (M₁ : ι → Type w₁) (M₂ : Type w₂) [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] :
Type (max v w₁ w₂)

Continuous multilinear maps over the ring R, from Πi, M₁ i to M₂ where M₁ i and M₂ are modules over R with a topological structure. In applications, there will be compatibility conditions between the algebraic and the topological structures, but this is not needed for the definition.

@[instance]
def continuous_multilinear_map.has_coe_to_fun {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] :

Equations
theorem continuous_multilinear_map.coe_continuous {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) :

@[simp]
theorem continuous_multilinear_map.coe_coe {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) :

theorem continuous_multilinear_map.to_multilinear_map_inj {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] :

@[ext]
theorem continuous_multilinear_map.ext {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] {f f' : continuous_multilinear_map R M₁ M₂} :
(∀ (x : Π (i : ι), M₁ i), f x = f' x)f = f'

@[simp]
theorem continuous_multilinear_map.map_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_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 continuous_multilinear_map.map_smul {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_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 continuous_multilinear_map.map_coord_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) {m : Π (i : ι), M₁ i} (i : ι) :
m i = 0f m = 0

@[simp]
theorem continuous_multilinear_map.map_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) [nonempty ι] :
f 0 = 0

@[instance]
def continuous_multilinear_map.has_zero {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] :

Equations
@[instance]
def continuous_multilinear_map.inhabited {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.zero_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (m : Π (i : ι), M₁ i) :
0 m = 0

@[instance]
def continuous_multilinear_map.has_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [has_continuous_add M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.add_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f f' : continuous_multilinear_map R M₁ M₂) [has_continuous_add M₂] (m : Π (i : ι), M₁ i) :
(f + f') m = f m + f' m

@[instance]
def continuous_multilinear_map.add_comm_monoid {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [has_continuous_add M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.sum_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [has_continuous_add M₂] {α : Type u_1} (f : α → continuous_multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) {s : finset α} :
(∑ (a : α) in s, f a) m = ∑ (a : α) in s, (f a) m

def continuous_multilinear_map.to_continuous_linear_map {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) (m : Π (i : ι), M₁ i) (i : ι) :
M₁ i →L[R] M₂

If f is a continuous multilinear map, then f.to_continuous_linear_map m i is the continuous linear map obtained by fixing all coordinates but i equal to those of m, and varying the i-th coordinate.

Equations
def continuous_multilinear_map.prod {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_space M₃] :
continuous_multilinear_map R M₁ M₂continuous_multilinear_map R M₁ M₃continuous_multilinear_map R M₁ (M₂ × M₃)

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

Equations
@[simp]
theorem continuous_multilinear_map.prod_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [add_comm_monoid M₃] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [semimodule R M₃] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_space M₃] (f : continuous_multilinear_map R M₁ M₂) (g : continuous_multilinear_map R M₁ M₃) (m : Π (i : ι), M₁ i) :
(f.prod g) m = (f m, g m)

def continuous_multilinear_map.comp_continuous_linear_map {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₁' : ι → Type w₁'} {M₄ : Type w₄} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), add_comm_monoid (M₁' i)] [add_comm_monoid M₄] [Π (i : ι), semimodule R (M₁ i)] [Π (i : ι), semimodule R (M₁' i)] [semimodule R M₄] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), topological_space (M₁' i)] [topological_space M₄] :
continuous_multilinear_map R M₁' M₄(Π (i : ι), M₁ i →L[R] M₁' i)continuous_multilinear_map R M₁ M₄

If g is continuous multilinear and f is a collection of continuous linear maps, then g (f₁ m₁, ..., fₙ mₙ) is again a continuous multilinear map, that we call g.comp_continuous_linear_map f.

Equations
@[simp]
theorem continuous_multilinear_map.comp_continuous_linear_map_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₁' : ι → Type w₁'} {M₄ : Type w₄} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [Π (i : ι), add_comm_monoid (M₁' i)] [add_comm_monoid M₄] [Π (i : ι), semimodule R (M₁ i)] [Π (i : ι), semimodule R (M₁' i)] [semimodule R M₄] [Π (i : ι), topological_space (M₁ i)] [Π (i : ι), topological_space (M₁' i)] [topological_space M₄] (g : continuous_multilinear_map R M₁' M₄) (f : Π (i : ι), M₁ i →L[R] M₁' i) (m : Π (i : ι), M₁ i) :
(g.comp_continuous_linear_map f) m = g (λ (i : ι), (f i) (m i))

theorem continuous_multilinear_map.cons_add {R : Type u} {n : } {M : fin n.succType w} {M₂ : Type w₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] [Π (i : fin n.succ), topological_space (M i)] [topological_space M₂] (f : continuous_multilinear_map R M M₂) (m : Π (i : fin n), M i.succ) (x y : M 0) :
f (fin.cons (x + y) m) = f (fin.cons x m) + f (fin.cons y m)

In the specific case of continuous 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 continuous_multilinear_map.cons_smul {R : Type u} {n : } {M : fin n.succType w} {M₂ : Type w₂} [semiring R] [Π (i : fin n.succ), add_comm_monoid (M i)] [add_comm_monoid M₂] [Π (i : fin n.succ), semimodule R (M i)] [semimodule R M₂] [Π (i : fin n.succ), topological_space (M i)] [topological_space M₂] (f : continuous_multilinear_map R M M₂) (m : Π (i : fin n), M i.succ) (c : R) (x : M 0) :
f (fin.cons (c x) m) = c f (fin.cons x m)

In the specific case of continuous 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 continuous_multilinear_map.map_piecewise_add {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) (m m' : Π (i : ι), M₁ i) (t : finset ι) :
f (t.piecewise (m + m') m') = ∑ (s : finset ι) in t.powerset, f (s.piecewise m m')

theorem continuous_multilinear_map.map_add_univ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) [fintype ι] (m m' : Π (i : ι), M₁ i) :
f (m + m') = ∑ (s : finset ι), f (s.piecewise m m')

Additivity of a continuous 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 continuous_multilinear_map.map_sum_finset {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) {α : ι → Type u_1} [fintype ι] (g : Π (i : ι), α iM₁ i) (A : Π (i : ι), finset (α i)) :
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 continuous 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 continuous_multilinear_map.map_sum {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) {α : ι → Type u_1} [fintype ι] (g : Π (i : ι), α iM₁ i) [Π (i : ι), fintype (α i)] :
f (λ (i : ι), ∑ (j : α i), g i j) = ∑ (r : Π (i : ι), α i), f (λ (i : ι), g i (r i))

If f is continuous 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.

@[simp]
theorem continuous_multilinear_map.map_sub {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_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)

@[instance]
def continuous_multilinear_map.has_neg {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_add_group M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.neg_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) [topological_add_group M₂] (m : Π (i : ι), M₁ i) :
(-f) m = -f m

@[instance]
def continuous_multilinear_map.add_comm_group {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_add_group M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.sub_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f f' : continuous_multilinear_map R M₁ M₂) [topological_add_group M₂] (m : Π (i : ι), M₁ i) :
(f - f') m = f m - f' m

theorem continuous_multilinear_map.map_piecewise_smul {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) (c : ι → R) (m : Π (i : ι), M₁ i) (s : finset ι) :
f (s.piecewise (λ (i : ι), c i m i) m) = (∏ (i : ι) in s, c i) f m

theorem continuous_multilinear_map.map_smul_univ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) [fintype ι] (c : ι → R) (m : Π (i : ι), M₁ i) :
f (λ (i : ι), c i m i) = (∏ (i : ι), c i) f m

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

@[instance]
def continuous_multilinear_map.has_scalar {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_space R] [topological_semimodule R M₂] :

Equations
@[simp]
theorem continuous_multilinear_map.smul_apply {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_monoid (M₁ i)] [add_comm_monoid M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] (f : continuous_multilinear_map R M₁ M₂) [topological_space R] [topological_semimodule R M₂] (c : R) (m : Π (i : ι), M₁ i) :
(c f) m = c f m

@[instance]
def continuous_multilinear_map.semimodule {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_add_group M₂] [topological_space R] [topological_semimodule R M₂] :

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

Equations
def continuous_multilinear_map.to_multilinear_map_linear {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [decidable_eq ι] [comm_ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [Π (i : ι), semimodule R (M₁ i)] [semimodule R M₂] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_add_group M₂] [topological_space R] [topological_semimodule R M₂] :

Linear map version of the map to_multilinear_map associating to a continuous multilinear map the corresponding multilinear map.

Equations
def continuous_linear_map.comp_continuous_multilinear_map {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [add_comm_group M₃] [Π (i : ι), module R (M₁ i)] [module R M₂] [module R M₃] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_space M₃] :
(M₂ →L[R] M₃)continuous_multilinear_map R M₁ M₂continuous_multilinear_map R M₁ M₃

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

Equations
@[simp]
theorem continuous_linear_map.comp_continuous_multilinear_map_coe {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [decidable_eq ι] [ring R] [Π (i : ι), add_comm_group (M₁ i)] [add_comm_group M₂] [add_comm_group M₃] [Π (i : ι), module R (M₁ i)] [module R M₂] [module R M₃] [Π (i : ι), topological_space (M₁ i)] [topological_space M₂] [topological_space M₃] (g : M₂ →L[R] M₃) (f : continuous_multilinear_map R M₁ M₂) :