The projective seminorm on a binary tensor product

For seminormed spaces E and F over a normed field 𝕜, the projective seminorm of u : E ⊗[𝕜] F is the infimum of ∑ i, ‖x i‖ * ‖y i‖ over all finite decompositions u = ∑ i, x i ⊗ₜ y i. It is the largest seminorm on E ⊗[𝕜] F that is bounded on pure tensors by the product of the norms of the factors. Over a nontrivially normed field, every bounded bilinear map out of E × F induces a linear map on E ⊗[𝕜] F bounded by its operator norm for this seminorm. On TauCeti.ProjectiveTensor 𝕜 E F this gives the norm-preserving universal property on algebraic tensors: bounded bilinear maps E →L[𝕜] F →L[𝕜] G correspond isometrically to bounded operators ProjectiveTensor 𝕜 E F →L[𝕜] G.

Mathlib's binary tensor product carries no norm of its own for general normed spaces, while for inner product spaces it carries the Hilbert-space norm. The type TauCeti.ProjectiveTensor 𝕜 E F is therefore a separate copy of E ⊗[𝕜] F carrying the projective seminorm; its completion is the completed projective tensor product. That the projective seminorm is a norm over ℝ and ℂ is proved with the injective seminorm in TauCeti.Analysis.Normed.Module.TensorProduct.InjectiveSeminorm.

The finite-family analogue is Mathlib's PiTensorProduct.projectiveSeminorm, whose arguments this file adapts to two factors indexed by Fin n decompositions. The construction of TauCeti.ProjectiveTensor.liftIsometry follows Mathlib's PiTensorProduct.liftIsometry.

Main definitions

• TensorProduct.projectiveSeminorm 𝕜 E F: the projective seminorm on E ⊗[𝕜] F.
• TauCeti.ProjectiveTensor 𝕜 E F: the algebraic tensor product with the projective seminorm.
• TauCeti.ProjectiveTensor.tmulL: the bounded bilinear map (x, y) ↦ x ⊗ₜ y.
• TauCeti.ProjectiveTensor.liftIsometry: the isometric universal property of the projective tensor product.

Main results

• TensorProduct.projectiveSeminorm_sum_tmul_le and TensorProduct.exists_sum_tmul_eq_of_projectiveSeminorm_lt: the projective seminorm is the infimum of the costs of finite decompositions.
• TensorProduct.apply_le_mul_projectiveSeminorm: a seminorm bounded by C ‖x‖ ‖y‖ on pure tensors is bounded by C times the projective seminorm.
• TensorProduct.norm_lift_le_projectiveSeminorm: over a nontrivially normed field, the linear map induced by a bounded bilinear map B is bounded by ‖B‖ times the projective seminorm.
• TensorProduct.projectiveSeminorm_comm, TensorProduct.projectiveSeminorm_eq_norm_lid and TensorProduct.projectiveSeminorm_eq_norm_rid: the projective seminorm is preserved by TensorProduct.comm, and on 𝕜 ⊗[𝕜] E and E ⊗[𝕜] 𝕜 it is the norm of the image in E.

References

• R. A. Ryan, Introduction to Tensor Products of Banach Spaces, Springer, 2002, §2.1.

noncomputable def TensorProduct.projectiveSeminorm (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Seminorm 𝕜 (TensorProduct 𝕜 E F)

The projective seminorm on E ⊗[𝕜] F: the infimum of ∑ i, ‖x i‖ * ‖y i‖ over all finite decompositions u = ∑ i, x i ⊗ₜ y i.

theorem TensorProduct.projectiveSeminorm_sum_tmul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_4} (s : Finset ι) (x : ι → E) (y : ι → F) : (projectiveSeminorm 𝕜 E F) (∑ i ∈ s, x i ⊗ₜ[𝕜] y i) ≤ ∑ i ∈ s, ‖x i‖ * ‖y i‖

The projective seminorm of a finite sum of pure tensors is at most its cost.

theorem TensorProduct.exists_sum_tmul_eq_of_projectiveSeminorm_lt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u : TensorProduct 𝕜 E F} {c : ℝ} (h : (projectiveSeminorm 𝕜 E F) u < c) : ∃ (n : ℕ) (x : Fin n → E) (y : Fin n → F), ∑ i : Fin n, x i ⊗ₜ[𝕜] y i = u ∧ ∑ i : Fin n, ‖x i‖ * ‖y i‖ < c

