refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate injectiveSeminorm (leanprover-community#35569)

This PR:
* Deprecates `PiTensorProduct.injectiveSeminorm` and supporting lemmas.
* Moves the theory of `liftEquiv` from InjectiveSeminorm.lean to ProjectiveSeminorm.lean. 

No changes are introduced beyond adding deprecation notices, adapting docstrings, and moving material between files.

The PR leaves InjectiveSeminorm.lean almost empty. A new implementation of `injectiveSeminorm`, one which reflects the common mathematical definition, is to be done.

This is the third in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633).

Author: goliath-klein

Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean

@@ -11,79 +11,36 @@ import Mathlib.LinearAlgebra.Isomorphisms
 /-!
 # Injective seminorm on the tensor of a finite family of normed spaces.
 
-Let `𝕜` be a nontrivially 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
-"injective seminorm". It 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 purpose of this file is to develop the theory of the injective tensor norm.
 
-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.norm_eval_le_projectiveSeminorm`, this map lands in
-`ContinuousMultilinearMap 𝕜 E F →L[𝕜] F`. As this last space has a natural operator (semi)norm,
-we get an induced seminorm on `⨂[𝕜] i, Eᵢ`, which, by
-`PiTensorProduct.norm_eval_le_projectiveSeminorm`, is bounded above by the projective seminorm
-`PiTensorProduct.projectiveSeminorm`. We then take the `sup` of these seminorms as `F` varies;
-as this family of seminorms is bounded, its `sup` has good properties.
+A first formalization turned out not to capture the common mathematical definition and is
+now deprecated. See
 
-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 prove in
-`norm_eval_le_injectiveSeminorm` that this gives the same result, because every multilinear map
-from `E = Πᵢ Eᵢ` to `F` factors though a normed vector space in the same universe as
-`⨂[𝕜] i, Eᵢ`.
-
-We then prove the universal property and the functoriality of `⨂[𝕜] i, Eᵢ` as a normed vector
-space.
+https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633
 
 ## Main definitions
 
 * `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 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_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 = Πᵢ 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 vector space, then
-  `‖mapLMultilinear 𝕜 E F‖ ≤ 1`.
 
 ## TODO
 
-* 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 https://github.com/leanprover-community/mathlib4/pull/11156.
-  It should probably go in a separate file.
-
-* Adapt the remaining functoriality constructions/properties from `PiTensorProduct`.
+* Reimplement `injectiveSeminorm`.
 
 -/
 
 @[expose] public section
 
-universe uι u𝕜 uE uF
+-- These explicit universe variables are required by `injectiveSeminorm`, which
+-- has been marked as deprecated on 2026-06-10. TBD: delete the variables after the
+-- deprecated material has been removed or re-implemented.
+universe uι u𝕜 uE
 
 variable {ι : Type uι} [Fintype ι]
 variable {𝕜 : Type u𝕜} [NontriviallyNormedField 𝕜]
 variable {E : ι → Type uE} [∀ i, SeminormedAddCommGroup (E i)] [∀ i, NormedSpace 𝕜 (E i)]
-variable {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F]
 
 open scoped TensorProduct
 
