feat(Analysis/NormedSpace/PiTensorProduct/{InjectiveNorm, ProjectiveNorm}, LinearAlgebra/PiTensorProduct): define the injective and projective norms on PiTensorProduct and prove the universal property of the first one (#11534) Define the injective and projective cross norms on a PiTensorProduct of normed vector spaces Eᵢ over a nontrivially normed field 𝕜 (cf https://en.wikipedia.org/wiki/Topological_tensor_product#Cross_norms_and_tensor_products_of_Banach_spaces). The projective norm, defined in Analysis/NormedSpace/PiTensorProduct/ProjectiveNorm.lean, is the biggest norm on the PiTensorProduct satisfying ‖⨂ₜ[𝕜] i, m i‖ ≤ Π i, ‖m i‖ for every m in Π i, Eᵢ. We are mainly interested in the injective norm in this PR, so we just give the definition of the projective norm and its basic properties. To help with the proofs, we introduce some lemmas in LinearAlgebra/PiTensorProduct.lean about the set of lifts in FreeAddMonoid (R × Π i, s i) of an element x of ⨂[R] i, s i. The injective norm, defined in Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean, is chosen to satisfy the following property: for every normed 𝕜-vector space F, the linear equivalence MultilinearMap 𝕜 E F ≃ₗ[𝕜] (⨂[𝕜] i, Eᵢ) →ₗ[𝕜] F expressing the universal property of the tensor product induces an isometric linear equivalence ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, Eᵢ) →L[𝕜] F. The idea is the following: Every normed 𝕜-vector space F defines a linear map from ⨂[𝕜] i, Eᵢ to ContinuousMultilinearMap 𝕜 E F →ₗ[𝕜] F, which sends x to the map f ↦ f.lift x. Thanks to PiTensorProduct.projectiveSeminorm_bound, this map lands in ContinuousMultilinearMap 𝕜 E F →L[𝕜] F. As this last space has a natural operator seminorm, we get an induced seminorm on ⨂[𝕜] i, Eᵢ, which, by PiTensorProduct.projectiveSeminorm_bound, is bounded above by the projective seminorm. We then take the sup of these seminorms as F varies; as this family of seminorms is bounded, its sup has good properties. In fact, we cannot take the sup over all normed spaces F because of set-theoretical issues, so we only take spaces F in the same universe as ⨂[𝕜] i, Eᵢ. We then prove in PiTensorProduct.norm_eval_le_injectiveSeminorm that this gives the same result, because every multilinear map from E to F factors though a normed vector space in the same universe as ⨂[𝕜] i, Eᵢ.

Main definitions

• PiTensorProduct.projectiveSeminorm: The projective seminorm on ⨂[𝕜] i, Eᵢ.
• PiTensorProduct.toDualContinuousMultilinearMap: The 𝕜-linear map from ⨂[𝕜] i, Eᵢ to ContinuousMultilinearMap 𝕜 E F →L[𝕜] F sending x to the map f ↦ f x.
• PiTensorProduct.injectiveSeminorm: The injective 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 cacnonical continuous multilinear map from 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 fun i ↦ (Eᵢ →L[𝕜] E'ᵢ) to (⨂[𝕜] i, Eᵢ) →L[𝕜] (⨂[𝕜] i, E'ᵢ) sending a family f to PiTensorProduct.mapL f.

Main results

• PiTensorProduct.norm_eval_le_projectiveSeminorm: For every x in ⨂[𝕜] i, Eᵢ and every continuous multilinear map f from E to a normed space F, we have ‖f.lift x‖ ≤ ‖f‖ * projectiveSeminorm x . This implies in particular:
• PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm: The injective seminorm is bounded above by the projective seminorm.
• PiTensorProduct.norm_eval_le_injectiveSeminorm: The main property of the injective seminorm on ⨂[𝕜] i, Eᵢ: for every x in ⨂[𝕜] i, Eᵢ and every continuous multilinear map f from E to a normed space F, we have ‖f.lift x‖ ≤ ‖f‖ * injectiveSeminorm x .
• PiTensorProduct.mapL_opNorm: If f is a family of continuous linear maps fᵢ : Eᵢ →L[𝕜] Fᵢ, then ‖PiTensorProduct.mapL f‖ ≤ ∏ i, ‖fᵢ‖.
• PiTensorProduct.mapLMultilinear_opNorm : If F is a normed vecteor space, then ‖mapLMultilinear 𝕜 E F‖ ≤ 1.

TODO (in a future PR)

If all Eᵢ are separated and satisfy SeparatingDual, then the seminorm on ⨂[𝕜] i, Eᵢ is a norm. This uses the construction of a basis of the PiTensorProduct, hence depends on PR #11156. It should probably go in a separate file, which is why I am creating a directory Analysis/NormedSpace/PiTensorProduct.

Technical issues

• Ideally, I would prefer not to define liftEquiv and to have only liftIsometry, but I am using liftEquiv.left_inv in the proof that liftIsometry preserves norms.