refactor(*/Multilinear): change *.ofSubsingleton (#8694)

Change `MultilinearMap.ofSubsingleton` and other similar definitions
so that they are now equivalences between linear maps
and `1`-multilinear maps.

Mathlib/Analysis/NormedSpace/Multilinear.lean

@@ -488,32 +488,49 @@ theorem op_norm_pi {ι' : Type v'} [Fintype ι'] {E' : ι' → Type wE'}
 
 section
 
-variable (𝕜 G)
-
-theorem norm_ofSubsingleton_le [Subsingleton ι] (i' : ι) : ‖ofSubsingleton 𝕜 G i'‖ ≤ 1 :=
-  op_norm_le_bound _ zero_le_one fun m => by
-    rw [Fintype.prod_subsingleton _ i', one_mul, ofSubsingleton_apply]
-#align continuous_multilinear_map.norm_of_subsingleton_le ContinuousMultilinearMap.norm_ofSubsingleton_le
-
 @[simp]
-theorem norm_ofSubsingleton [Subsingleton ι] [Nontrivial G] (i' : ι) :
-    ‖ofSubsingleton 𝕜 G i'‖ = 1 := by
-  apply le_antisymm (norm_ofSubsingleton_le 𝕜 G i')
-  obtain ⟨g, hg⟩ := exists_ne (0 : G)
-  rw [← norm_ne_zero_iff] at hg
-  have := (ofSubsingleton 𝕜 G i').ratio_le_op_norm fun _ => g
-  rwa [Fintype.prod_subsingleton _ i', ofSubsingleton_apply, div_self hg] at this
-#align continuous_multilinear_map.norm_of_subsingleton ContinuousMultilinearMap.norm_ofSubsingleton
-
-theorem nnnorm_ofSubsingleton_le [Subsingleton ι] (i' : ι) : ‖ofSubsingleton 𝕜 G i'‖₊ ≤ 1 :=
-  norm_ofSubsingleton_le _ _ _
-#align continuous_multilinear_map.nnnorm_of_subsingleton_le ContinuousMultilinearMap.nnnorm_ofSubsingleton_le
+theorem norm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
+    ‖ofSubsingleton 𝕜 G G' i f‖ = ‖f‖ := by
+  letI : Unique ι := uniqueOfSubsingleton i
+  simp only [norm_def, ContinuousLinearMap.norm_def, (Equiv.funUnique _ _).symm.surjective.forall,
+    Fintype.prod_subsingleton _ i]; rfl
 
 @[simp]
-theorem nnnorm_ofSubsingleton [Subsingleton ι] [Nontrivial G] (i' : ι) :
-    ‖ofSubsingleton 𝕜 G i'‖₊ = 1 :=
-  NNReal.eq <| norm_ofSubsingleton _ _ _
-#align continuous_multilinear_map.nnnorm_of_subsingleton ContinuousMultilinearMap.nnnorm_ofSubsingleton
+theorem nnnorm_ofSubsingleton [Subsingleton ι] (i : ι) (f : G →L[𝕜] G') :
+    ‖ofSubsingleton 𝕜 G G' i f‖₊ = ‖f‖₊ :=
+  NNReal.eq <| norm_ofSubsingleton i f
+
+variable (𝕜 G)
+
+/-- Linear isometry between continuous linear maps from `G` to `G'`
+and continuous `1`-multilinear maps from `G` to `G'`. -/
+@[simps apply symm_apply]
+def ofSubsingletonₗᵢ [Subsingleton ι] (i : ι) :
+    (G →L[𝕜] G') ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ G) G' :=
+  { ofSubsingleton 𝕜 G G' i with
+    map_add' := fun _ _ ↦ rfl
+    map_smul' := fun _ _ ↦ rfl
+    norm_map' := norm_ofSubsingleton i }
+
+theorem norm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) :
+    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ ≤ 1 := by
+  rw [norm_ofSubsingleton]
+  apply ContinuousLinearMap.norm_id_le
+#align continuous_multilinear_map.norm_of_subsingleton_le ContinuousMultilinearMap.norm_ofSubsingleton_id_le
+
+theorem norm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
+    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ = 1 := by simp
+#align continuous_multilinear_map.norm_of_subsingleton ContinuousMultilinearMap.norm_ofSubsingleton_id
+
+theorem nnnorm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) :
+    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ ≤ 1 :=
+  norm_ofSubsingleton_id_le _ _ _
+#align continuous_multilinear_map.nnnorm_of_subsingleton_le ContinuousMultilinearMap.nnnorm_ofSubsingleton_id_le
+
+theorem nnnorm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) :
+    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖₊ = 1 :=
+  NNReal.eq <| norm_ofSubsingleton_id _ _ _
+#align continuous_multilinear_map.nnnorm_of_subsingleton ContinuousMultilinearMap.nnnorm_ofSubsingleton_id
 
 variable {G} (E)
 

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -1509,6 +1509,9 @@ theorem norm_id [Nontrivial E] : ‖id 𝕜 E‖ = 1 := by
   exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩
 #align continuous_linear_map.norm_id ContinuousLinearMap.norm_id
 
+@[simp]
+lemma nnnorm_id [Nontrivial E] : ‖id 𝕜 E‖₊ = 1 := NNReal.eq norm_id
+
 instance normOneClass [Nontrivial E] : NormOneClass (E →L[𝕜] E) :=
   ⟨norm_id⟩
 #align continuous_linear_map.norm_one_class ContinuousLinearMap.normOneClass

Mathlib/LinearAlgebra/Alternating/Basic.lean

@@ -434,19 +434,21 @@ end Module
 
 section
 
-variable (R M)
+variable (R M N)
 
-/-- The evaluation map from `ι → M` to `M` at a given `i` is alternating when `ι` is subsingleton.
--/
-@[simps]
-def ofSubsingleton [Subsingleton ι] (i : ι) : AlternatingMap R M M ι :=
-  { MultilinearMap.ofSubsingleton R M i with
-    toFun := Function.eval i
-    map_eq_zero_of_eq' := fun _ _ _ _ hij => (hij <| Subsingleton.elim _ _).elim }
+/-- The natural equivalence between linear maps from `M` to `N`
+and `1`-multilinear alternating maps from `M` to `N`. -/
+@[simps!]
+def ofSubsingleton [Subsingleton ι] (i : ι) : (M →ₗ[R] N) ≃ AlternatingMap R M N ι where
+  toFun f := ⟨MultilinearMap.ofSubsingleton R M N i f, fun _ _ _ _ ↦ absurd (Subsingleton.elim _ _)⟩
+  invFun f := (MultilinearMap.ofSubsingleton R M N i).symm f
+  left_inv _ := rfl
+  right_inv _ := coe_multilinearMap_injective <|
+    (MultilinearMap.ofSubsingleton R M N i).apply_symm_apply _
 #align alternating_map.of_subsingleton AlternatingMap.ofSubsingleton
-#align alternating_map.of_subsingleton_apply AlternatingMap.ofSubsingleton_apply
+#align alternating_map.of_subsingleton_apply AlternatingMap.ofSubsingleton_apply_apply
 
-variable (ι)
+variable (ι) {N}
 
 /-- The constant map is alternating when `ι` is empty. -/
 @[simps (config := .asFn)]

Mathlib/LinearAlgebra/Multilinear/Basic.lean

@@ -275,22 +275,24 @@ def pi {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)] [∀ i,
 
 section
 
-variable (R M₂)
+variable (R M₂ M₃)
 
-/-- The evaluation map from `ι → M₂` to `M₂` is multilinear at a given `i` when `ι` is subsingleton.
--/
+/-- Equivalence between linear maps `M₂ →ₗ[R] M₃` and one-multilinear maps. -/
 @[simps]
-def ofSubsingleton [Subsingleton ι] (i' : ι) : MultilinearMap R (fun _ : ι => M₂) M₂ where
-  toFun := Function.eval i'
-  map_add' m i x y := by
-    rw [Subsingleton.elim i i']
-    simp only [Function.eval, Function.update_same]
-  map_smul' m i r x := by
-    rw [Subsingleton.elim i i']
-    simp only [Function.eval, Function.update_same]
-#align multilinear_map.of_subsingleton MultilinearMap.ofSubsingleton
-#align multilinear_map.of_subsingleton_apply MultilinearMap.ofSubsingleton_apply
-
+def ofSubsingleton [Subsingleton ι] (i : ι) :
+    (M₂ →ₗ[R] M₃) ≃ MultilinearMap R (fun _ : ι ↦ M₂) M₃ where
+  toFun f :=
+    { toFun := fun x ↦ f (x i)
+      map_add' := by intros; simp [update_eq_const_of_subsingleton]
+      map_smul' := by intros; simp [update_eq_const_of_subsingleton] }
+  invFun f :=
+    { toFun := fun x ↦ f fun _ ↦ x
+      map_add' := fun x y ↦ by simpa [update_eq_const_of_subsingleton] using f.map_add 0 i x y
+      map_smul' := fun c x ↦ by simpa [update_eq_const_of_subsingleton] using f.map_smul 0 i c x }
+  left_inv f := rfl
+  right_inv f := by ext x; refine congr_arg f ?_; exact (eq_const_of_subsingleton _ _).symm
+#align multilinear_map.of_subsingleton MultilinearMap.ofSubsingletonₓ
+#align multilinear_map.of_subsingleton_apply MultilinearMap.ofSubsingleton_apply_applyₓ
 
 variable (M₁) {M₂}
 
@@ -839,6 +841,21 @@ instance [NoZeroSMulDivisors S M₂] : NoZeroSMulDivisors S (MultilinearMap R M
 
 variable (R S M₁ M₂ M₃)
 
+section OfSubsingleton
+
+variable [AddCommMonoid M₃] [Semiring S] [Module S M₃] [Module R M₃] [SMulCommClass R S M₃]
+
+/-- Linear equivalence between linear maps `M₂ →ₗ[R] M₃`
+and one-multilinear maps `MultilinearMap R (fun _ : ι ↦ M₂) M₃`. -/
+@[simps (config := { simpRhs := true })]
+def ofSubsingletonₗ [Subsingleton ι] (i : ι) :
+    (M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun _ : ι ↦ M₂) M₃ :=
+  { ofSubsingleton R M₂ M₃ i with
+    map_add' := fun _ _ ↦ rfl
+    map_smul' := fun _ _ ↦ rfl }
+
+end OfSubsingleton
+
 /-- The dependent version of `MultilinearMap.domDomCongrLinearEquiv`. -/
 @[simps apply symm_apply]
 def domDomCongrLinearEquiv' {ι' : Type*} (σ : ι ≃ ι') :

Mathlib/LinearAlgebra/PiTensorProduct.lean

@@ -562,22 +562,21 @@ Tensor product of `M` over a singleton set is equivalent to `M`
 -/
 @[simps symm_apply]
 def subsingletonEquiv [Subsingleton ι] (i₀ : ι) : (⨂[R] _ : ι, M) ≃ₗ[R] M where
-  toFun := lift (MultilinearMap.ofSubsingleton R M i₀)
+  toFun := lift (MultilinearMap.ofSubsingleton R M M i₀ .id)
   invFun m := tprod R fun _ ↦ m
   left_inv x := by
     dsimp only
-    have : ∀ (f : ι → M) (z : M), (fun _ : ι ↦ z) = update f i₀ z := by
-      intro f z
+    have : ∀ (f : ι → M) (z : M), (fun _ : ι ↦ z) = update f i₀ z := fun f z ↦ by
       ext i
       rw [Subsingleton.elim i i₀, Function.update_same]
     refine x.induction_on ?_ ?_
     · intro r f
-      simp only [LinearMap.map_smul, lift.tprod, ofSubsingleton_apply, Function.eval, this f,
-        MultilinearMap.map_smul, update_eq_self]
+      simp only [LinearMap.map_smul, LinearMap.id_apply, lift.tprod, ofSubsingleton_apply_apply,
+        this f, MultilinearMap.map_smul, update_eq_self]
     · intro x y hx hy
       rw [LinearMap.map_add, this 0 (_ + _), MultilinearMap.map_add, ← this 0 (lift _ _), hx,
         ← this 0 (lift _ _), hy]
-  right_inv t := by simp only [ofSubsingleton_apply, lift.tprod, Function.eval_apply]
+  right_inv t := by simp only [ofSubsingleton_apply_apply, LinearMap.id_apply, lift.tprod]
   map_add' := LinearMap.map_add _
   map_smul' := fun r x => by
     simp only

Mathlib/Topology/Algebra/Module/Alternating.lean

@@ -270,21 +270,27 @@ theorem pi_apply {ι' : Type*} {M' : ι' → Type*} [∀ i, AddCommMonoid (M' i)
 
 section
 
-variable (R M)
+variable (R M N)
 
-/-- The evaluation map from `ι → M` to `M` is alternating at a given `i` when `ι` is subsingleton.
--/
-@[simps! toContinuousMultilinearMap apply]
-def ofSubsingleton [Subsingleton ι] (i' : ι) : M [Λ^ι]→L[R] M :=
-  { AlternatingMap.ofSubsingleton R _ i' with
-    toContinuousMultilinearMap := ContinuousMultilinearMap.ofSubsingleton R _ i' }
+/-- The natural equivalence between continuous linear maps from `M` to `N`
+and continuous 1-multilinear alternating maps from `M` to `N`. -/
+@[simps! apply_apply symm_apply_apply apply_toContinuousMultilinearMap]
+def ofSubsingleton [Subsingleton ι] (i : ι) :
+    (M →L[R] N) ≃ M [Λ^ι]→L[R] N where
+  toFun f :=
+    { AlternatingMap.ofSubsingleton R M N i f with
+      toContinuousMultilinearMap := ContinuousMultilinearMap.ofSubsingleton R M N i f }
+  invFun f := (ContinuousMultilinearMap.ofSubsingleton R M N i).symm f.1
+  left_inv _ := rfl
+  right_inv _ := toContinuousMultilinearMap_injective <|
+    (ContinuousMultilinearMap.ofSubsingleton R M N i).apply_symm_apply _
 
 @[simp]
-theorem ofSubsingleton_toAlternatingMap [Subsingleton ι] (i' : ι) :
-    (ofSubsingleton R M i').toAlternatingMap = AlternatingMap.ofSubsingleton R M i' :=
+theorem ofSubsingleton_toAlternatingMap [Subsingleton ι] (i : ι) (f : M →L[R] N) :
+    (ofSubsingleton R M N i f).toAlternatingMap = AlternatingMap.ofSubsingleton R M N i f :=
   rfl
 
-variable (ι)
+variable (ι) {N}
 
 /-- The constant map is alternating when `ι` is empty. -/
 @[simps! toContinuousMultilinearMap apply]

Mathlib/Topology/Algebra/Module/Multilinear.lean

@@ -278,14 +278,20 @@ def codRestrict (f : ContinuousMultilinearMap R M₁ M₂) (p : Submodule R M₂
 
 section
 
-variable (R M₂)
-
-/-- The evaluation map from `ι → M₂` to `M₂` is multilinear at a given `i` when `ι` is subsingleton.
--/
-@[simps! toMultilinearMap apply]
-def ofSubsingleton [Subsingleton ι] (i' : ι) : ContinuousMultilinearMap R (fun _ : ι => M₂) M₂ where
-  toMultilinearMap := MultilinearMap.ofSubsingleton R _ i'
-  cont := continuous_apply _
+variable (R M₂ M₃)
+
+/-- The natural equivalence between continuous linear maps from `M₂` to `M₃`
+and continuous 1-multilinear maps from `M₂` to `M₃`. -/
+@[simps! apply_toMultilinearMap apply_apply symm_apply_apply]
+def ofSubsingleton [Subsingleton ι] (i : ι) :
+    (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun _ : ι => M₂) M₃ where
+  toFun f := ⟨MultilinearMap.ofSubsingleton R M₂ M₃ i f,
+    (map_continuous f).comp (continuous_apply i)⟩
+  invFun f := ⟨(MultilinearMap.ofSubsingleton R M₂ M₃ i).symm f.toMultilinearMap,
+    (map_continuous f).comp <| continuous_pi fun _ ↦ continuous_id⟩
+  left_inv _ := rfl
+  right_inv f := toMultilinearMap_injective <|
+    (MultilinearMap.ofSubsingleton R M₂ M₃ i).apply_symm_apply f.toMultilinearMap
 #align continuous_multilinear_map.of_subsingleton ContinuousMultilinearMap.ofSubsingleton
 
 variable (M₁) {M₂}