feat(NormedSpace): Move toSpanNonzeroSingleton to new file and add Li…

…nearIsometryEquiv (#10118)

Mathlib.lean

@@ -866,6 +866,7 @@ import Mathlib.Analysis.NormedSpace.QuaternionExponential
 import Mathlib.Analysis.NormedSpace.Ray
 import Mathlib.Analysis.NormedSpace.Real
 import Mathlib.Analysis.NormedSpace.RieszLemma
+import Mathlib.Analysis.NormedSpace.Span
 import Mathlib.Analysis.NormedSpace.Spectrum
 import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 import Mathlib.Analysis.NormedSpace.Star.Basic

Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean

@@ -3,8 +3,8 @@ Copyright (c) 2019 Jan-David Salchow. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
-import Mathlib.Analysis.NormedSpace.Basic
 import Mathlib.Topology.Algebra.Module.Basic
+import Mathlib.Analysis.Normed.MulAction
 
 #align_import analysis.normed_space.continuous_linear_map from "leanprover-community/mathlib"@"fe18deda804e30c594e75a6e5fe0f7d14695289f"
 
@@ -216,81 +216,3 @@ noncomputable def ContinuousLinearEquiv.ofHomothety (f : E ≃ₛₗ[σ] F) (a :
 #align continuous_linear_equiv.of_homothety ContinuousLinearEquiv.ofHomothety
 
 end Seminormed
-
-/-! ## The span of a single vector -/
-
-namespace ContinuousLinearMap
-
-variable (𝕜)
-
-section Seminormed
-
-variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
-
-theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
-    ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by
-  rw [mul_comm]
-  exact norm_smul _ _
-#align continuous_linear_map.to_span_singleton_homothety ContinuousLinearMap.toSpanSingleton_homothety
-
-end Seminormed
-
-end ContinuousLinearMap
-
-namespace ContinuousLinearEquiv
-
-variable (𝕜)
-
-section Seminormed
-variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
-
-theorem toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
-    ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
-  ContinuousLinearMap.toSpanSingleton_homothety _ _ _
-#align continuous_linear_equiv.to_span_nonzero_singleton_homothety ContinuousLinearEquiv.toSpanNonzeroSingleton_homothety
-
-end Seminormed
-
-section Normed
-variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
-
-/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
-    continuous linear equivalence from `E₁` to the span of `x`.-/
-noncomputable def toSpanNonzeroSingleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] 𝕜 ∙ x :=
-  ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ (norm_pos_iff.mpr h)
-    (toSpanNonzeroSingleton_homothety 𝕜 x h)
-#align continuous_linear_equiv.to_span_nonzero_singleton ContinuousLinearEquiv.toSpanNonzeroSingleton
-
-/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural continuous
-    linear map from the span of `x` to `𝕜`.-/
-noncomputable def coord (x : E) (h : x ≠ 0) : (𝕜 ∙ x) →L[𝕜] 𝕜 :=
-  (toSpanNonzeroSingleton 𝕜 x h).symm
-#align continuous_linear_equiv.coord ContinuousLinearEquiv.coord
-
-@[simp]
-theorem coe_toSpanNonzeroSingleton_symm {x : E} (h : x ≠ 0) :
-    ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h :=
-  rfl
-#align continuous_linear_equiv.coe_to_span_nonzero_singleton_symm ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm
-
-@[simp]
-theorem coord_toSpanNonzeroSingleton {x : E} (h : x ≠ 0) (c : 𝕜) :
-    coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c :=
-  (toSpanNonzeroSingleton 𝕜 x h).symm_apply_apply c
-#align continuous_linear_equiv.coord_to_span_nonzero_singleton ContinuousLinearEquiv.coord_toSpanNonzeroSingleton
-
-@[simp]
-theorem toSpanNonzeroSingleton_coord {x : E} (h : x ≠ 0) (y : 𝕜 ∙ x) :
-    toSpanNonzeroSingleton 𝕜 x h (coord 𝕜 x h y) = y :=
-  (toSpanNonzeroSingleton 𝕜 x h).apply_symm_apply y
-#align continuous_linear_equiv.to_span_nonzero_singleton_coord ContinuousLinearEquiv.toSpanNonzeroSingleton_coord
-
-@[simp]
-theorem coord_self (x : E) (h : x ≠ 0) :
-    (coord 𝕜 x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : 𝕜 ∙ x) = 1 :=
-  LinearEquiv.coord_self 𝕜 E x h
-#align continuous_linear_equiv.coord_self ContinuousLinearEquiv.coord_self
-
-end Normed
-
-end ContinuousLinearEquiv

Mathlib/Analysis/NormedSpace/OperatorNorm.lean

@@ -5,8 +5,7 @@ Authors: Jan-David Salchow, Sébastien Gouëzel, Jean Lo
 -/
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Analysis.Asymptotics.Asymptotics
-import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
-import Mathlib.Analysis.NormedSpace.LinearIsometry
+import Mathlib.Analysis.NormedSpace.Span
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
 import Mathlib.Topology.Algebra.Module.StrongTopology
 import Mathlib.Tactic.SuppressCompilation
@@ -2202,7 +2201,7 @@ theorem coord_norm (x : E) (h : x ≠ 0) : ‖coord 𝕜 x h‖ = ‖x‖⁻¹ :
   have hx : 0 < ‖x‖ := norm_pos_iff.mpr h
   haveI : Nontrivial (𝕜 ∙ x) := Submodule.nontrivial_span_singleton h
   exact ContinuousLinearMap.homothety_norm _ fun y =>
-    homothety_inverse _ hx _ (toSpanNonzeroSingleton_homothety 𝕜 x h) _
+    homothety_inverse _ hx _ (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h) _
 #align continuous_linear_equiv.coord_norm ContinuousLinearEquiv.coord_norm
 
 end

Mathlib/Analysis/NormedSpace/Span.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2024 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll
+-/
+
+import Mathlib.Analysis.NormedSpace.LinearIsometry
+import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
+import Mathlib.Analysis.NormedSpace.Basic
+
+/-!
+# The span of a single vector
+
+The equivalence of `𝕜` and `𝕜 • x` for `x ≠ 0` are defined as continuous linear equivalence and
+isometry.
+
+## Main definitions
+
+* `ContinuousLinearEquiv.toSpanNonzeroSingleton`: The continuous linear equivalence between `𝕜` and
+`𝕜 • x` for `x ≠ 0`.
+* `LinearIsometryEquiv.toSpanUnitSingleton`: For `‖x‖ = 1` the continuous linear equivalence is a
+linear isometry equivalence.
+
+-/
+
+variable {𝕜 E : Type*}
+
+namespace LinearMap
+
+variable (𝕜)
+
+section Seminormed
+
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
+theorem toSpanSingleton_homothety (x : E) (c : 𝕜) :
+    ‖LinearMap.toSpanSingleton 𝕜 E x c‖ = ‖x‖ * ‖c‖ := by
+  rw [mul_comm]
+  exact norm_smul _ _
+#align continuous_linear_map.to_span_singleton_homothety LinearMap.toSpanSingleton_homothety
+
+end Seminormed
+
+end LinearMap
+
+namespace ContinuousLinearEquiv
+
+variable (𝕜)
+
+section Seminormed
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
+theorem _root_.LinearEquiv.toSpanNonzeroSingleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
+    ‖LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h c‖ = ‖x‖ * ‖c‖ :=
+  LinearMap.toSpanSingleton_homothety _ _ _
+#align continuous_linear_equiv.to_span_nonzero_singleton_homothety LinearEquiv.toSpanNonzeroSingleton_homothety
+
+end Seminormed
+
+section Normed
+variable [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural
+    continuous linear equivalence from `E₁` to the span of `x`.-/
+noncomputable def toSpanNonzeroSingleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] 𝕜 ∙ x :=
+  ofHomothety (LinearEquiv.toSpanNonzeroSingleton 𝕜 E x h) ‖x‖ (norm_pos_iff.mpr h)
+    (LinearEquiv.toSpanNonzeroSingleton_homothety 𝕜 x h)
+#align continuous_linear_equiv.to_span_nonzero_singleton ContinuousLinearEquiv.toSpanNonzeroSingleton
+
+/-- Given a nonzero element `x` of a normed space `E₁` over a field `𝕜`, the natural continuous
+    linear map from the span of `x` to `𝕜`.-/
+noncomputable def coord (x : E) (h : x ≠ 0) : (𝕜 ∙ x) →L[𝕜] 𝕜 :=
+  (toSpanNonzeroSingleton 𝕜 x h).symm
+#align continuous_linear_equiv.coord ContinuousLinearEquiv.coord
+
+@[simp]
+theorem coe_toSpanNonzeroSingleton_symm {x : E} (h : x ≠ 0) :
+    ⇑(toSpanNonzeroSingleton 𝕜 x h).symm = coord 𝕜 x h :=
+  rfl
+#align continuous_linear_equiv.coe_to_span_nonzero_singleton_symm ContinuousLinearEquiv.coe_toSpanNonzeroSingleton_symm
+
+@[simp]
+theorem coord_toSpanNonzeroSingleton {x : E} (h : x ≠ 0) (c : 𝕜) :
+    coord 𝕜 x h (toSpanNonzeroSingleton 𝕜 x h c) = c :=
+  (toSpanNonzeroSingleton 𝕜 x h).symm_apply_apply c
+#align continuous_linear_equiv.coord_to_span_nonzero_singleton ContinuousLinearEquiv.coord_toSpanNonzeroSingleton
+
+@[simp]
+theorem toSpanNonzeroSingleton_coord {x : E} (h : x ≠ 0) (y : 𝕜 ∙ x) :
+    toSpanNonzeroSingleton 𝕜 x h (coord 𝕜 x h y) = y :=
+  (toSpanNonzeroSingleton 𝕜 x h).apply_symm_apply y
+#align continuous_linear_equiv.to_span_nonzero_singleton_coord ContinuousLinearEquiv.toSpanNonzeroSingleton_coord
+
+@[simp]
+theorem coord_self (x : E) (h : x ≠ 0) :
+    (coord 𝕜 x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : 𝕜 ∙ x) = 1 :=
+  LinearEquiv.coord_self 𝕜 E x h
+#align continuous_linear_equiv.coord_self ContinuousLinearEquiv.coord_self
+
+end Normed
+
+end ContinuousLinearEquiv
+
+namespace LinearIsometryEquiv
+
+variable [NormedDivisionRing 𝕜] [SeminormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+
+/-- Given a unit element `x` of a normed space `E` over a field `𝕜`, the natural
+    linear isometry equivalence from `E` to the span of `x`.-/
+noncomputable def toSpanUnitSingleton (x : E) (hx : ‖x‖ = 1) :
+    𝕜 ≃ₗᵢ[𝕜] 𝕜 ∙ x where
+  toLinearEquiv := LinearEquiv.toSpanNonzeroSingleton 𝕜 E x (by aesop)
+  norm_map' := by
+    intro
+    rw [LinearEquiv.toSpanNonzeroSingleton_homothety, hx, one_mul]
+
+@[simp] theorem toSpanUnitSingleton_apply (x : E) (hx : ‖x‖ = 1) (r : 𝕜) :
+    toSpanUnitSingleton x hx r = (⟨r • x, by aesop⟩ : 𝕜 ∙ x) := by
+  rfl

Mathlib/Data/IsROrC/Basic.lean

@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 import Mathlib.Data.Real.Sqrt
 import Mathlib.Analysis.NormedSpace.Star.Basic
 import Mathlib.Analysis.NormedSpace.ContinuousLinearMap
+import Mathlib.Analysis.NormedSpace.Basic
 
 #align_import data.is_R_or_C.basic from "leanprover-community/mathlib"@"baa88307f3e699fa7054ef04ec79fa4f056169cb"
 

Mathlib/LinearAlgebra/Span.lean

@@ -1099,12 +1099,14 @@ def toSpanNonzeroSingleton : R ≃ₗ[R] R ∙ x :=
     (LinearEquiv.ofEq (range <| toSpanSingleton R M x) (R ∙ x) (span_singleton_eq_range R M x).symm)
 #align linear_equiv.to_span_nonzero_singleton LinearEquiv.toSpanNonzeroSingleton
 
+@[simp] theorem toSpanNonzeroSingleton_apply (t : R) :
+    LinearEquiv.toSpanNonzeroSingleton R M x h t =
+      (⟨t • x, Submodule.smul_mem _ _ (Submodule.mem_span_singleton_self x)⟩ : R ∙ x) := by
+  rfl
+
 theorem toSpanNonzeroSingleton_one :
     LinearEquiv.toSpanNonzeroSingleton R M x h 1 =
-      (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) := by
-  apply SetLike.coe_eq_coe.mp
-  have : ↑(toSpanNonzeroSingleton R M x h 1) = toSpanSingleton R M x 1 := rfl
-  rw [this, toSpanSingleton_one, Submodule.coe_mk]
+      (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) := by simp
 #align linear_equiv.to_span_nonzero_singleton_one LinearEquiv.toSpanNonzeroSingleton_one
 
 /-- Given a nonzero element `x` of a torsion-free module `M` over a ring `R`, the natural