A strict upper bound on the projective seminorm is beaten by the cost of some finite decomposition.

theorem TensorProduct.projectiveSeminorm_tmul_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) : (projectiveSeminorm 𝕜 E F) (x ⊗ₜ[𝕜] y) ≤ ‖x‖ * ‖y‖

The projective seminorm of a pure tensor is at most the product of the norms.

theorem TensorProduct.apply_le_mul_projectiveSeminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [AddCommGroup G] [Module 𝕜 G] {p : Seminorm 𝕜 G} {f : TensorProduct 𝕜 E F →ₗ[𝕜] G} {C : ℝ} (hC : 0 ≤ C) (h : ∀ (x : E) (y : F), p (f (x ⊗ₜ[𝕜] y)) ≤ C * (‖x‖ * ‖y‖)) (u : TensorProduct 𝕜 E F) : p (f u) ≤ C * (projectiveSeminorm 𝕜 E F) u

A seminorm bounded on the images of pure tensors by C * (‖x‖ * ‖y‖) is bounded on the image of every tensor by C times the projective seminorm.

theorem TensorProduct.le_projectiveSeminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {p : Seminorm 𝕜 (TensorProduct 𝕜 E F)} (h : ∀ (x : E) (y : F), p (x ⊗ₜ[𝕜] y) ≤ ‖x‖ * ‖y‖) : p ≤ projectiveSeminorm 𝕜 E F

The projective seminorm is the largest seminorm on E ⊗[𝕜] F bounded on pure tensors by the product of the norms.

@[simp]

theorem TensorProduct.projectiveSeminorm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (projectiveSeminorm 𝕜 F E) ((TensorProduct.comm 𝕜 E F) u) = (projectiveSeminorm 𝕜 E F) u

The projective seminorm is symmetric: swapping the factors preserves it.

