feat(Analysis/InnerProductSpace/TensorProduct): continuous version of TensorProduct.mk (#40340)

and isometric version of `TensorProduct.rid`.

Author: themathqueen

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

@@ -197,6 +197,19 @@ theorem ext_iff_inner_left_threefold {x y : E ⊗[𝕜] F ⊗[𝕜] G} :
   simpa only [← inner_conj_symm x, ← inner_conj_symm y, starRingEnd_apply, star_inj] using
     ext_iff_inner_right_threefold (x := x) (y := y)
 
+variable (𝕜 E F) in
+/-- The canonical continuous bilinear map `E → F → E ⊗ F`. This is the continuous version of
+`mk`. -/
+noncomputable def mkL : E →L[𝕜] F →L[𝕜] E ⊗[𝕜] F := (mk 𝕜 E F).mkContinuous₂ 1 fun _ _ ↦ by simp
+
+@[simp] lemma coe_mkL_apply (x : E) : ⇑(mkL 𝕜 E F x) = mk 𝕜 E F x := rfl
+@[simp] lemma toLinearMap₁₂_mkL : (mkL 𝕜 E F).toLinearMap₁₂ = mk 𝕜 E F := rfl
+@[simp] lemma toLinearMap_mkL_apply (x : E) : (mkL 𝕜 E F x).toLinearMap = mk 𝕜 E F x := rfl
+lemma mkL_apply_apply (x : E) (y : F) : mkL 𝕜 E F x y = x ⊗ₜ y := rfl
+
+@[fun_prop] lemma continuous_tmul : Continuous fun x : E × F ↦ x.1 ⊗ₜ[𝕜] x.2 :=
+  (mkL 𝕜 E F).continuous₂
+
 section isometry
 
 /-- The tensor product map of two linear isometries is a linear isometry. In particular, this is
@@ -360,21 +373,53 @@ variable (𝕜 E) in
 noncomputable def lidIsometry : 𝕜 ⊗[𝕜] E ≃ₗᵢ[𝕜] E :=
   TensorProduct.lid 𝕜 E |>.isometryOfInner inner_lid_lid
 
-@[simp] lemma lidIsometry_apply (x : 𝕜 ⊗[𝕜] E) :
-    lidIsometry 𝕜 E x = TensorProduct.lid 𝕜 E x := rfl
-@[simp] lemma lidIsometry_symm_apply (x : E) :
-    (lidIsometry 𝕜 E).symm x = 1 ⊗ₜ x := rfl
-
 @[simp] lemma toLinearEquiv_lidIsometry :
     (lidIsometry 𝕜 E).toLinearEquiv = TensorProduct.lid 𝕜 E := rfl
 
-@[simp] lemma norm_lid (x : 𝕜 ⊗[𝕜] E) :
-    ‖TensorProduct.lid 𝕜 E x‖ = ‖x‖ := lidIsometry 𝕜 E |>.norm_map x
-@[simp] lemma nnnorm_lid (x : 𝕜 ⊗[𝕜] E) :
-    ‖TensorProduct.lid 𝕜 E x‖₊ = ‖x‖₊ := lidIsometry 𝕜 E |>.nnnorm_map x
+lemma toContinuousLinearMap_symm_lidIsometry :
+    (lidIsometry 𝕜 E).symm.toContinuousLinearEquiv.toContinuousLinearMap = mkL 𝕜 𝕜 E 1 := rfl
+
+@[simp] lemma lidIsometry_apply (x : 𝕜 ⊗[𝕜] E) : lidIsometry 𝕜 E x = TensorProduct.lid 𝕜 E x := rfl
+@[simp] lemma lidIsometry_symm_apply (x : E) : (lidIsometry 𝕜 E).symm x = 1 ⊗ₜ x := rfl
+
+@[simp] lemma norm_lid (x) : ‖TensorProduct.lid 𝕜 E x‖ = ‖x‖ := (lidIsometry 𝕜 E).norm_map x
+@[simp] lemma nnnorm_lid (x) : ‖TensorProduct.lid 𝕜 E x‖₊ = ‖x‖₊ := lidIsometry 𝕜 E |>.nnnorm_map x
+
 @[simp] lemma enorm_lid (x : 𝕜 ⊗[𝕜] E) :
     ‖TensorProduct.lid 𝕜 E x‖ₑ = ‖x‖ₑ := lidIsometry 𝕜 E |>.toLinearIsometry.enorm_map x
 
+@[simp] theorem inner_rid_rid (x y : E ⊗[𝕜] 𝕜) :
+    inner 𝕜 (TensorProduct.rid 𝕜 E x) (TensorProduct.rid 𝕜 E y) = inner 𝕜 x y := by
+  simp [← lid_comm]
+
+variable (𝕜 E) in
+/-- The linear isometry equivalence version of `TensorProduct.rid`. -/
+noncomputable def ridIsometry : E ⊗[𝕜] 𝕜 ≃ₗᵢ[𝕜] E :=
+  TensorProduct.rid 𝕜 E |>.isometryOfInner inner_rid_rid
+
+@[simp] lemma toLinearEquiv_ridIsometry :
+    (ridIsometry 𝕜 E).toLinearEquiv = TensorProduct.rid 𝕜 E := rfl
+
+lemma toContinuousLinearMap_symm_ridIsometry :
+    (ridIsometry 𝕜 E).symm.toContinuousLinearEquiv.toContinuousLinearMap = (mkL 𝕜 E 𝕜).flip 1 := rfl
+
+@[simp] lemma ridIsometry_apply (x) : ridIsometry 𝕜 E x = TensorProduct.rid 𝕜 E x := rfl
+@[simp] lemma symm_ridIsometry_apply (x) : (ridIsometry 𝕜 E).symm x = x ⊗ₜ 1 := rfl
+
+lemma lidIsometry_eq_ridIsometry : lidIsometry 𝕜 𝕜 = ridIsometry 𝕜 𝕜 := by ext; simp [lid_eq_rid]
+
+@[simp] lemma norm_rid (x) : ‖TensorProduct.rid 𝕜 E x‖ = ‖x‖ := (ridIsometry 𝕜 E).norm_map x
+@[simp] lemma nnnorm_rid (x) : ‖TensorProduct.rid 𝕜 E x‖₊ = ‖x‖₊ := by simp [← NNReal.coe_inj]
+
+@[simp] lemma enorm_rid (x) : ‖TensorProduct.rid 𝕜 E x‖ₑ = ‖x‖ₑ :=
+  ridIsometry 𝕜 E |>.toLinearIsometry.enorm_map x
+
+@[simp] lemma commIsometry_trans_lidIsometry :
+    (commIsometry 𝕜 E 𝕜).trans (lidIsometry 𝕜 E) = ridIsometry 𝕜 E := by ext; simp
+
+@[simp] lemma commIsometry_trans_ridIsometry :
+    (commIsometry 𝕜 𝕜 E).trans (ridIsometry 𝕜 E) = lidIsometry 𝕜 E := by ext; simp
+
 @[simp] theorem inner_assoc_assoc (x y : E ⊗[𝕜] F ⊗[𝕜] G) :
     inner 𝕜 (TensorProduct.assoc 𝕜 E F G x) (TensorProduct.assoc 𝕜 E F G y) = inner 𝕜 x y :=
   x.induction_on (by simp) (fun a _ =>

Mathlib/LinearAlgebra/TensorProduct/Associator.lean

@@ -92,11 +92,19 @@ theorem comm_trans_lid :
     TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M = TensorProduct.rid R M :=
   LinearEquiv.toLinearMap_injective (ext (by ext; rfl))
 
+@[simp] lemma lid_comm (x) :
+    TensorProduct.lid R M (TensorProduct.comm R M R x) = TensorProduct.rid R M x :=
+  congr($comm_trans_lid _)
+
 @[simp]
 theorem comm_trans_rid :
     TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M = TensorProduct.lid R M :=
   LinearEquiv.toLinearMap_injective (ext (by ext; rfl))
 
+@[simp] lemma rid_comm (x) :
+    TensorProduct.rid R M (TensorProduct.comm R R M x) = TensorProduct.lid R M x :=
+  congr($comm_trans_rid _)
+
 variable (R) in
 theorem lid_eq_rid : TensorProduct.lid R R = TensorProduct.rid R R :=
   LinearEquiv.toLinearMap_injective <| ext' mul_comm