The injective seminorm on a binary tensor product

A tensor u : E ⊗[𝕜] F defines a bounded operator StrongDual 𝕜 E →L[𝕜] F, sending f to ∑ i, f (x i) • y i for any decomposition u = ∑ i, x i ⊗ₜ y i. The injective seminorm of u is the operator norm of this map. Over ℝ and ℂ it is the supremum of ‖∑ i, f (x i) * g (y i)‖ over continuous linear functionals f on E and g on F of norm at most one, which is the classical definition of the injective norm.

This file proves that the injective seminorm is bounded by the projective seminorm. Over ℝ and ℂ, both agree with ‖x‖ * ‖y‖ on a pure tensor x ⊗ₜ y and are norms when E and F are normed spaces. Definiteness follows, via Hahn–Banach, from the injectivity of the map from tensors to operators on the dual.

The type TauCeti.InjectiveTensor 𝕜 E F is a copy of E ⊗[𝕜] F carrying the injective seminorm, and the identity of the underlying tensors is a contraction from TauCeti.ProjectiveTensor 𝕜 E F to it.

Mathlib's PiTensorProduct.injectiveSeminorm is a different seminorm on finite families of factors, defined by duality against all normed target spaces rather than against the scalar field; it is not the classical injective norm used here.

Main definitions

• TensorProduct.contractStrongDual 𝕜 E F: the bounded operator on the dual of E induced by a tensor.
• TensorProduct.injectiveSeminorm 𝕜 E F: the injective seminorm on E ⊗[𝕜] F.
• TauCeti.InjectiveTensor 𝕜 E F: the algebraic tensor product with the injective seminorm.
• TauCeti.ProjectiveTensor.toInjectiveTensor: the contraction from the projective to the injective tensor product.

Main results

• TensorProduct.injectiveSeminorm_le_projectiveSeminorm: ε ≤ π.
• TensorProduct.injectiveSeminorm_le_iff_forall_norm_le_one: the classical description of the injective seminorm over ℝ and ℂ.
• TensorProduct.injectiveSeminorm_le_iff_forall_norm_contractStrongDual_le: over ℝ and ℂ, the injective seminorm is the supremum of ‖contractStrongDual 𝕜 E F u f‖ over the closed unit ball of the dual of E.
• TensorProduct.injectiveSeminorm_tmul and TensorProduct.projectiveSeminorm_tmul: both seminorms are cross norms.
• TensorProduct.injectiveSeminorm_eq_norm_lid: on 𝕜 ⊗[𝕜] E, the injective seminorm is the norm of the image in E, over any nontrivially normed field.
• TensorProduct.injectiveSeminorm_comm and TensorProduct.injectiveSeminorm_eq_norm_rid: over ℝ and ℂ, the injective seminorm is preserved by TensorProduct.comm, and on E ⊗[𝕜] 𝕜 it is the norm of the image in E.
• TensorProduct.contractStrongDual_injective: over ℝ and ℂ, a tensor is determined by the operator it induces on the dual of a normed left factor.
• TensorProduct.injectiveSeminorm_eq_zero_iff and TensorProduct.projectiveSeminorm_eq_zero_iff: both seminorms are definite.

References

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

noncomputable def TensorProduct.contractStrongDual (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : TensorProduct 𝕜 E F →ₗ[𝕜] StrongDual 𝕜 E →L[𝕜] F

The bounded operator StrongDual 𝕜 E →L[𝕜] F induced by a tensor in E ⊗[𝕜] F: the pure tensor x ⊗ₜ y gives f ↦ f x • y.

@[simp]

theorem TensorProduct.contractStrongDual_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) (f : StrongDual 𝕜 E) : ((contractStrongDual 𝕜 E F) (x ⊗ₜ[𝕜] y)) f = f x • y

The operator induced by x ⊗ₜ y sends f to f x • y.

theorem TensorProduct.contractStrongDual_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) (f : StrongDual 𝕜 E) : ((contractStrongDual 𝕜 E F) u) f = (TensorProduct.lid 𝕜 F) ((LinearMap.rTensor F ↑f) u)

The operator induced by a tensor sends f to the image of the tensor under f ⊗ id, followed by 𝕜 ⊗[𝕜] F ≃ F.

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

The injective seminorm on E ⊗[𝕜] F: the operator norm of the operator on the dual of E induced by a tensor. Over ℝ and ℂ it is the supremum of ‖∑ i, f (x i) * g (y i)‖ over continuous linear functionals f and g of norm at most one, for any decomposition u = ∑ i, x i ⊗ₜ y i; see injectiveSeminorm_le_iff_forall_norm_le_one.

theorem TensorProduct.injectiveSeminorm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (injectiveSeminorm 𝕜 E F) u = ‖(contractStrongDual 𝕜 E F) u‖

