Exact source: MathlibAnnex/Analysis/Normed/Sphere/Dimension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Isometric unit spheres force equal finite dimensions
1import MathlibAnnex.Analysis.Normed.Sphere.RadialExtension2import Mathlib.Analysis.Normed.Module.FiniteDimension3import Mathlib.Topology.Algebra.Module.FiniteDimension4import Mathlib.Topology.Homeomorph.Lemmas5import Mathlib.Topology.MetricSpace.HausdorffDimension6import Mathlib.Tactic78/-!9# Finite-dimensional consequences of a unit-sphere isometry1011A bijective isometry between the unit spheres extends to a homeomorphism of the12ambient real normed spaces. Local compactness and Riesz's theorem transfer13finite-dimensionality from either ambient space to the other. If both spaces14are finite-dimensional, the two `finrank`s agree by the Hausdorff-dimension15comparison supplied by the forward and inverse `3`-Lipschitz radial maps.1617This file uses Mathlib's root-level `dimH` directly. It retains18`Module.finrank_pos_iff` as the designated positivity provider and therefore19introduces neither a Hausdorff-dimension compatibility alias nor a wrapper20theorem for positivity of `finrank`.21-/2223noncomputable section2425open Set Function26open scoped ENNReal2728namespace MathlibAnnex29namespace Sphere3031universe u v3233variable {X : Type u} {Y : Type v}34 [NormedAddCommGroup X] [NormedSpace ℝ X]35 [NormedAddCommGroup Y] [NormedSpace ℝ Y]3637/-- If the domain ambient space is finite-dimensional, then the codomain38ambient space is finite-dimensional. -/39theorem finiteDimensional_codomain40 [FiniteDimensional ℝ X]41 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :42 FiniteDimensional ℝ Y := by43 let h : X ≃ₜ Y := radialExtensionHomeomorph e44 letI : ProperSpace X := FiniteDimensional.proper_real X45 letI : LocallyCompactSpace Y :=46 h.locallyCompactSpace_iff.mp (inferInstance : LocallyCompactSpace X)47 exact FiniteDimensional.of_locallyCompactSpace ℝ4849/-- If the codomain ambient space is finite-dimensional, then the domain50ambient space is finite-dimensional. -/51theorem finiteDimensional_domain52 [FiniteDimensional ℝ Y]53 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :54 FiniteDimensional ℝ X :=55 finiteDimensional_codomain e.symm5657private theorem dimH_univ_le58 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]59 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :60 _root_.dimH (Set.univ : Set Y) ≤ _root_.dimH (Set.univ : Set X) := by61 have h := (lipschitzWith_radialExtension e).dimH_range_le62 rw [Set.range_eq_univ.mpr (radialExtension_surjective e)] at h63 exact h6465private theorem dimH_univ_ge66 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]67 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :68 _root_.dimH (Set.univ : Set X) ≤ _root_.dimH (Set.univ : Set Y) :=69 dimH_univ_le e.symm7071private theorem dimH_univ_eq72 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]73 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :74 _root_.dimH (Set.univ : Set X) = _root_.dimH (Set.univ : Set Y) :=75 le_antisymm (dimH_univ_ge e) (dimH_univ_le e)7677/-- A bijective isometry between unit spheres of finite-dimensional real normed78spaces forces equality of the ambient real dimensions. -/79theorem finrank_eq80 [FiniteDimensional ℝ X] [FiniteDimensional ℝ Y]81 (e : Metric.sphere (0 : X) 1 ≃ᵢ Metric.sphere (0 : Y) 1) :82 Module.finrank ℝ X = Module.finrank ℝ Y := by83 have h := dimH_univ_eq e84 rw [Real.dimH_univ_eq_finrank X, Real.dimH_univ_eq_finrank Y] at h85 exact_mod_cast h8687end Sphere88end MathlibAnnex