@@ -116,11 +73,15 @@ theorem toDualContinuousMultilinearMap_le_projectiveSeminorm (x : ⨂[𝕜] i, E
 normed vector spaces `F`. In fact, we only take in the same universe as `⨂[𝕜] i, Eᵢ`, and then
 prove in `PiTensorProduct.norm_eval_le_injectiveSeminorm` that this gives the same result.
 -/
+@[deprecated
+  "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`"
+  (since := "2026-06-10")]
 noncomputable irreducible_def injectiveSeminorm : Seminorm 𝕜 (⨂[𝕜] i, E i) :=
   sSup {p | ∃ (G : Type (max uι u𝕜 uE)) (_ : SeminormedAddCommGroup G)
   (_ : NormedSpace 𝕜 G), p = Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
   (toDualContinuousMultilinearMap G (𝕜 := 𝕜) (E := E))}
 
+@[deprecated "no replacement" (since := "2026-06-10")]
 lemma dualSeminorms_bounded : BddAbove {p | ∃ (G : Type (max uι u𝕜 uE))
     (_ : SeminormedAddCommGroup G) (_ : NormedSpace 𝕜 G),
     p = Seminorm.comp (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G))
@@ -130,6 +91,9 @@ lemma dualSeminorms_bounded : BddAbove {p | ∃ (G : Type (max uι u𝕜 uE))
   intro p G _ _ hp x
   simpa [hp] using toDualContinuousMultilinearMap_le_projectiveSeminorm _
 
+@[deprecated
+  "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`"
+  (since := "2026-06-10")]
 theorem injectiveSeminorm_apply (x : ⨂[𝕜] i, E i) :
     injectiveSeminorm x = ⨆ p : {p | ∃ (G : Type (max uι u𝕜 uE))
     (_ : SeminormedAddCommGroup G) (_ : NormedSpace 𝕜 G), p = Seminorm.comp (normSeminorm 𝕜
@@ -138,6 +102,10 @@ theorem injectiveSeminorm_apply (x : ⨂[𝕜] i, E i) :
   simpa only [injectiveSeminorm, Set.coe_setOf, Set.mem_setOf_eq]
     using Seminorm.sSup_apply dualSeminorms_bounded
 
+attribute [-instance] instSeminormedAddCommGroup in
+@[deprecated
+  "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`"
+  (since := "2026-06-10")]
 theorem norm_eval_le_injectiveSeminorm (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
     ‖lift f.toMultilinearMap x‖ ≤ ‖f‖ * injectiveSeminorm x := by
     /- If `F` were in `Type (max uι u𝕜 uE)` (which is the type of `⨂[𝕜] i, E i`), then the
@@ -191,6 +159,9 @@ theorem norm_eval_le_injectiveSeminorm (f : ContinuousMultilinearMap 𝕜 E F) (
   rw [mul_comm]
   exact ContinuousLinearMap.le_opNorm _ _
 
+@[deprecated
+  "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`"
+  (since := "2026-06-10")]
 theorem injectiveSeminorm_le_projectiveSeminorm :
     injectiveSeminorm (𝕜 := 𝕜) (E := E) ≤ projectiveSeminorm := by
   rw [injectiveSeminorm]
@@ -208,188 +179,13 @@ theorem injectiveSeminorm_le_projectiveSeminorm :
     rw [h]; intro x; simp only [Seminorm.comp_apply, coe_normSeminorm]
     exact toDualContinuousMultilinearMap_le_projectiveSeminorm _
 
+@[deprecated
+  "`injectiveSeminorm` is deprecated in favor of the extensionally equal `projectiveSeminorm`"
+  (since := "2026-06-10")]
 theorem injectiveSeminorm_tprod_le (m : Π (i : ι), E i) :
     injectiveSeminorm (⨂ₜ[𝕜] i, m i) ≤ ∏ i, ‖m i‖ :=
   le_trans (injectiveSeminorm_le_projectiveSeminorm _) (projectiveSeminorm_tprod_le m)
 
--- Use `projectiveSeminorm` to turn the `PiTensorProduct` into a seminormed space.
--- The definition `injectiveSeminorm` is subject to deprecation in a follow-up PR. See:
--- https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633
-noncomputable instance : SeminormedAddCommGroup (⨂[𝕜] i, E i) :=
-  fast_instance% AddGroupSeminorm.toSeminormedAddCommGroup projectiveSeminorm.toAddGroupSeminorm
-
-noncomputable instance : NormedSpace 𝕜 (⨂[𝕜] i, E i) := ⟨projectiveSeminorm_smul_le⟩
-
-variable (𝕜 E F)
-
-/-- The linear equivalence between `ContinuousMultilinearMap 𝕜 E F` and `(⨂[𝕜] i, Eᵢ) →L[𝕜] F`
-induced by `PiTensorProduct.lift`, for every normed space `F`.
--/
-@[simps]
-noncomputable def liftEquiv : ContinuousMultilinearMap 𝕜 E F ≃ₗ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F where
-  toFun f := LinearMap.mkContinuous (lift f.toMultilinearMap) ‖f‖ fun x ↦
-    norm_eval_le_projectiveSeminorm f x
-  map_add' f g := by ext; simp
-  map_smul' a f := by ext; simp
-  invFun l := MultilinearMap.mkContinuous (lift.symm l.toLinearMap) ‖l‖ fun x ↦
-    ContinuousLinearMap.le_opNorm_of_le _ (projectiveSeminorm_tprod_le x)
-  left_inv f := by ext; simp
-  right_inv l := by
-    rw [← ContinuousLinearMap.coe_inj]
-    ext; simp
-
-/-- 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. -/
-noncomputable def liftIsometry : ContinuousMultilinearMap 𝕜 E F ≃ₗᵢ[𝕜] (⨂[𝕜] i, E i) →L[𝕜] F :=
-  LinearIsometryEquiv.ofBounds (liftEquiv 𝕜 E F)
-  (fun f ↦ LinearMap.mkContinuous_norm_le _ (norm_nonneg f) (norm_eval_le_projectiveSeminorm f))
-  (fun f ↦ by
-      rw [liftEquiv_symm_apply]
-      exact MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _)
-
-variable {𝕜 E F}
-
--- API missing for `LinearIsometryEquiv.ofBounds`?
-@[simp]
-theorem liftIsometry_apply_apply (f : ContinuousMultilinearMap 𝕜 E F) (x : ⨂[𝕜] i, E i) :
-    liftIsometry 𝕜 E F f x = lift f.toMultilinearMap x := by
-  simp [LinearIsometryEquiv.ofBounds, liftIsometry]
-
-variable (𝕜) in
-/-- The canonical continuous multilinear map from `E = Πᵢ Eᵢ` to `⨂[𝕜] i, Eᵢ`. -/
-@[simps! toFun]
-noncomputable def tprodL : ContinuousMultilinearMap 𝕜 E (⨂[𝕜] i, E i) :=
-  (liftIsometry 𝕜 E _).symm (ContinuousLinearMap.id 𝕜 _)
-
-@[simp]
-theorem tprodL_coe : (tprodL 𝕜).toMultilinearMap = tprod 𝕜 (s := E) := by
-  ext; simp
-
-@[simp]
-theorem liftIsometry_symm_apply (l : (⨂[𝕜] i, E i) →L[𝕜] F) :
-    (liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (tprodL 𝕜) := by
-  rfl
-
-@[simp]
-theorem liftIsometry_tprodL :
-    liftIsometry 𝕜 E _ (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] i, E i) := by
-  ext; simp
-
 end seminorm
 
-section map
-
-variable {E' E'' : ι → Type*}
-variable [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
-variable [∀ i, SeminormedAddCommGroup (E'' i)] [∀ i, NormedSpace 𝕜 (E'' i)]
-variable (g : Π i, E' i →L[𝕜] E'' i) (f : Π i, E i →L[𝕜] 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ᵢ`. -/
-noncomputable def mapL : (⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E' i :=
-  liftIsometry 𝕜 E _ <| (tprodL 𝕜).compContinuousLinearMap f
-
-@[simp]
-theorem mapL_coe : (mapL f).toLinearMap = map (fun i ↦ (f i).toLinearMap) := by
-  ext; simp [mapL]
-
-@[simp]
-theorem mapL_apply (x : ⨂[𝕜] i, E i) : mapL f x = map (fun i ↦ (f i).toLinearMap) x := by
-  rfl
-
-/-- Given submodules `pᵢ ⊆ Eᵢ`, this is the natural map: `⨂[𝕜] i, pᵢ → ⨂[𝕜] i, Eᵢ`.
-This is the continuous version of `PiTensorProduct.mapIncl`. -/
-@[simp]
-noncomputable def mapLIncl (p : Π i, Submodule 𝕜 (E i)) : (⨂[𝕜] i, p i) →L[𝕜] ⨂[𝕜] i, E i :=
-  mapL fun (i : ι) ↦ (p i).subtypeL
-
-theorem mapL_comp : mapL (fun (i : ι) ↦ g i ∘L f i) = mapL g ∘L mapL f := by
-  apply ContinuousLinearMap.coe_injective
-  ext; simp
-
-theorem liftIsometry_comp_mapL (h : ContinuousMultilinearMap 𝕜 E' F) :
-    liftIsometry 𝕜 E' F h ∘L mapL f = liftIsometry 𝕜 E F (h.compContinuousLinearMap f) := by
-  apply ContinuousLinearMap.coe_injective
-  ext; simp
-
-@[simp]
-theorem mapL_id : mapL (fun i ↦ ContinuousLinearMap.id 𝕜 (E i)) = ContinuousLinearMap.id _ _ := by
-  apply ContinuousLinearMap.coe_injective
-  ext; simp
-
-@[simp]
-theorem mapL_one : mapL (fun (i : ι) ↦ (1 : E i →L[𝕜] E i)) = 1 :=
-  mapL_id
-
-theorem mapL_mul (f₁ f₂ : Π i, E i →L[𝕜] E i) :
-    mapL (fun i ↦ f₁ i * f₂ i) = mapL f₁ * mapL f₂ :=
-  mapL_comp f₁ f₂
-
-/-- Upgrading `PiTensorProduct.mapL` to a `MonoidHom` when `E = E'`. -/
-@[simps]
-noncomputable def mapLMonoidHom : (Π i, E i →L[𝕜] E i) →* ((⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E i) where
-  toFun := mapL
-  map_one' := mapL_one
-  map_mul' := mapL_mul
-
-@[simp]
-protected theorem mapL_pow (f : Π i, E i →L[𝕜] E i) (n : ℕ) :
-    mapL (f ^ n) = mapL f ^ n := MonoidHom.map_pow mapLMonoidHom f n
-
--- We redeclare `ι` here, and later dependent arguments,
--- to avoid the `[Fintype ι]` assumption present throughout the rest of the file.
-open Function in
-private theorem mapL_add_smul_aux {ι : Type uι}
-    {E : ι → Type uE} [(i : ι) → SeminormedAddCommGroup (E i)] [(i : ι) → NormedSpace 𝕜 (E i)]
-    {E' : ι → Type u_1} [(i : ι) → SeminormedAddCommGroup (E' i)] [(i : ι) → NormedSpace 𝕜 (E' i)]
-    (f : (i : ι) → E i →L[𝕜] E' i) [DecidableEq ι] (i : ι) (u : E i →L[𝕜] E' i) :
-    (fun j ↦ (update f i u j).toLinearMap) =
-      update (fun j ↦ (f j).toLinearMap) i u.toLinearMap := by
-  grind
-
-open Function in
-protected theorem mapL_add [DecidableEq ι] (i : ι) (u v : E i →L[𝕜] E' i) :
-    mapL (update f i (u + v)) = mapL (update f i u) + mapL (update f i v) := by
-  ext
-  simp [mapL_add_smul_aux, PiTensorProduct.map_update_add]
-
-open Function in
-protected theorem mapL_smul [DecidableEq ι] (i : ι) (c : 𝕜) (u : E i →L[𝕜] E' i) :
-    mapL (update f i (c • u)) = c • mapL (update f i u) := by
-  ext
-  simp [mapL_add_smul_aux, PiTensorProduct.map_update_smul]
-
-theorem mapL_opNorm : ‖mapL f‖ ≤ ∏ i, ‖f i‖ := by
-  refine (ContinuousLinearMap.opNorm_le_iff (by positivity)).mpr fun x ↦ ?_
-  apply le_trans (norm_eval_le_projectiveSeminorm ..) (mul_le_mul_of_nonneg_right _ (norm_nonneg x))
-  refine (ContinuousMultilinearMap.opNorm_le_iff (by positivity)).mpr fun m ↦ ?_
-  apply le_trans (projectiveSeminorm_tprod_le fun i ↦ f i (m i))
-  rw [← Finset.prod_mul_distrib]
-  gcongr
-  exact ContinuousLinearMap.le_opNorm _ _
-
-variable (𝕜 E E')
-
-/-- The tensor of a family of linear maps from `Eᵢ` to `E'ᵢ`, as a continuous multilinear map of
-the family. -/
-@[simps! toFun_apply]
-noncomputable def mapLMultilinear : ContinuousMultilinearMap 𝕜 (fun (i : ι) ↦ E i →L[𝕜] E' i)
-    ((⨂[𝕜] i, E i) →L[𝕜] ⨂[𝕜] i, E' i) :=
-  MultilinearMap.mkContinuous
-  { toFun := mapL
-    map_update_smul' := fun _ _ _ _ ↦ PiTensorProduct.mapL_smul _ _ _ _
-    map_update_add' := fun _ _ _ _ ↦ PiTensorProduct.mapL_add _ _ _ _ }
-  1 (fun f ↦ by rw [one_mul]; exact mapL_opNorm f)
-
-variable {𝕜 E E'}
-
-theorem mapLMultilinear_opNorm : ‖mapLMultilinear 𝕜 E E'‖ ≤ 1 :=
-  MultilinearMap.mkContinuous_norm_le _ zero_le_one _
-
-end map
-
 end PiTensorProduct