The injective seminorm is the operator norm of the induced operator on the dual.

theorem TensorProduct.norm_contractStrongDual_apply_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) (f : StrongDual 𝕜 E) : ‖((contractStrongDual 𝕜 E F) u) f‖ ≤ (injectiveSeminorm 𝕜 E F) u * ‖f‖

The operator induced by a tensor is bounded by its injective seminorm.

theorem TensorProduct.lift_smulRight {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] (f : StrongDual 𝕜 E) (g : F →L[𝕜] G) (u : TensorProduct 𝕜 E F) : (lift (ContinuousLinearMap.toLinearMap₁₂ (ContinuousLinearMap.smulRight f g))) u = g (((contractStrongDual 𝕜 E F) u) f)

The linear map induced on algebraic tensors by the bilinear map (x, y) ↦ f x • g y sends a tensor u to g applied to the operator induced by u on the dual of E, evaluated at f.

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

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

theorem TensorProduct.injectiveSeminorm_le_projectiveSeminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : injectiveSeminorm 𝕜 E F ≤ projectiveSeminorm 𝕜 E F

The injective seminorm is bounded by the projective seminorm.

theorem TensorProduct.contractStrongDual_id {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (u : TensorProduct 𝕜 𝕜 E) : ((contractStrongDual 𝕜 𝕜 E) u) (ContinuousLinearMap.id 𝕜 𝕜) = (TensorProduct.lid 𝕜 E) u

Evaluating the operator induced by u : 𝕜 ⊗[𝕜] E at the identity functional of 𝕜 gives the image of u under a ⊗ₜ x ↦ a • x.

theorem TensorProduct.injectiveSeminorm_eq_norm_lid {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (u : TensorProduct 𝕜 𝕜 E) : (injectiveSeminorm 𝕜 𝕜 E) u = ‖(TensorProduct.lid 𝕜 E) u‖

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

theorem TensorProduct.apply_contractStrongDual_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) (f : StrongDual 𝕜 E) (g : StrongDual 𝕜 F) : f (((contractStrongDual 𝕜 F E) ((TensorProduct.comm 𝕜 E F) u)) g) = g (((contractStrongDual 𝕜 E F) u) f)

The operators induced by u and by its swap TensorProduct.comm 𝕜 E F u pair the same way with functionals on both factors: both values are ∑ i, f (x i) * g (y i) for any decomposition u = ∑ i, x i ⊗ₜ y i.

theorem TensorProduct.injectiveSeminorm_le_iff_forall_norm_le_one {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u : TensorProduct 𝕜 E F} {C : ℝ} (hC : 0 ≤ C) : (injectiveSeminorm 𝕜 E F) u ≤ C ↔ ∀ (f : StrongDual 𝕜 E) (g : StrongDual 𝕜 F), ‖f‖ ≤ 1 → ‖g‖ ≤ 1 → ‖g (((contractStrongDual 𝕜 E F) u) f)‖ ≤ C

Over ℝ and ℂ, the injective seminorm is the supremum of ‖g (contractStrongDual 𝕜 E F u f)‖ = ‖∑ i, f (x i) * g (y i)‖ over the closed unit balls of the duals of E and F.

theorem TensorProduct.injectiveSeminorm_le_iff_forall_norm_contractStrongDual_le {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u : TensorProduct 𝕜 E F} {C : ℝ} (hC : 0 ≤ C) : (injectiveSeminorm 𝕜 E F) u ≤ C ↔ ∀ (f : StrongDual 𝕜 E), ‖f‖ ≤ 1 → ‖((contractStrongDual 𝕜 E F) u) f‖ ≤ C

The injective seminorm is at most C iff the operator induced on the dual of the left factor maps the closed unit ball into the closed ball of radius C.

@[simp]

theorem TensorProduct.injectiveSeminorm_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) : (injectiveSeminorm 𝕜 E F) (x ⊗ₜ[𝕜] y) = ‖x‖ * ‖y‖

The injective seminorm is a cross norm: its value on x ⊗ₜ y is ‖x‖ * ‖y‖.

@[simp]

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

The projective seminorm is a cross norm: its value on x ⊗ₜ y is ‖x‖ * ‖y‖.

@[simp]

theorem TensorProduct.injectiveSeminorm_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : TensorProduct 𝕜 E F) : (injectiveSeminorm 𝕜 F E) ((TensorProduct.comm 𝕜 E F) u) = (injectiveSeminorm 𝕜 E F) u

Over ℝ and ℂ, the injective seminorm is symmetric: swapping the factors preserves it.