theorem TensorProduct.projectiveSeminorm_eq_norm_lid {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (u : TensorProduct 𝕜 𝕜 E) : (projectiveSeminorm 𝕜 𝕜 E) u = ‖(TensorProduct.lid 𝕜 E) u‖

On 𝕜 ⊗[𝕜] E, the projective seminorm is the norm of the image under a ⊗ₜ x ↦ a • x.

theorem TensorProduct.projectiveSeminorm_eq_norm_rid {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (u : TensorProduct 𝕜 E 𝕜) : (projectiveSeminorm 𝕜 E 𝕜) u = ‖(TensorProduct.rid 𝕜 E) u‖

On E ⊗[𝕜] 𝕜, the projective seminorm is the norm of the image under x ⊗ₜ a ↦ a • x.

theorem TensorProduct.norm_lift_le_projectiveSeminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (u : TensorProduct 𝕜 E F) : ‖(lift (ContinuousLinearMap.toLinearMap₁₂ B)) u‖ ≤ ‖B‖ * (projectiveSeminorm 𝕜 E F) u

The linear map on E ⊗[𝕜] F induced by a bounded bilinear map B is bounded by ‖B‖ times the projective seminorm.

structure TauCeti.ProjectiveTensor (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Type (max u_2 u_3)

The algebraic tensor product E ⊗[𝕜] F carrying the projective seminorm.

This wrapper distinguishes the projective seminorm from other norms on the same algebraic tensor product, such as the injective norm or the Hilbert-space norm of inner product spaces.

• toTensorProduct : TensorProduct 𝕜 E F

  The underlying element of the algebraic tensor product.

def TauCeti.ProjectiveTensor.equiv (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ProjectiveTensor 𝕜 E F ≃ TensorProduct 𝕜 E F

Forget the projective seminorm.

@[instance_reducible]

instance TauCeti.ProjectiveTensor.instAddCommGroup (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : AddCommGroup (ProjectiveTensor 𝕜 E F)

def TauCeti.ProjectiveTensor.addEquiv (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ProjectiveTensor 𝕜 E F ≃+ TensorProduct 𝕜 E F

Forget the projective seminorm and retain the additive structure.

@[instance_reducible]

instance TauCeti.ProjectiveTensor.instModule (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Module 𝕜 (ProjectiveTensor 𝕜 E F)

def TauCeti.ProjectiveTensor.linearEquiv (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ProjectiveTensor 𝕜 E F ≃ₗ[𝕜] TensorProduct 𝕜 E F

The projective tensor product is linearly equivalent to the algebraic tensor product.

@[simp]

theorem TauCeti.ProjectiveTensor.equiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : (equiv 𝕜 E F) u = u.toTensorProduct

The equivalence with E ⊗[𝕜] F forgets the wrapper.

@[simp]

theorem TauCeti.ProjectiveTensor.equiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (equiv 𝕜 E F).symm u = { toTensorProduct := u }

The inverse equivalence wraps an algebraic tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.addEquiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : (addEquiv 𝕜 E F) u = u.toTensorProduct

The additive equivalence with E ⊗[𝕜] F forgets the wrapper.

@[simp]

theorem TauCeti.ProjectiveTensor.addEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (addEquiv 𝕜 E F).symm u = { toTensorProduct := u }

The inverse additive equivalence wraps an algebraic tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.linearEquiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : (linearEquiv 𝕜 E F) u = u.toTensorProduct

The linear equivalence with E ⊗[𝕜] F forgets the wrapper.

@[simp]

theorem TauCeti.ProjectiveTensor.linearEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (linearEquiv 𝕜 E F).symm u = { toTensorProduct := u }

The inverse linear equivalence wraps an algebraic tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.toTensorProduct_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : toTensorProduct 0 = 0

The underlying tensor of 0 is 0.

@[simp]

theorem TauCeti.ProjectiveTensor.toTensorProduct_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : ProjectiveTensor 𝕜 E F) : (u + v).toTensorProduct = u.toTensorProduct + v.toTensorProduct

The underlying tensor of a sum is the sum of the underlying tensors.

@[simp]

theorem TauCeti.ProjectiveTensor.toTensorProduct_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : (-u).toTensorProduct = -u.toTensorProduct

The underlying tensor of a negation is the negated underlying tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.toTensorProduct_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : ProjectiveTensor 𝕜 E F) : (u - v).toTensorProduct = u.toTensorProduct - v.toTensorProduct

The underlying tensor of a difference is the difference of the underlying tensors.

@[simp]

theorem TauCeti.ProjectiveTensor.toTensorProduct_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (a : 𝕜) (u : ProjectiveTensor 𝕜 E F) : (a • u).toTensorProduct = a • u.toTensorProduct

The underlying tensor of a scalar multiple is the scalar multiple of the underlying tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.mk_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : { toTensorProduct := 0 } = 0

Wrapping 0 gives 0.

@[simp]

theorem TauCeti.ProjectiveTensor.mk_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : TensorProduct 𝕜 E F) : { toTensorProduct := u + v } = { toTensorProduct := u } + { toTensorProduct := v }

Wrapping a sum gives the sum of the wrapped tensors.

@[simp]

theorem TauCeti.ProjectiveTensor.mk_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : { toTensorProduct := -u } = -{ toTensorProduct := u }

Wrapping a negation gives the negation of the wrapped tensor.

@[simp]

theorem TauCeti.ProjectiveTensor.mk_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : TensorProduct 𝕜 E F) : { toTensorProduct := u - v } = { toTensorProduct := u } - { toTensorProduct := v }

Wrapping a difference gives the difference of the wrapped tensors.

@[simp]

theorem TauCeti.ProjectiveTensor.mk_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (a : 𝕜) (u : TensorProduct 𝕜 E F) : { toTensorProduct := a • u } = a • { toTensorProduct := u }

Wrapping a scalar multiple gives the scalar multiple of the wrapped tensor.

theorem TauCeti.ProjectiveTensor.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u v : ProjectiveTensor 𝕜 E F} (h : u.toTensorProduct = v.toTensorProduct) : u = v

Two projective tensors are equal when their underlying algebraic tensors are equal.

theorem TauCeti.ProjectiveTensor.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u v : ProjectiveTensor 𝕜 E F} : u = v ↔ u.toTensorProduct = v.toTensorProduct

@[instance_reducible]

noncomputable instance TauCeti.ProjectiveTensor.instSeminormedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : SeminormedAddCommGroup (ProjectiveTensor 𝕜 E F)

theorem TauCeti.ProjectiveTensor.norm_def {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : ‖u‖ = (TensorProduct.projectiveSeminorm 𝕜 E F) u.toTensorProduct

The norm of a projective tensor is the projective seminorm of its underlying tensor.

@[instance_reducible]

noncomputable instance TauCeti.ProjectiveTensor.instNormedSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : NormedSpace 𝕜 (ProjectiveTensor 𝕜 E F)

theorem TauCeti.ProjectiveTensor.continuousLinearMap_ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {M : Type u_4} [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] {l l' : ProjectiveTensor 𝕜 E F →L[𝕜] M} (h : ∀ (x : E) (y : F), l { toTensorProduct := x ⊗ₜ[𝕜] y } = l' { toTensorProduct := x ⊗ₜ[𝕜] y }) : l = l'

Two bounded operators out of the projective tensor product agree when they agree on pure tensors.

theorem TauCeti.ProjectiveTensor.continuousLinearMap_ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {M : Type u_4} [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] {l l' : ProjectiveTensor 𝕜 E F →L[𝕜] M} : l = l' ↔ ∀ (x : E) (y : F), l { toTensorProduct := x ⊗ₜ[𝕜] y } = l' { toTensorProduct := x ⊗ₜ[𝕜] y }

noncomputable def TauCeti.ProjectiveTensor.tmulL (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : E →L[𝕜] F →L[𝕜] ProjectiveTensor 𝕜 E F

The canonical bounded bilinear map (x, y) ↦ x ⊗ₜ y into the projective tensor product.

@[simp]

theorem TauCeti.ProjectiveTensor.tmulL_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) : ((tmulL 𝕜 E F) x) y = { toTensorProduct := x ⊗ₜ[𝕜] y }

The canonical bilinear map sends (x, y) to the pure tensor x ⊗ₜ y.

theorem TauCeti.ProjectiveTensor.norm_tmulL_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : ‖tmulL 𝕜 E F‖ ≤ 1

The canonical bilinear map into the projective tensor product has norm at most one.

noncomputable def TauCeti.ProjectiveTensor.liftIsometry (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) (G : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] : (E →L[𝕜] F →L[𝕜] G) ≃ₗᵢ[𝕜] ProjectiveTensor 𝕜 E F →L[𝕜] G

The universal property of the projective tensor product: bounded bilinear maps E →L[𝕜] F →L[𝕜] G correspond isometrically to bounded operators on ProjectiveTensor 𝕜 E F. The operator induced by B sends x ⊗ₜ y to B x y.

theorem TauCeti.ProjectiveTensor.liftIsometry_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (u : ProjectiveTensor 𝕜 E F) : ((liftIsometry 𝕜 E F G) B) u = (TensorProduct.lift (ContinuousLinearMap.toLinearMap₁₂ B)) u.toTensorProduct

The operator induced by a bounded bilinear map acts on the underlying tensor by TensorProduct.lift.

@[simp]

theorem TauCeti.ProjectiveTensor.liftIsometry_apply_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (x : E) (y : F) : ((liftIsometry 𝕜 E F G) B) { toTensorProduct := x ⊗ₜ[𝕜] y } = (B x) y

The operator induced by a bounded bilinear map B sends x ⊗ₜ y to B x y.

@[simp]

theorem TauCeti.ProjectiveTensor.liftIsometry_symm_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (l : ProjectiveTensor 𝕜 E F →L[𝕜] G) (x : E) (y : F) : (((liftIsometry 𝕜 E F G).symm l) x) y = l { toTensorProduct := x ⊗ₜ[𝕜] y }

The bilinear map corresponding to an operator l on the projective tensor product is (x, y) ↦ l (x ⊗ₜ y).

@[simp]

theorem TauCeti.ProjectiveTensor.liftIsometry_tmulL {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : (liftIsometry 𝕜 E F (ProjectiveTensor 𝕜 E F)) (tmulL 𝕜 E F) = ContinuousLinearMap.id 𝕜 (ProjectiveTensor 𝕜 E F)

The canonical bilinear map induces the identity of the projective tensor product.