Projective seminorm on the tensor of a finite family of normed spaces.

Let 𝕜 be a normed field and E be a family of normed 𝕜-vector spaces Eᵢ, indexed by a finite type ι. We define a seminorm on ⨂[𝕜] i, Eᵢ, which we call the "projective seminorm". For x an element of ⨂[𝕜] i, Eᵢ, its projective seminorm is the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼ ∈ Π i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

In particular, every norm ‖.‖ on ⨂[𝕜] i, Eᵢ satisfying ‖⨂ₜ[𝕜] i, m i‖ ≤ Π i, ‖m i‖ for every m in Π i, Eᵢ is bounded above by the projective seminorm.

Main definitions

• PiTensorProduct.projectiveSeminorm: The projective seminorm on ⨂[𝕜] i, Eᵢ.
• PiTensorProduct.liftEquiv: The bijection between ContinuousMultilinearMap 𝕜 E F and (⨂[𝕜] i, Eᵢ) →L[𝕜] F, as a continuous linear equivalence.
• PiTensorProduct.liftIsometry: The bijection between ContinuousMultilinearMap 𝕜 E F and (⨂[𝕜] i, Eᵢ) →L[𝕜] F, as an isometric linear equivalence.
• PiTensorProduct.tprodL: The canonical continuous multilinear map from E = Πᵢ Eᵢ to ⨂[𝕜] i, Eᵢ.
• PiTensorProduct.mapL: The continuous linear map from ⨂[𝕜] i, Eᵢ to ⨂[𝕜] i, E'ᵢ induced by a family of continuous linear maps Eᵢ →L[𝕜] E'ᵢ.
• PiTensorProduct.mapLMultilinear: The continuous multilinear map from Πᵢ (Eᵢ →L[𝕜] E'ᵢ) to (⨂[𝕜] i, Eᵢ) →L[𝕜] (⨂[𝕜] i, E'ᵢ) sending a family f to PiTensorProduct.mapL f.

Main results

• PiTensorProduct.norm_eval_le_projectiveSeminorm: If f is a continuous multilinear map on E = Π i, Eᵢ and x is in ⨂[𝕜] i, Eᵢ, then ‖f.lift x‖ ≤ projectiveSeminorm x * ‖f‖.
• PiTensorProduct.mapL_opNorm: If f is a family of continuous linear maps fᵢ : Eᵢ →L[𝕜] Fᵢ, then ‖PiTensorProduct.mapL f‖ ≤ ∏ i, ‖fᵢ‖.
• PiTensorProduct.opNorm_mapLMultilinear_le : If F is a normed vecteor space, then ‖mapLMultilinear 𝕜 E F‖ ≤ 1.

TODO

• If the base field is ℝ or ℂ (or more generally if the injection of Eᵢ into its bidual is an isometry for every i), then we have projectiveSeminorm ⨂ₜ[𝕜] i, mᵢ = Π i, ‖mᵢ‖.
• If all Eᵢ are separated and satisfy SeparatingDual, then the seminorm on ⨂[𝕜] i, Eᵢ is a norm.
• Adapt the remaining functoriality constructions/properties from PiTensorProduct.

def PiTensorProduct.projectiveSeminormAux {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] : FreeAddMonoid (𝕜 × ((i : ι) → E i)) → ℝ

A lift of the projective seminorm to FreeAddMonoid (𝕜 × Π i, Eᵢ), useful to prove the properties of projectiveSeminorm.

Equations

• PiTensorProduct.projectiveSeminormAux p = (List.map (fun (p : 𝕜 × ((i : ι) → E i)) => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) (FreeAddMonoid.toList p)).sum