theorem TensorProduct.injectiveSeminorm_eq_norm_rid {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (u : TensorProduct 𝕜 E 𝕜) : (injectiveSeminorm 𝕜 E 𝕜) u = ‖(TensorProduct.rid 𝕜 E) u‖

Over ℝ and ℂ, on E ⊗[𝕜] 𝕜 the injective seminorm is the norm of the image under x ⊗ₜ a ↦ a • x.

theorem TensorProduct.contractStrongDual_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : Function.Injective ⇑(contractStrongDual 𝕜 E F)

Over ℝ and ℂ, a tensor whose left factor is a normed space is determined by the operator it induces on the dual of that factor.

@[simp]

theorem TensorProduct.injectiveSeminorm_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {u : TensorProduct 𝕜 E F} : (injectiveSeminorm 𝕜 E F) u = 0 ↔ u = 0

Over ℝ and ℂ, the injective seminorm on a tensor product of normed spaces is definite.

@[simp]

theorem TensorProduct.projectiveSeminorm_eq_zero_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {u : TensorProduct 𝕜 E F} : (projectiveSeminorm 𝕜 E F) u = 0 ↔ u = 0

Over ℝ and ℂ, the projective seminorm on a tensor product of normed spaces is definite.

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

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

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

• toTensorProduct : TensorProduct 𝕜 E F

  The underlying element of the algebraic tensor product.

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

Forget the injective seminorm.

@[instance_reducible]

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

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

Forget the injective seminorm and retain the additive structure.

@[instance_reducible]

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

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

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

@[simp]

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

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

@[simp]

theorem TauCeti.InjectiveTensor.equiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.addEquiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : InjectiveTensor 𝕜 E F) : (addEquiv 𝕜 E F) u = u.toTensorProduct

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

@[simp]

theorem TauCeti.InjectiveTensor.addEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.linearEquiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : InjectiveTensor 𝕜 E F) : (linearEquiv 𝕜 E F) u = u.toTensorProduct

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

@[simp]

theorem TauCeti.InjectiveTensor.linearEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.toTensorProduct_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : toTensorProduct 0 = 0

The underlying tensor of 0 is 0.

@[simp]

theorem TauCeti.InjectiveTensor.toTensorProduct_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : InjectiveTensor 𝕜 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.InjectiveTensor.toTensorProduct_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : InjectiveTensor 𝕜 E F) : (-u).toTensorProduct = -u.toTensorProduct

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

@[simp]

theorem TauCeti.InjectiveTensor.toTensorProduct_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u v : InjectiveTensor 𝕜 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.InjectiveTensor.toTensorProduct_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (a : 𝕜) (u : InjectiveTensor 𝕜 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.InjectiveTensor.mk_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] : { toTensorProduct := 0 } = 0

Wrapping 0 gives 0.

@[simp]

theorem TauCeti.InjectiveTensor.mk_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.mk_neg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.mk_sub {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.mk_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [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.InjectiveTensor.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {u v : InjectiveTensor 𝕜 E F} (h : u.toTensorProduct = v.toTensorProduct) : u = v

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

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

@[instance_reducible]

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

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

The norm of an injective tensor is the injective seminorm of its underlying tensor.

@[instance_reducible]

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

theorem TauCeti.InjectiveTensor.continuousLinearMap_ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {M : Type u_4} [AddCommGroup M] [Module 𝕜 M] [TopologicalSpace M] {l l' : InjectiveTensor 𝕜 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 injective tensor product agree when they agree on pure tensors.

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

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

The identity of the underlying tensors, from the projective to the injective tensor product. It is a contraction because the injective seminorm is bounded by the projective seminorm.

@[simp]

theorem TauCeti.ProjectiveTensor.toInjectiveTensor_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (u : ProjectiveTensor 𝕜 E F) : (toInjectiveTensor 𝕜 E F) u = { toTensorProduct := u.toTensorProduct }

The contraction to the injective tensor product keeps the underlying tensor.

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

The identity from the projective to the injective tensor product is a contraction.

@[instance_reducible]

noncomputable instance TauCeti.instNormedAddCommGroupProjectiveTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : NormedAddCommGroup (ProjectiveTensor 𝕜 E F)

@[instance_reducible]

noncomputable instance TauCeti.instNormedAddCommGroupInjectiveTensor {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : NormedAddCommGroup (InjectiveTensor 𝕜 E F)

@[simp]

theorem TauCeti.ProjectiveTensor.norm_mk_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) : ‖{ toTensorProduct := x ⊗ₜ[𝕜] y }‖ = ‖x‖ * ‖y‖

Over ℝ and ℂ, the norm of a pure projective tensor is the product of the norms.

@[simp]

theorem TauCeti.InjectiveTensor.norm_mk_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : F) : ‖{ toTensorProduct := x ⊗ₜ[𝕜] y }‖ = ‖x‖ * ‖y‖

Over ℝ and ℂ, the norm of a pure injective tensor is the product of the norms.