Exact source: MathlibAnnex/Analysis/Normed/Sphere/MetricRigidity.lean
Pinned GitHub source · Raw UTF-8 source
Back to The unit-sphere chord metric determines the ambient normed space
1import MathlibAnnex.Analysis.Normed.Sphere.ModelTransport2import MathlibAnnex.Analysis.Normed.Sphere.Dimension3import MathlibAnnex.Analysis.Normed.Sphere.RadialExtension4import Mathlib.Analysis.Normed.Operator.LinearIsometry56noncomputable section7set_option autoImplicit false8open Set9universe u v1011namespace MathlibAnnex.Sphere12namespace Internal13private noncomputable def coordinateEquivOfFinrankEq14 {n : ℕ} (X : Type u)15 [NormedAddCommGroup X] [NormedSpace ℝ X]16 [FiniteDimensional ℝ X]17 (h : n = Module.finrank ℝ X) : (Fin n → ℝ) ≃L[ℝ] X :=18 ContinuousLinearEquiv.ofFinrankEq (by19 change Module.finrank ℝ (Fin n → ℝ) = Module.finrank ℝ X20 calc21 Module.finrank ℝ (Fin n → ℝ) = n :=22 (Module.finrank_fin_fun ℝ :23 Module.finrank ℝ (Fin n → ℝ) = n)24 _ = Module.finrank ℝ X := h)25private theorem nonempty_linearIsometryEquiv_of_sphereIsometryEquiv26 {X : Type u} {Y : Type v}27 [NormedAddCommGroup X] [NormedSpace ℝ X]28 [NormedAddCommGroup Y] [NormedSpace ℝ Y]29 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]30 [Nontrivial X] [Nontrivial Y]31 (Δ : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by32 have hdim : Module.finrank ℝ X = Module.finrank ℝ Y :=33 finrank_eq Δ34 have hpos : 0 < Module.finrank ℝ X :=35 (Module.finrank_pos_iff (R := ℝ)).2 inferInstance36 let m : ℕ := Module.finrank ℝ X - 137 have hmX : m + 1 = Module.finrank ℝ X := by38 dsimp [m]39 omega40 have hmY : m + 1 = Module.finrank ℝ Y := hmX.trans hdim41 let eX : (Fin (m + 1) → ℝ) ≃L[ℝ] X :=42 coordinateEquivOfFinrankEq X hmX43 let eY : (Fin (m + 1) → ℝ) ≃L[ℝ] Y :=44 coordinateEquivOfFinrankEq Y hmY45 exact nonempty_linearIsometryEquiv_of_coordinate_model Δ eX eY4647end Internal48open Internal49private noncomputable def sphereIsoOfIsometrySurjective50 {X : Type u} {Y : Type v}51 [NormedAddCommGroup X] [NormedAddCommGroup Y]52 (f : (Metric.sphere (0 : X) 1) → (Metric.sphere (0 : Y) 1))53 (hf : Isometry f) (hsurj : Function.Surjective f) : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) where54 toEquiv := Equiv.ofBijective f ⟨hf.injective, hsurj⟩55 isometry_toFun := hf56noncomputable def isometryEquivOfLinearIsometryEquiv57 {X : Type u} {Y : Type v}58 [NormedAddCommGroup X] [NormedSpace ℝ X]59 [NormedAddCommGroup Y] [NormedSpace ℝ Y]60 (A : X ≃ₗᵢ[ℝ] Y) : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) where61 toEquiv := {62 toFun := fun u => ⟨A u.1, by63 apply mem_sphere_zero_iff_norm.mpr64 calc65 ‖A u.1‖ = ‖u.1‖ := A.norm_map u.166 _ = 1 := mem_sphere_zero_iff_norm.mp u.2⟩67 invFun := fun v => ⟨A.symm v.1, by68 apply mem_sphere_zero_iff_norm.mpr69 calc70 ‖A.symm v.1‖ = ‖v.1‖ := A.symm.norm_map v.171 _ = 1 := mem_sphere_zero_iff_norm.mp v.2⟩72 left_inv := by73 intro u74 apply Subtype.ext75 exact A.symm_apply_apply u.176 right_inv := by77 intro v78 apply Subtype.ext79 exact A.apply_symm_apply v.180 }81 isometry_toFun := by82 refine Isometry.of_dist_eq ?_83 intro u v84 change dist (A (u : X)) (A (v : X)) = dist u v85 calc86 dist (A (u : X)) (A (v : X)) = dist (u : X) (v : X) :=87 A.isometry.dist_eq _ _88 _ = dist u v :=89 (isometry_subtype_coe :90 Isometry ((↑) : (Metric.sphere (0 : X) 1) → X)).dist_eq u v91theorem nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional92 {X : Type u} {Y : Type v}93 [NormedAddCommGroup X] [NormedSpace ℝ X]94 [NormedAddCommGroup Y] [NormedSpace ℝ Y]95 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]96 (Δ : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by97 have hdim : Module.finrank ℝ X = Module.finrank ℝ Y :=98 finrank_eq Δ99 by_cases hzeroX : Module.finrank ℝ X = 0100 · have hzeroY : Module.finrank ℝ Y = 0 := hdim.symm.trans hzeroX101 letI : Subsingleton X :=102 (Module.finrank_zero_iff (R := ℝ) (M := X)).mp hzeroX103 letI : Subsingleton Y :=104 (Module.finrank_zero_iff (R := ℝ) (M := Y)).mp hzeroY105 exact ⟨{106 toLinearEquiv := LinearEquiv.ofSubsingleton X Y107 norm_map' := by108 intro x109 have hx : x = 0 := Subsingleton.elim _ _110 subst x111 simp }⟩112 · have hposX : 0 < Module.finrank ℝ X := Nat.pos_of_ne_zero hzeroX113 have hposY : 0 < Module.finrank ℝ Y := by114 rw [← hdim]115 exact hposX116 letI : Nontrivial X :=117 Module.nontrivial_of_finrank_pos (R := ℝ) hposX118 letI : Nontrivial Y :=119 Module.nontrivial_of_finrank_pos (R := ℝ) hposY120 exact nonempty_linearIsometryEquiv_of_sphereIsometryEquiv Δ121122/-- Function-form sphere-metric rigidity for all finite dimensions. -/123theorem nonempty_linearIsometryEquiv_of_isometry_surjective_finiteDimensional124 {X : Type u} {Y : Type v}125 [NormedAddCommGroup X] [NormedSpace ℝ X]126 [NormedAddCommGroup Y] [NormedSpace ℝ Y]127 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]128 (f : (Metric.sphere (0 : X) 1) → (Metric.sphere (0 : Y) 1))129 (hf : Isometry f) (hsurj : Function.Surjective f) :130 Nonempty (X ≃ₗᵢ[ℝ] Y) :=131 nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional132 (sphereIsoOfIsometrySurjective f hf hsurj)133134/-- The unit-sphere chord metric is a complete invariant in every finite dimension. -/135theorem nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_finiteDimensional136 {X : Type u} {Y : Type v}137 [NormedAddCommGroup X] [NormedSpace ℝ X]138 [NormedAddCommGroup Y] [NormedSpace ℝ Y]139 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y] :140 Nonempty ((Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) ↔ Nonempty (X ≃ₗᵢ[ℝ] Y) := by141 constructor142 · rintro ⟨Δ⟩143 exact nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional Δ144 · rintro ⟨A⟩145 exact ⟨isometryEquivOfLinearIsometryEquiv A⟩146theorem nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional_domain147 {X : Type u} {Y : Type v}148 [NormedAddCommGroup X] [NormedSpace ℝ X]149 [NormedAddCommGroup Y] [NormedSpace ℝ Y]150 [FiniteDimensional ℝ X]151 (Δ : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by152 letI : FiniteDimensional ℝ Y := finiteDimensional_codomain Δ153 exact nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional Δ154155/-- Sphere-metric rigidity when the target ambient space is finite-dimensional. -/156theorem nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional_codomain157 {X : Type u} {Y : Type v}158 [NormedAddCommGroup X] [NormedSpace ℝ X]159 [NormedAddCommGroup Y] [NormedSpace ℝ Y]160 [FiniteDimensional ℝ Y]161 (Δ : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by162 letI : FiniteDimensional ℝ X := finiteDimensional_domain Δ163 exact nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional Δ164165/-- Sphere-metric rigidity assuming that at least one ambient space is finite-dimensional. -/166theorem nonempty_linearIsometryEquiv_of_isometryEquiv_of_finiteDimensional167 {X : Type u} {Y : Type v}168 [NormedAddCommGroup X] [NormedSpace ℝ X]169 [NormedAddCommGroup Y] [NormedSpace ℝ Y]170 (hfin : FiniteDimensional ℝ X ∨ FiniteDimensional ℝ Y)171 (Δ : (Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) : Nonempty (X ≃ₗᵢ[ℝ] Y) := by172 rcases hfin with hX | hY173 · letI : FiniteDimensional ℝ X := hX174 exact nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional_domain Δ175 · letI : FiniteDimensional ℝ Y := hY176 exact nonempty_linearIsometryEquiv_of_isometryEquiv_finiteDimensional_codomain Δ177178/-- Function form of sphere-metric rigidity when one ambient space is finite-dimensional. -/179theorem nonempty_linearIsometryEquiv_of_isometry_surjective_of_finiteDimensional180 {X : Type u} {Y : Type v}181 [NormedAddCommGroup X] [NormedSpace ℝ X]182 [NormedAddCommGroup Y] [NormedSpace ℝ Y]183 (hfin : FiniteDimensional ℝ X ∨ FiniteDimensional ℝ Y)184 (f : (Metric.sphere (0 : X) 1) → (Metric.sphere (0 : Y) 1))185 (hf : Isometry f) (hsurj : Function.Surjective f) :186 Nonempty (X ≃ₗᵢ[ℝ] Y) :=187 nonempty_linearIsometryEquiv_of_isometryEquiv_of_finiteDimensional hfin188 (sphereIsoOfIsometrySurjective f hf hsurj)189190/-- If one ambient space is finite-dimensional, the unit-sphere chord metric191is a complete invariant of real normed spaces up to linear isometry. -/192theorem nonempty_isometryEquiv_iff_nonempty_linearIsometryEquiv_of_finiteDimensional193 {X : Type u} {Y : Type v}194 [NormedAddCommGroup X] [NormedSpace ℝ X]195 [NormedAddCommGroup Y] [NormedSpace ℝ Y]196 (hfin : FiniteDimensional ℝ X ∨ FiniteDimensional ℝ Y) :197 Nonempty ((Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1)) ↔ Nonempty (X ≃ₗᵢ[ℝ] Y) := by198 constructor199 · rintro ⟨Δ⟩200 exact nonempty_linearIsometryEquiv_of_isometryEquiv_of_finiteDimensional hfin Δ201 · rintro ⟨A⟩202 exact ⟨isometryEquivOfLinearIsometryEquiv A⟩203204end MathlibAnnex.Sphere