theorem PiTensorProduct.projectiveSeminormAux_nonneg {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : 0 ≤ projectiveSeminormAux p

theorem PiTensorProduct.projectiveSeminormAux_add_le {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] (p q : FreeAddMonoid (𝕜 × ((i : ι) → E i))) : projectiveSeminormAux (p + q) ≤ projectiveSeminormAux p + projectiveSeminormAux q

theorem PiTensorProduct.projectiveSeminormAux_smul {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] (p : FreeAddMonoid (𝕜 × ((i : ι) → E i))) (a : 𝕜) : projectiveSeminormAux ((FreeAddMonoid.map fun (y : 𝕜 × ((i : ι) → E i)) => (a * y.1, y.2)) p) = ‖a‖ * projectiveSeminormAux p

theorem PiTensorProduct.bddBelow_projectiveSemiNormAux {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : BddBelow (Set.range fun (p : ↑x.lifts) => projectiveSeminormAux ↑p)

@[implicit_reducible]

noncomputable instance PiTensorProduct.instNorm {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : Norm (PiTensorProduct 𝕜 fun (i : ι) => E i)

Equations

• PiTensorProduct.instNorm = { norm := fun (x : PiTensorProduct 𝕜 fun (i : ι) => E i) => ⨅ (p : ↑x.lifts), PiTensorProduct.projectiveSeminormAux ↑p }

theorem PiTensorProduct.norm_def {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖x‖ = ⨅ (p : ↑x.lifts), projectiveSeminormAux ↑p

@[deprecated Norm.norm (since := "2026-06-10")]

def PiTensorProduct.projectiveSeminormFun {E : Type u_8} [self : Norm E] : E → ℝ

Alias of Norm.norm.

Equations

• @PiTensorProduct.projectiveSeminormFun = @norm

theorem PiTensorProduct.projectiveSeminorm_zero {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : ‖0‖ = 0

theorem PiTensorProduct.projectiveSeminorm_add_le {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x y : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖x + y‖ ≤ ‖x‖ + ‖y‖

theorem PiTensorProduct.projectiveSeminorm_smul_le {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (a : 𝕜) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖a • x‖ ≤ ‖a‖ * ‖x‖

noncomputable def PiTensorProduct.projectiveSeminorm {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : Seminorm 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

The projective seminorm on ⨂[𝕜] i, Eᵢ. It sends an element x of ⨂[𝕜] i, Eᵢ to the infimum over all expressions of x as ∑ j, ⨂ₜ[𝕜] mⱼ i (with the mⱼ ∈ Π i, Eᵢ) of ∑ j, Π i, ‖mⱼ i‖.

Equations

• PiTensorProduct.projectiveSeminorm = Seminorm.ofSMulLE norm ⋯ ⋯ ⋯

@[implicit_reducible]

noncomputable instance PiTensorProduct.instSeminormedAddCommGroup {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : SeminormedAddCommGroup (PiTensorProduct 𝕜 fun (i : ι) => E i)

Equations

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

@[implicit_reducible]

noncomputable instance PiTensorProduct.instNormedSpace {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : NormedSpace 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

Equations

• PiTensorProduct.instNormedSpace = { toModule := PiTensorProduct.instModule, norm_smul_le := ⋯ }

@[deprecated PiTensorProduct.norm_def (since := "2026-06-10")]

theorem PiTensorProduct.projectiveSeminorm_apply {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : projectiveSeminorm x = ⨅ (p : ↑x.lifts), projectiveSeminormAux ↑p

theorem PiTensorProduct.projectiveSeminorm_tprod_le {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (m : (i : ι) → E i) : projectiveSeminorm (⨂ₜ[𝕜] (i : ι), m i) ≤ ∏ i : ι, ‖m i‖

theorem PiTensorProduct.norm_eval_le_projectiveSeminorm {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {G : Type u_4} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 E G) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ‖(lift f.toMultilinearMap) x‖ ≤ ‖f‖ * ‖x‖

noncomputable def PiTensorProduct.liftEquiv {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ContinuousMultilinearMap 𝕜 E F ≃ₗ[𝕜] (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] F

The linear equivalence between ContinuousMultilinearMap 𝕜 E F and (⨂[𝕜] i, Eᵢ) →L[𝕜] F induced by PiTensorProduct.lift, for every normed space F.

Equations

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

@[simp]

theorem PiTensorProduct.liftEquiv_apply {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : ContinuousMultilinearMap 𝕜 E F) : (liftEquiv 𝕜 E F) f = (lift f.toMultilinearMap).mkContinuous ‖f‖ ⋯

@[simp]

theorem PiTensorProduct.liftEquiv_symm_apply {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (l : (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] F) : (liftEquiv 𝕜 E F).symm l = (lift.symm ↑l).mkContinuous ‖l‖ ⋯

noncomputable def PiTensorProduct.liftIsometry {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4) [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] F

For a normed space F, we have constructed in PiTensorProduct.liftEquiv the canonical linear equivalence between ContinuousMultilinearMap 𝕜 E F and (⨂[𝕜] i, Eᵢ) →L[𝕜] F (induced by PiTensorProduct.lift). Here we give the upgrade of this equivalence to an isometric linear equivalence; in particular, it is a continuous linear equivalence.

Equations

• PiTensorProduct.liftIsometry 𝕜 E F = LinearIsometryEquiv.ofBounds (PiTensorProduct.liftEquiv 𝕜 E F) ⋯ ⋯

@[simp]

theorem PiTensorProduct.liftIsometry_apply_apply {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : ContinuousMultilinearMap 𝕜 E F) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : ((liftIsometry 𝕜 E F) f) x = (lift f.toMultilinearMap) x

noncomputable def PiTensorProduct.tprodL {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : ContinuousMultilinearMap 𝕜 E (PiTensorProduct 𝕜 fun (i : ι) => E i)

The canonical continuous multilinear map from E = Πᵢ Eᵢ to ⨂[𝕜] i, Eᵢ.

Equations

• PiTensorProduct.tprodL 𝕜 = (PiTensorProduct.liftIsometry 𝕜 E (PiTensorProduct 𝕜 fun (i : ι) => E i)).symm (ContinuousLinearMap.id 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i))

@[simp]

theorem PiTensorProduct.tprodL_toFun {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (a✝ : (i : ι) → E i) : (tprodL 𝕜) a✝ = (tprod 𝕜) a✝

@[simp]

theorem PiTensorProduct.tprodL_coe {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : (tprodL 𝕜).toMultilinearMap = tprod 𝕜

@[simp]

theorem PiTensorProduct.liftIsometry_symm_apply {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (l : (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] F) : (liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜)

@[simp]

theorem PiTensorProduct.liftIsometry_tprodL {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : (liftIsometry 𝕜 E (PiTensorProduct 𝕜 fun (i : ι) => E i)) (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

noncomputable def PiTensorProduct.mapL {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) : (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] PiTensorProduct 𝕜 fun (i : ι) => E' i

Let Eᵢ and E'ᵢ be two families of normed 𝕜-vector spaces. Let f be a family of continuous 𝕜-linear maps between Eᵢ and E'ᵢ, i.e. f : Πᵢ Eᵢ →L[𝕜] E'ᵢ, then there is an induced continuous linear map ⨂ᵢ Eᵢ → ⨂ᵢ E'ᵢ by ⨂ aᵢ ↦ ⨂ fᵢ aᵢ.

Equations

• PiTensorProduct.mapL f = (PiTensorProduct.liftIsometry 𝕜 E (PiTensorProduct 𝕜 fun (i : ι) => E' i)) ((PiTensorProduct.tprodL 𝕜).compContinuousLinearMap f)

@[simp]

theorem PiTensorProduct.mapL_coe {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) : ↑(mapL f) = map fun (i : ι) => ↑(f i)

@[simp]

theorem PiTensorProduct.mapL_apply {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) (x : PiTensorProduct 𝕜 fun (i : ι) => E i) : (mapL f) x = (map fun (i : ι) => ↑(f i)) x

noncomputable def PiTensorProduct.mapLIncl {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (p : (i : ι) → Submodule 𝕜 (E i)) : (PiTensorProduct 𝕜 fun (i : ι) => ↥(p i)) →L[𝕜] PiTensorProduct 𝕜 fun (i : ι) => E i

Given submodules pᵢ ⊆ Eᵢ, this is the natural map: ⨂[𝕜] i, pᵢ → ⨂[𝕜] i, Eᵢ. This is the continuous version of PiTensorProduct.mapIncl.

Equations

• PiTensorProduct.mapLIncl p = PiTensorProduct.mapL fun (i : ι) => (p i).subtypeL

theorem PiTensorProduct.mapL_comp {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} {E'' : ι → Type u_6} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] [(i : ι) → SeminormedAddCommGroup (E'' i)] [(i : ι) → NormedSpace 𝕜 (E'' i)] (g : (i : ι) → E' i →L[𝕜] E'' i) (f : (i : ι) → E i →L[𝕜] E' i) : (mapL fun (i : ι) => g i ∘SL f i) = mapL g ∘SL mapL f

theorem PiTensorProduct.liftIsometry_comp_mapL {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) (h : ContinuousMultilinearMap 𝕜 E' F) : (liftIsometry 𝕜 E' F) h ∘SL mapL f = (liftIsometry 𝕜 E F) (h.compContinuousLinearMap f)

@[simp]

theorem PiTensorProduct.mapL_id {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : (mapL fun (i : ι) => ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id 𝕜 (PiTensorProduct 𝕜 fun (i : ι) => E i)

@[simp]

theorem PiTensorProduct.mapL_one {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : (mapL fun (i : ι) => 1) = 1

theorem PiTensorProduct.mapL_mul {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (f₁ f₂ : (i : ι) → E i →L[𝕜] E i) : (mapL fun (i : ι) => f₁ i * f₂ i) = mapL f₁ * mapL f₂

noncomputable def PiTensorProduct.mapLMonoidHom {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] : ((i : ι) → E i →L[𝕜] E i) →* (PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] PiTensorProduct 𝕜 fun (i : ι) => E i

Upgrading PiTensorProduct.mapL to a MonoidHom when E = E'.

Equations

• PiTensorProduct.mapLMonoidHom = { toFun := PiTensorProduct.mapL, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem PiTensorProduct.mapLMonoidHom_apply {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (f : (i : ι) → E i →L[𝕜] E i) : mapLMonoidHom f = mapL f

@[simp]

theorem PiTensorProduct.mapL_pow {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (f : (i : ι) → E i →L[𝕜] E i) (n : ℕ) : mapL (f ^ n) = mapL f ^ n

theorem PiTensorProduct.mapL_add {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) [DecidableEq ι] (i : ι) (u v : E i →L[𝕜] E' i) : mapL (Function.update f i (u + v)) = mapL (Function.update f i u) + mapL (Function.update f i v)

theorem PiTensorProduct.mapL_smul {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) [DecidableEq ι] (i : ι) (c : 𝕜) (u : E i →L[𝕜] E' i) : mapL (Function.update f i (c • u)) = c • mapL (Function.update f i u)

theorem PiTensorProduct.opNorm_mapL {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) : ‖mapL f‖ ≤ ∏ i : ι, ‖f i‖

noncomputable def PiTensorProduct.mapLMultilinear {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (E' : ι → Type u_5) [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] : ContinuousMultilinearMap 𝕜 (fun (i : ι) => E i →L[𝕜] E' i) ((PiTensorProduct 𝕜 fun (i : ι) => E i) →L[𝕜] PiTensorProduct 𝕜 fun (i : ι) => E' i)

The tensor of a family of linear maps from Eᵢ to E'ᵢ, as a continuous multilinear map of the family.

Equations

• PiTensorProduct.mapLMultilinear 𝕜 E E' = { toFun := PiTensorProduct.mapL, map_update_add' := ⋯, map_update_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem PiTensorProduct.mapLMultilinear_toFun_apply {ι : Type u_1} [Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] (E' : ι → Type u_5) [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] (f : (i : ι) → E i →L[𝕜] E' i) (a✝ : PiTensorProduct 𝕜 fun (i : ι) => E i) : ((mapLMultilinear 𝕜 E E') f) a✝ = (liftAux ((tprodL 𝕜).compContinuousLinearMap f).toMultilinearMap) a✝

theorem PiTensorProduct.opNorm_mapLMultilinear_le {ι : Type u_1} [Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [(i : ι) → SeminormedAddCommGroup (E i)] [NontriviallyNormedField 𝕜] [(i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)] : ‖mapLMultilinear 𝕜 E E'‖ ≤ 1