Exact source: Mathlib/Topology/Algebra/Module/FiniteDimension.lean
Pinned GitHub source · Raw UTF-8 source
Back to Finite-dimensionality transfers across a sphere isometry
1/-2Copyright (c) 2022 Anatole Dedecker. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Sébastien Gouëzel, Anatole Dedecker5-/6module78public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull9public import Mathlib.Analysis.LocallyConvex.Bounded10public import Mathlib.Analysis.Normed.Module.Basic11public import Mathlib.Analysis.SpecificLimits.Normed12public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas13public import Mathlib.RingTheory.LocalRing.Basic14public import Mathlib.Topology.Algebra.Module.Determinant15public import Mathlib.Topology.Algebra.Module.ModuleTopology16public import Mathlib.Topology.Algebra.Module.Simple17public import Mathlib.Topology.Algebra.Module.Complement18public import Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional19public import Mathlib.Topology.Maps.Strict.Basic2021/-!22# Finite-dimensional topological vector spaces over complete fields2324Let `𝕜` be a complete nontrivially normed field, and `E` a topological vector space (TVS) over25`𝕜` (i.e we have `[AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]`26and `[ContinuousSMul 𝕜 E]`).2728If `E` is finite dimensional and Hausdorff, then all linear maps from `E` to any other TVS are29continuous.3031When `E` is a normed space, this gets us the equivalence of norms in finite dimension.3233## Main results :3435* `LinearMap.continuous_iff_isClosed_ker` : a linear form is continuous if and only if its kernel36 is closed.37* `LinearMap.continuous_of_finiteDimensional` : a linear map on a finite-dimensional Hausdorff38 space over a complete field is continuous.3940## TODO4142Generalize more of `Mathlib/Analysis/Normed/Module/FiniteDimension.lean` to general TVSs.4344## Implementation detail4546The main result from which everything follows is the fact that, if `ξ : ι → E` is a finite basis,47then `ξ.equivFun : E →ₗ (ι → 𝕜)` is continuous. However, for technical reasons, it is easier to48prove this when `ι` and `E` live in the same universe. So we start by doing that as a private49lemma, then we deduce `LinearMap.continuous_of_finiteDimensional` from it, and then the general50result follows as `continuous_equivFun_basis`.5152-/5354@[expose] public section5556open Filter Module Set TopologicalSpace Topology5758universe u v w x5960noncomputable section6162section FiniteDimensional6364variable {𝕜 E F : Type*}65 [AddCommGroup E] [TopologicalSpace E]66 [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F]6768/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional. -/69instance ContinuousLinearMap.instModuleFinite [CommRing 𝕜] [Module 𝕜 E] [Module.Finite 𝕜 E]70 [Module 𝕜 F] [IsNoetherian 𝕜 F] [ContinuousConstSMul 𝕜 F] :71 Module.Finite 𝕜 (E →L[𝕜] F) :=72 .of_injective (ContinuousLinearMap.coeLM 𝕜 : (E →L[𝕜] F) →ₗ[𝕜] E →ₗ[𝕜] F)73 ContinuousLinearMap.coe_injective7475/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.7677This theorem is here to match searches looking for `FiniteDimensional` instead of `Module.Finite`.78We use a strictly more general `ContinuousLinearMap.instModuleFinite` as an instance. -/79protected theorem ContinuousLinearMap.finiteDimensional [Field 𝕜] [Module 𝕜 E]80 [FiniteDimensional 𝕜 E] [Module 𝕜 F] [FiniteDimensional 𝕜 F] [ContinuousConstSMul 𝕜 F] :81 FiniteDimensional 𝕜 (E →L[𝕜] F) :=82 inferInstance8384end FiniteDimensional8586section NormedField8788variable {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [AddCommGroup E] [Module 𝕜 E]89 [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {F : Type w} [AddCommGroup F]90 [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] {F' : Type x}91 [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] [IsTopologicalAddGroup F']92 [ContinuousSMul 𝕜 F']9394/-- If `𝕜` is a nontrivially normed field, any T2 topology on `𝕜` which makes it a topological95vector space over itself (with the norm topology) is *equal* to the norm topology. -/96theorem unique_topology_of_t2 {t : TopologicalSpace 𝕜} (h₁ : @IsTopologicalAddGroup 𝕜 t _)97 (h₂ : @ContinuousSMul 𝕜 𝕜 _ hnorm.toUniformSpace.toTopologicalSpace t) (h₃ : @T2Space 𝕜 t) :98 t = hnorm.toUniformSpace.toTopologicalSpace := by99 -- Let `𝓣₀` denote the topology on `𝕜` induced by the norm, and `𝓣` be any T2 vector100 -- topology on `𝕜`. To show that `𝓣₀ = 𝓣`, it suffices to show that they have the same101 -- neighborhoods of 0.102 refine IsTopologicalAddGroup.ext h₁ inferInstance (le_antisymm ?_ ?_)103 · -- To show `𝓣 ≤ 𝓣₀`, we have to show that closed balls are `𝓣`-neighborhoods of 0.104 rw [Metric.nhds_basis_closedBall.ge_iff]105 -- Let `ε > 0`. Since `𝕜` is nontrivially normed, we have `0 < ‖ξ₀‖ < ε` for some `ξ₀ : 𝕜`.106 intro ε hε107 rcases NormedField.exists_norm_lt 𝕜 hε with ⟨ξ₀, hξ₀, hξ₀ε⟩108 -- Since `ξ₀ ≠ 0` and `𝓣` is T2, we know that `{ξ₀}ᶜ` is a `𝓣`-neighborhood of 0.109 have : {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := IsOpen.mem_nhds isOpen_compl_singleton <|110 mem_compl_singleton_iff.mpr <| Ne.symm <| norm_ne_zero_iff.mp hξ₀.ne.symm111 -- Thus, its balanced core `𝓑` is too. Let's show that the closed ball of radius `ε` contains112 -- `𝓑`, which will imply that the closed ball is indeed a `𝓣`-neighborhood of 0.113 have : balancedCore 𝕜 {ξ₀}ᶜ ∈ @nhds 𝕜 t 0 := balancedCore_mem_nhds_zero this114 refine mem_of_superset this fun ξ hξ => ?_115 -- Let `ξ ∈ 𝓑`. We want to show `‖ξ‖ < ε`. If `ξ = 0`, this is trivial.116 by_cases hξ0 : ξ = 0117 · rw [hξ0]118 exact Metric.mem_closedBall_self hε.le119 · rw [mem_closedBall_zero_iff]120 -- Now suppose `ξ ≠ 0`. By contradiction, let's assume `ε < ‖ξ‖`, and show that121 -- `ξ₀ ∈ 𝓑 ⊆ {ξ₀}ᶜ`, which is a contradiction.122 by_contra! h123 suffices (ξ₀ * ξ⁻¹) • ξ ∈ balancedCore 𝕜 {ξ₀}ᶜ by124 rw [smul_eq_mul, mul_assoc, inv_mul_cancel₀ hξ0, mul_one] at this125 exact notMem_compl_iff.mpr (mem_singleton ξ₀) ((balancedCore_subset _) this)126 -- For that, we use that `𝓑` is balanced : since `‖ξ₀‖ < ε < ‖ξ‖`, we have `‖ξ₀ / ξ‖ ≤ 1`,127 -- hence `ξ₀ = (ξ₀ / ξ) • ξ ∈ 𝓑` because `ξ ∈ 𝓑`.128 refine (balancedCore_balanced _).smul_mem ?_ hξ129 rw [norm_mul, norm_inv, mul_inv_le_iff₀ (norm_pos_iff.mpr hξ0), one_mul]130 exact (hξ₀ε.trans h).le131 · -- Finally, to show `𝓣₀ ≤ 𝓣`, we simply argue that `id = (fun x ↦ x • 1)` is continuous from132 -- `(𝕜, 𝓣₀)` to `(𝕜, 𝓣)` because `(•) : (𝕜, 𝓣₀) × (𝕜, 𝓣) → (𝕜, 𝓣)` is continuous.133 calc134 @nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0 =135 map id (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) :=136 map_id.symm137 _ = map (fun x => id x • (1 : 𝕜)) (@nhds 𝕜 hnorm.toUniformSpace.toTopologicalSpace 0) := by138 simp139 _ ≤ @nhds 𝕜 t ((0 : 𝕜) • (1 : 𝕜)) :=140 (@Tendsto.smul_const _ _ _ hnorm.toUniformSpace.toTopologicalSpace t _ _ _ _ _141 tendsto_id (1 : 𝕜))142 _ = @nhds 𝕜 t 0 := by rw [zero_smul]143144/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if145its kernel is closed. -/146theorem LinearMap.continuous_of_isClosed_ker (l : E →ₗ[𝕜] 𝕜)147 (hl : IsClosed (LinearMap.ker l : Set E)) :148 Continuous l := by149 -- `l` is either constant or surjective. If it is constant, the result is trivial.150 by_cases H : finrank 𝕜 (LinearMap.range l) = 0151 · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H152 rw [H]153 exact continuous_zero154 · -- In the case where `l` is surjective, we factor it as `φ : (E ⧸ l.ker) ≃ₗ[𝕜] 𝕜`. Note that155 -- `E ⧸ l.ker` is T2 since `l.ker` is closed.156 have : finrank 𝕜 (LinearMap.range l) = 1 :=157 le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range l).finrank_le) (zero_lt_iff.mpr H)158 have hi : Function.Injective ((LinearMap.ker l).liftQ l (le_refl _)) := by159 rw [← LinearMap.ker_eq_bot]160 exact Submodule.ker_liftQ_eq_bot _ _ _ (le_refl _)161 have hs : Function.Surjective ((LinearMap.ker l).liftQ l (le_refl _)) := by162 rw [← LinearMap.range_eq_top, Submodule.range_liftQ]163 exact Submodule.eq_top_of_finrank_eq ((finrank_self 𝕜).symm ▸ this)164 let φ : (E ⧸ LinearMap.ker l) ≃ₗ[𝕜] 𝕜 :=165 LinearEquiv.ofBijective ((LinearMap.ker l).liftQ l (le_refl _)) ⟨hi, hs⟩166 have hlφ : (l : E → 𝕜) = φ ∘ (LinearMap.ker l).mkQ := by ext; rfl167 -- Since the quotient map `E →ₗ[𝕜] (E ⧸ l.ker)` is continuous, the continuity of `l` will follow168 -- form the continuity of `φ`.169 suffices Continuous φ.toEquiv by170 rw [hlφ]171 exact this.comp continuous_quot_mk172 -- The pullback by `φ.symm` of the quotient topology is a T2 topology on `𝕜`, because `φ.symm`173 -- is injective. Since `φ.symm` is linear, it is also a vector space topology.174 -- Hence, we know that it is equal to the topology induced by the norm.175 have : induced φ.toEquiv.symm inferInstance = hnorm.toUniformSpace.toTopologicalSpace := by176 refine unique_topology_of_t2 (topologicalAddGroup_induced φ.symm.toLinearMap)177 (continuousSMul_induced φ.symm.toMulActionHom) ?_178 rw [t2Space_iff]179 exact fun x y hxy =>180 @separated_by_continuous _ _ (induced _ _) _ _ _ continuous_induced_dom _ _181 (φ.toEquiv.symm.injective.ne hxy)182 -- Finally, the pullback by `φ.symm` is exactly the pushforward by `φ`, so we have to prove183 -- that `φ` is continuous when `𝕜` is endowed with the pushforward by `φ` of the quotient184 -- topology, which is trivial by definition of the pushforward.185 simp_rw +instances [this.symm, Equiv.induced_symm]186 exact continuous_coinduced_rng187188/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if189and only if its kernel is closed. -/190theorem LinearMap.continuous_iff_isClosed_ker (l : E →ₗ[𝕜] 𝕜) :191 Continuous l ↔ IsClosed (LinearMap.ker l : Set E) :=192 ⟨fun h => isClosed_singleton.preimage h, l.continuous_of_isClosed_ker⟩193194/-- Over a nontrivially normed field, any linear form which is nonzero on a nonempty open set is195automatically continuous. -/196theorem LinearMap.continuous_of_nonzero_on_open (l : E →ₗ[𝕜] 𝕜) (s : Set E) (hs₁ : IsOpen s)197 (hs₂ : s.Nonempty) (hs₃ : ∀ x ∈ s, l x ≠ 0) : Continuous l := by198 refine l.continuous_of_isClosed_ker (l.isClosed_or_dense_ker.resolve_right fun hl => ?_)199 rcases hs₂ with ⟨x, hx⟩200 have : x ∈ interior (LinearMap.ker l : Set E)ᶜ := by201 rw [mem_interior_iff_mem_nhds]202 exact mem_of_superset (hs₁.mem_nhds hx) hs₃203 rwa [hl.interior_compl] at this204205variable [CompleteSpace 𝕜]206207/-- This version imposes `ι` and `E` to live in the same universe, so you should instead use208`continuous_equivFun_basis` which gives the same result without universe restrictions. -/209private theorem continuous_equivFun_basis_aux [T2Space E] {ι : Type v} [Finite ι]210 (ξ : Basis ι 𝕜 E) : Continuous ξ.equivFun := by211 have := Fintype.ofFinite ι212 letI : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E213 letI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup214 suffices ∀ n, Fintype.card ι = n → Continuous ξ.equivFun by exact this _ rfl215 intro n hn216 induction n generalizing ι E with217 | zero =>218 rw [Fintype.card_eq_zero_iff] at hn219 exact continuous_of_const fun x y => funext hn.elim220 | succ n IH =>221 haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite222 -- first step: thanks to the induction hypothesis, any n-dimensional subspace is equivalent223 -- to a standard space of dimension n, hence it is complete and therefore closed.224 have H₁ : ∀ s : Submodule 𝕜 E, finrank 𝕜 s = n → IsClosed (s : Set E) := by225 intro s s_dim226 letI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup227 let b := Basis.ofVectorSpace 𝕜 s228 have U : IsUniformEmbedding b.equivFun.symm.toEquiv := by229 have : Fintype.card (Basis.ofVectorSpaceIndex 𝕜 s) = n := by230 rw [← s_dim]231 exact (finrank_eq_card_basis b).symm232 have : Continuous b.equivFun := IH b inferInstance this233 exact234 b.equivFun.symm.isUniformEmbedding b.equivFun.symm.toLinearMap.continuous_on_pi this235 have : IsComplete (s : Set E) :=236 completeSpace_coe_iff_isComplete.1 ((completeSpace_congr U).1 inferInstance)237 exact this.isClosed238 -- second step: any linear form is continuous, as its kernel is closed by the first step239 have H₂ : ∀ f : E →ₗ[𝕜] 𝕜, Continuous f := by240 intro f241 by_cases H : finrank 𝕜 (LinearMap.range f) = 0242 · rw [Submodule.finrank_eq_zero, LinearMap.range_eq_bot] at H243 rw [H]244 exact continuous_zero245 · have : finrank 𝕜 (LinearMap.ker f) = n := by246 have Z := f.finrank_range_add_finrank_ker247 rw [finrank_eq_card_basis ξ, hn] at Z248 have : finrank 𝕜 (LinearMap.range f) = 1 :=249 le_antisymm (finrank_self 𝕜 ▸ (LinearMap.range f).finrank_le) (zero_lt_iff.mpr H)250 rw [this, add_comm, Nat.add_one] at Z251 exact Nat.succ.inj Z252 have : IsClosed (LinearMap.ker f : Set E) := H₁ _ this253 exact LinearMap.continuous_of_isClosed_ker f this254 rw [continuous_pi_iff]255 intro i256 change Continuous (ξ.coord i)257 exact H₂ (ξ.coord i)258259/-- A finite-dimensional t2 vector space over a complete field must carry the module topology.260261Not declared as a global instance only for performance reasons. -/262@[local instance]263lemma isModuleTopologyOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] :264 IsModuleTopology 𝕜 E :=265 -- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equivFun_basis`, and266 -- use that it has the module topology267 let b := Basis.ofVectorSpace 𝕜 E268 have continuousEquiv : E ≃L[𝕜] (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜 :=269 { __ := b.equivFun270 continuous_toFun := continuous_equivFun_basis_aux b271 continuous_invFun := IsModuleTopology.continuous_of_linearMap (R := 𝕜)272 (A := (Basis.ofVectorSpaceIndex 𝕜 E) → 𝕜) (B := E) b.equivFun.symm }273 IsModuleTopology.iso continuousEquiv.symm274275/-- Any linear map on a finite-dimensional space over a complete field is continuous. -/276theorem LinearMap.continuous_of_finiteDimensional [T2Space E] [FiniteDimensional 𝕜 E]277 (f : E →ₗ[𝕜] F') : Continuous f :=278 IsModuleTopology.continuous_of_linearMap f279280instance LinearMap.continuousLinearMapClassOfFiniteDimensional [T2Space E] [FiniteDimensional 𝕜 E] :281 ContinuousLinearMapClass (E →ₗ[𝕜] F') 𝕜 E F' :=282 { LinearMap.semilinearMapClass with map_continuous := fun f => f.continuous_of_finiteDimensional }283284/-- In finite dimensions over a non-discrete complete normed field, the canonical identification285(in terms of a basis) with `𝕜^n` (endowed with the product topology) is continuous.286This is the key fact which makes all linear maps from a T2 finite-dimensional TVS over such a field287continuous (see `LinearMap.continuous_of_finiteDimensional`), which in turn implies that all288norms are equivalent in finite dimensions. -/289theorem continuous_equivFun_basis [T2Space E] {ι : Type*} [Finite ι] (ξ : Basis ι 𝕜 E) :290 Continuous ξ.equivFun :=291 haveI : FiniteDimensional 𝕜 E := ξ.finiteDimensional_of_finite292 ξ.equivFun.toLinearMap.continuous_of_finiteDimensional293294namespace LinearMap295296variable [T2Space E] [FiniteDimensional 𝕜 E]297298/-- The continuous linear map induced by a linear map on a finite-dimensional space -/299def toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F' where300 toFun f := ⟨f, f.continuous_of_finiteDimensional⟩301 invFun := (↑)302 map_add' _ _ := rfl303 map_smul' _ _ := rfl304 right_inv _ := ContinuousLinearMap.coe_injective rfl305306/-- Algebra equivalence between the linear maps and continuous linear maps on a finite-dimensional307space. -/308def _root_.Module.End.toContinuousLinearMap (E : Type v) [NormedAddCommGroup E]309 [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] : (E →ₗ[𝕜] E) ≃ₐ[𝕜] (E →L[𝕜] E) :=310 { LinearMap.toContinuousLinearMap with311 map_mul' := fun _ _ ↦ rfl312 commutes' := fun _ ↦ rfl }313314@[simp]315theorem coe_toContinuousLinearMap' (f : E →ₗ[𝕜] F') : ⇑(LinearMap.toContinuousLinearMap f) = f :=316 rfl317318@[simp]319theorem coe_toContinuousLinearMap (f : E →ₗ[𝕜] F') :320 ((LinearMap.toContinuousLinearMap f) : E →ₗ[𝕜] F') = f :=321 rfl322323@[simp]324theorem coe_toContinuousLinearMap_symm :325 ⇑(toContinuousLinearMap : (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F').symm =326 ((↑) : (E →L[𝕜] F') → E →ₗ[𝕜] F') :=327 rfl328329@[simp]330theorem det_toContinuousLinearMap (f : E →ₗ[𝕜] E) :331 (LinearMap.toContinuousLinearMap f).det = LinearMap.det f :=332 rfl333334@[deprecated coe_toContinuousLinearMap (since := "2025-12-23")]335theorem ker_toContinuousLinearMap (f : E →ₗ[𝕜] F') :336 (LinearMap.toContinuousLinearMap f).ker = ker f := by337 simp338339@[deprecated coe_toContinuousLinearMap (since := "2025-12-23")]340theorem range_toContinuousLinearMap (f : E →ₗ[𝕜] F') :341 (LinearMap.toContinuousLinearMap f).range = range f :=342 rfl343344/-- A surjective linear map `f` with finite-dimensional codomain is an open map. -/345theorem isOpenMap_of_finiteDimensional (f : F →ₗ[𝕜] E) (hf : Function.Surjective f) :346 IsOpenMap f :=347 IsModuleTopology.isOpenMap_of_surjective hf348349instance canLiftContinuousLinearMap : CanLift (E →ₗ[𝕜] F) (E →L[𝕜] F) (↑) fun _ => True :=350 ⟨fun f _ => ⟨LinearMap.toContinuousLinearMap f, rfl⟩⟩351352lemma toContinuousLinearMap_eq_iff_eq_toLinearMap (f : E →ₗ[𝕜] E) (g : E →L[𝕜] E) :353 f.toContinuousLinearMap = g ↔ f = g.toLinearMap := by354 simp [ContinuousLinearMap.ext_iff, LinearMap.ext_iff]355356lemma _root_.ContinuousLinearMap.toLinearMap_eq_iff_eq_toContinuousLinearMap (g : E →L[𝕜] E)357 (f : E →ₗ[𝕜] E) : g.toLinearMap = f ↔ g = f.toContinuousLinearMap := by358 simp [ContinuousLinearMap.ext_iff, LinearMap.ext_iff]359360end LinearMap361362section363364variable [T2Space E] [T2Space F] [FiniteDimensional 𝕜 E]365366namespace LinearEquiv367368/-- The continuous linear equivalence induced by a linear equivalence on a finite-dimensional369space. -/370def toContinuousLinearEquiv (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F :=371 { e with372 continuous_toFun := e.toLinearMap.continuous_of_finiteDimensional373 continuous_invFun :=374 haveI : FiniteDimensional 𝕜 F := e.finiteDimensional375 e.symm.toLinearMap.continuous_of_finiteDimensional }376377@[simp]378theorem coe_toContinuousLinearEquiv (e : E ≃ₗ[𝕜] F) : (e.toContinuousLinearEquiv : E →ₗ[𝕜] F) = e :=379 rfl380381@[simp]382theorem coe_toContinuousLinearEquiv' (e : E ≃ₗ[𝕜] F) : (e.toContinuousLinearEquiv : E → F) = e :=383 rfl384385@[simp]386theorem coe_toContinuousLinearEquiv_symm (e : E ≃ₗ[𝕜] F) :387 (e.toContinuousLinearEquiv.toLinearEquiv.symm : F →ₗ[𝕜] E) = e.symm := rfl388389@[simp]390theorem coe_toContinuousLinearEquiv_symm' (e : E ≃ₗ[𝕜] F) :391 (e.toContinuousLinearEquiv.symm : F → E) = e.symm :=392 rfl393394@[simp]395theorem toLinearEquiv_toContinuousLinearEquiv (e : E ≃ₗ[𝕜] F) :396 e.toContinuousLinearEquiv.toLinearEquiv = e := by397 ext x398 rfl399400theorem toLinearEquiv_toContinuousLinearEquiv_symm (e : E ≃ₗ[𝕜] F) :401 e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm := by402 ext x403 rfl404405instance canLiftContinuousLinearEquiv :406 CanLift (E ≃ₗ[𝕜] F) (E ≃L[𝕜] F) ContinuousLinearEquiv.toLinearEquiv fun _ => True :=407 ⟨fun f _ => ⟨_, f.toLinearEquiv_toContinuousLinearEquiv⟩⟩408409end LinearEquiv410411variable [FiniteDimensional 𝕜 F]412413/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously414linearly equivalent if they have the same (finite) dimension. -/415theorem FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq416 (cond : finrank 𝕜 E = finrank 𝕜 F) : Nonempty (E ≃L[𝕜] F) :=417 (nonempty_linearEquiv_of_finrank_eq cond).map LinearEquiv.toContinuousLinearEquiv418419/-- Two finite-dimensional topological vector spaces over a complete normed field are continuously420linearly equivalent if and only if they have the same (finite) dimension. -/421theorem FiniteDimensional.nonempty_continuousLinearEquiv_iff_finrank_eq :422 Nonempty (E ≃L[𝕜] F) ↔ finrank 𝕜 E = finrank 𝕜 F :=423 ⟨fun ⟨h⟩ => h.toLinearEquiv.finrank_eq, fun h =>424 FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq h⟩425426/-- A continuous linear equivalence between two finite-dimensional topological vector spaces over a427complete normed field of the same (finite) dimension. -/428def ContinuousLinearEquiv.ofFinrankEq (cond : finrank 𝕜 E = finrank 𝕜 F) : E ≃L[𝕜] F :=429 (LinearEquiv.ofFinrankEq E F cond).toContinuousLinearEquiv430431end432433namespace Module.Basis434variable {ι : Type*} [Finite ι] [T2Space E]435436/-- Construct a continuous linear map given the value at a finite basis. -/437def constrL (v : Basis ι 𝕜 E) (f : ι → F) : E →L[𝕜] F :=438 haveI : FiniteDimensional 𝕜 E := v.finiteDimensional_of_finite439 LinearMap.toContinuousLinearMap (v.constr 𝕜 f)440441@[simp]442theorem coe_constrL (v : Basis ι 𝕜 E) (f : ι → F) : (v.constrL f : E →ₗ[𝕜] F) = v.constr 𝕜 f :=443 rfl444445/-- The continuous linear equivalence between a vector space over `𝕜` with a finite basis and446functions from its basis indexing type to `𝕜`. -/447@[simps! apply]448def equivFunL (v : Basis ι 𝕜 E) : E ≃L[𝕜] ι → 𝕜 :=449 { v.equivFun with450 continuous_toFun :=451 haveI : FiniteDimensional 𝕜 E := v.finiteDimensional_of_finite452 v.equivFun.toLinearMap.continuous_of_finiteDimensional453 continuous_invFun := by454 change Continuous v.equivFun.symm.toFun455 exact v.equivFun.symm.toLinearMap.continuous_of_finiteDimensional }456457@[simp]458lemma equivFunL_symm_apply_repr (v : Basis ι 𝕜 E) (x : E) :459 v.equivFunL.symm (v.repr x) = x :=460 v.equivFunL.symm_apply_apply x461462@[simp]463theorem constrL_apply {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) (f : ι → F) (e : E) :464 v.constrL f e = ∑ i, v.equivFun e i • f i :=465 v.constr_apply_fintype 𝕜 _ _466467@[simp 1100]468theorem constrL_basis (v : Basis ι 𝕜 E) (f : ι → F) (i : ι) : v.constrL f (v i) = f i :=469 v.constr_basis 𝕜 _ _470471end Module.Basis472473namespace ContinuousLinearMap474475variable [T2Space E] [FiniteDimensional 𝕜 E]476477/-- Builds a continuous linear equivalence from a continuous linear map on a finite-dimensional478vector space whose determinant is nonzero. -/479def toContinuousLinearEquivOfDetNeZero (f : E →L[𝕜] E) (hf : f.det ≠ 0) : E ≃L[𝕜] E :=480 ((f : E →ₗ[𝕜] E).equivOfDetNeZero hf).toContinuousLinearEquiv481482@[simp]483theorem coe_toContinuousLinearEquivOfDetNeZero (f : E →L[𝕜] E) (hf : f.det ≠ 0) :484 (f.toContinuousLinearEquivOfDetNeZero hf : E →L[𝕜] E) = f := by485 ext x486 rfl487488@[simp]489theorem toContinuousLinearEquivOfDetNeZero_apply (f : E →L[𝕜] E) (hf : f.det ≠ 0) (x : E) :490 f.toContinuousLinearEquivOfDetNeZero hf x = f x :=491 rfl492493theorem _root_.Matrix.toLin_finTwoProd_toContinuousLinearMap (a b c d : 𝕜) :494 LinearMap.toContinuousLinearMap495 (Matrix.toLin (Basis.finTwoProd 𝕜) (Basis.finTwoProd 𝕜) !![a, b; c, d]) =496 (a • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + b • ContinuousLinearMap.snd 𝕜 𝕜 𝕜).prod497 (c • ContinuousLinearMap.fst 𝕜 𝕜 𝕜 + d • ContinuousLinearMap.snd 𝕜 𝕜 𝕜) :=498 ContinuousLinearMap.ext <| Matrix.toLin_finTwoProd_apply _ _ _ _499500end ContinuousLinearMap501502end NormedField503504section IsUniformAddGroup505506variable (𝕜 E : Type*) [NontriviallyNormedField 𝕜]507 [CompleteSpace 𝕜] [AddCommGroup E] [UniformSpace E] [T2Space E] [IsUniformAddGroup E]508 [Module 𝕜 E] [ContinuousSMul 𝕜 E]509510include 𝕜 in511theorem FiniteDimensional.complete [FiniteDimensional 𝕜 E] : CompleteSpace E := by512 set e := ContinuousLinearEquiv.ofFinrankEq (@finrank_fin_fun 𝕜 _ _ (finrank 𝕜 E)).symm513 have : IsUniformEmbedding e.toEquiv.symm := e.symm.isUniformEmbedding514 exact (completeSpace_congr this).1 inferInstance515516variable {𝕜 E}517518/-- A finite-dimensional subspace is complete. -/519theorem Submodule.complete_of_finiteDimensional (s : Submodule 𝕜 E) [FiniteDimensional 𝕜 s] :520 IsComplete (s : Set E) :=521 haveI : IsUniformAddGroup s := s.toAddSubgroup.isUniformAddGroup522 completeSpace_coe_iff_isComplete.1 (FiniteDimensional.complete 𝕜 s)523524end IsUniformAddGroup525526variable {𝕜 E F : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]527 [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module 𝕜 E]528 [ContinuousSMul 𝕜 E]529 [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F]530 [ContinuousSMul 𝕜 F]531532/-- A finite-dimensional subspace is closed. -/533theorem Submodule.closed_of_finiteDimensional534 [T2Space E] (s : Submodule 𝕜 E) [FiniteDimensional 𝕜 s] :535 IsClosed (s : Set E) :=536 letI := IsTopologicalAddGroup.rightUniformSpace E537 haveI : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup538 s.complete_of_finiteDimensional.isClosed539540/-- If `s` is a closed subspace with finite codimension, any subspace containing `s` is closed. -/541theorem Submodule.isClosed_mono_of_finiteDimensional_quotient542 {s t : Submodule 𝕜 E} [FiniteDimensional 𝕜 (E ⧸ s)] (s_closed : IsClosed (s : Set E))543 (s_le_t : s ≤ t) :544 IsClosed (t : Set E) := by545 rw [show t = comap s.mkQ (map s.mkQ t) by simpa]546 exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk547548/-- The supremum of a closed subspace and a finite dimensional subspace is closed. -/549theorem Submodule.isClosed_sup_finiteDimensional550 (s t : Submodule 𝕜 E) (hs : IsClosed (s : Set E)) [ht : FiniteDimensional 𝕜 t] :551 IsClosed ((s ⊔ t : Submodule 𝕜 E) : Set E) := by552 rw [← comap_map_mkQ]553 exact (map s.mkQ t).closed_of_finiteDimensional.preimage continuous_quot_mk554555/-- An injective linear map with finite-dimensional domain is a closed embedding. -/556theorem LinearMap.isClosedEmbedding_of_injective [T2Space E] [FiniteDimensional 𝕜 E] [T2Space F]557 {f : E →ₗ[𝕜] F} (hf : LinearMap.ker f = ⊥) : IsClosedEmbedding f :=558 let g := LinearEquiv.ofInjective f (LinearMap.ker_eq_bot.mp hf)559 { IsEmbedding.subtypeVal.comp g.toContinuousLinearEquiv.toHomeomorph.isEmbedding with560 isClosed_range := by561 simpa [LinearMap.coe_range f] using (LinearMap.range f).closed_of_finiteDimensional }562563theorem isClosedEmbedding_smul_left [T2Space E] {c : E} (hc : c ≠ 0) :564 IsClosedEmbedding fun x : 𝕜 => x • c :=565 LinearMap.isClosedEmbedding_of_injective (LinearMap.ker_toSpanSingleton 𝕜 hc)566567-- `smul` is a closed map in the first argument.568theorem isClosedMap_smul_left [T2Space E] (c : E) : IsClosedMap fun x : 𝕜 => x • c := by569 by_cases hc : c = 0570 · simp_rw [hc, smul_zero]571 exact isClosedMap_const572 · exact (isClosedEmbedding_smul_left hc).isClosedMap573574theorem ContinuousLinearMap.exists_rightInverse_of_surjective [T2Space F] [FiniteDimensional 𝕜 F]575 (f : E →L[𝕜] F) (hf : f.range = ⊤) : ∃ g : F →L[𝕜] E, f.comp g = ContinuousLinearMap.id 𝕜 F :=576 let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_rightInverse_of_surjective hf577 ⟨LinearMap.toContinuousLinearMap g, ContinuousLinearMap.coe_inj.1 hg⟩578579@[deprecated (since := "2026-04-24")]580alias ContinuousLinearMap.exists_right_inverse_of_surjective :=581 ContinuousLinearMap.exists_rightInverse_of_surjective582583theorem ContinuousLinearMap.isQuotientMap_of_finiteDimensional [T2Space F] [FiniteDimensional 𝕜 F]584 (f : E →L[𝕜] F) (hf : f.range = ⊤) :585 IsQuotientMap f :=586 let ⟨g, hg⟩ := f.exists_rightInverse_of_surjective hf587 .of_inverse g.continuous f.continuous (fun _ ↦ congr($hg _))588589theorem ContinuousLinearMap.isStrictMap_of_finiteDimensional [T2Space F] [FiniteDimensional 𝕜 F]590 (f : E →L[𝕜] F) :591 IsStrictMap f := by592 rw [isStrictMap_iff_isQuotientMap_rangeFactorization]593 exact f.rangeRestrict.isQuotientMap_of_finiteDimensional (by simp)594595/-- If `K` is a complete field and `V` is a finite-dimensional vector space over `K` (equipped with596any topology so that `V` is a topological `K`-module, meaning `[IsTopologicalAddGroup V]`597and `[ContinuousSMul K V]`), and `K` is locally compact, then `V` is locally compact.598599This is not an instance because `K` cannot be inferred. -/600theorem LocallyCompactSpace.of_finiteDimensional_of_complete (K V : Type*)601 [NontriviallyNormedField K] [CompleteSpace K] [LocallyCompactSpace K]602 [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V]603 [Module K V] [ContinuousSMul K V] [FiniteDimensional K V] :604 LocallyCompactSpace V :=605 -- Reduce to `SeparationQuotient V`, which is a `T2Space`.606 suffices LocallyCompactSpace (SeparationQuotient V) from607 SeparationQuotient.isInducing_mk.locallyCompactSpace <|608 SeparationQuotient.range_mk (X := V) ▸ isClosed_univ.isLocallyClosed609 let ⟨_, ⟨b⟩⟩ := Basis.exists_basis K (SeparationQuotient V)610 have := FiniteDimensional.fintypeBasisIndex b611 b.equivFun.toContinuousLinearEquiv.toHomeomorph.isOpenEmbedding.locallyCompactSpace612613section Riesz614615variable (𝕜 : Type*) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]616 {E Eᵤ : Type*} [AddCommGroup E] [AddCommGroup Eᵤ] [Module 𝕜 E] [Module 𝕜 Eᵤ]617 [TopologicalSpace E] [UniformSpace Eᵤ] [T2Space E] [T2Space Eᵤ]618 [IsTopologicalAddGroup E] [IsUniformAddGroup Eᵤ]619 [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 Eᵤ]620621open scoped Pointwise in622/-- **Riesz's theorem**: a T2 topological vector space over a complete non-trivial normed field623which admits a totally bounded neighborhood of `0` is finite-dimensional. -/624theorem FiniteDimensional.of_totallyBounded_nhds_zero {U : Set Eᵤ} (hU_nhds : U ∈ 𝓝 (0 : Eᵤ))625 (hU_tb : TotallyBounded U) : FiniteDimensional 𝕜 Eᵤ := by626 obtain ⟨c, hc0, hc1⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < 1 := NormedField.exists_norm_lt 𝕜 zero_lt_one627 have hc_ne : c ≠ 0 := norm_pos_iff.mp hc0628 obtain ⟨F, hF_finite, hF_cover⟩ := totallyBounded_iff_subset_finite_iUnion_nhds_zero.mp hU_tb629 (c • U) ((set_smul_mem_nhds_zero_iff hc_ne).mpr hU_nhds)630 let M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F631 letI : FiniteDimensional 𝕜 M := Finite.span_of_finite 𝕜 hF_finite632 have h_cover : U ⊆ M + c • U := fun x hx ↦ by633 obtain ⟨f, hf, y, hy, rfl⟩ := Set.mem_iUnion₂.mp <| hF_cover hx634 exact ⟨f, Submodule.subset_span hf, y, hy, rfl⟩635 have h_ind (n : ℕ) : U ⊆ M + c ^ n • U := by636 induction n with637 | zero => simpa using! fun x hx ↦ ⟨0, M.zero_mem, x, hx, zero_add x⟩638 | succ n ih =>639 calc640 U ⊆ M + c ^ n • U := ih641 _ ⊆ M + c ^ n • (M + c • U) := by gcongr642 _ ⊆ M + c ^ (n + 1) • U := by643 rw [smul_add, smul_smul, pow_succ, ← add_assoc]644 congr!645 lift c to 𝕜ˣ using isUnit_iff_ne_zero.mpr hc_ne646 simp [← Units.val_pow_eq_pow_val, ← Units.smul_def]647 have h_small : Tendsto (fun n ↦ c ^ n • U) atTop (𝓝 0).smallSets :=648 (TotallyBounded.isVonNBounded 𝕜 hU_tb).tendsto_smallSets_nhds.comp649 (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc1)650 have hU_sub_M : U ⊆ M := by651 intro x hx652 choose m hm u hu h_eq using fun n ↦ h_ind n hx653 have hu_tendsto : Tendsto u atTop (𝓝 0) := by654 intro W hW655 exact (tendsto_smallSets_iff.mp h_small W hW).mono fun n hn ↦ hn (hu n)656 have hm_tendsto : Tendsto m atTop (𝓝 x) := by657 simpa [show m = fun n ↦ x - u n by grind] using! tendsto_const_nhds.sub hu_tendsto658 exact M.closed_of_finiteDimensional.mem_of_tendsto hm_tendsto (Eventually.of_forall hm)659 have hM_top : M = ⊤ := absorbent_nhds_zero (𝕜 := 𝕜) hU_nhds |>.mono hU_sub_M |>.submodule_eq_top660 exact FiniteDimensional.of_surjective M.subtype fun x ↦ ⟨⟨x, by simp [hM_top]⟩, rfl⟩661662open scoped Pointwise in663/-- **Riesz's theorem**: if a T2 topological vector space over a complete non-trivial664normed field admits a totally bounded neighborhood of some point, then it is665finite-dimensional. -/666theorem FiniteDimensional.of_totallyBounded_nhds {x : Eᵤ} {U : Set Eᵤ} (hU_nhds : U ∈ 𝓝 x)667 (hU_tb : TotallyBounded U) : FiniteDimensional 𝕜 Eᵤ := by668 replace hU_nhds : x +ᵥ (-x) +ᵥ U ∈ 𝓝 x := by simpa669 rw [vadd_mem_nhds_self] at hU_nhds670 refine .of_totallyBounded_nhds_zero _ hU_nhds ?_671 have : -x +ᵥ U = (· - x) '' U := by simp [← Set.image_vadd, neg_add_eq_sub]672 exact this ▸ hU_tb.image (uniformContinuous_id.sub uniformContinuous_const)673674/-- **Riesz's theorem**: in a T2 topological vector space over a complete non-trivial normed field,675if there exists a totally bounded neighborhood of some point, then the space is finite-dimensional.676-/677theorem FiniteDimensional.of_exists_totallyBounded_nhds678 (h : ∃ x : Eᵤ, ∃ U ∈ 𝓝 x, TotallyBounded U) : FiniteDimensional 𝕜 Eᵤ := by679 rcases h with ⟨x, U, hU_nhds, hU_tb⟩680 exact FiniteDimensional.of_totallyBounded_nhds (𝕜 := 𝕜) hU_nhds hU_tb681682/-- **Riesz's theorem**: a locally compact topological vector space is finite-dimensional. -/683theorem FiniteDimensional.of_locallyCompactSpace [WeaklyLocallyCompactSpace E] :684 FiniteDimensional 𝕜 E :=685 let : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E686 have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup687 let ⟨_, hU_compact, hU_nhds⟩ := exists_compact_mem_nhds (0 : E)688 .of_totallyBounded_nhds_zero 𝕜 hU_nhds hU_compact.totallyBounded689690/-- If a function has compact support, then either the function is trivial691or the space is finite-dimensional. -/692theorem HasCompactSupport.eq_zero_or_finiteDimensional {X : Type*} [TopologicalSpace X] [Zero X]693 [T1Space X] {f : E → X} (hf : HasCompactSupport f) (h'f : Continuous f) :694 f = 0 ∨ FiniteDimensional 𝕜 E :=695 (HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup hf h'f).imp_right fun h ↦696 have : LocallyCompactSpace E := h; .of_locallyCompactSpace 𝕜697698/-- If a function has compact multiplicative support, then either the function is trivial699or the space is finite-dimensional. -/700theorem HasCompactMulSupport.eq_one_or_finiteDimensional {X : Type*} [TopologicalSpace X] [One X]701 [T1Space X] {f : E → X} (hf : HasCompactMulSupport f) (h'f : Continuous f) :702 f = 1 ∨ FiniteDimensional 𝕜 E :=703 have : T1Space (Additive X) := ‹_›704 HasCompactSupport.eq_zero_or_finiteDimensional 𝕜 (X := Additive X) hf h'f705706end Riesz707708section Compl709710open Submodule711712/-- If `p` is a closed subspace with finite codimension, then any algebraic complement `q` to `p`713is a topological complement. -/714theorem Submodule.IsCompl.isTopCompl_of_finiteDimensional_quotient {p q : Submodule 𝕜 E}715 (h : IsCompl p q) (hp : IsClosed (p : Set E)) [FiniteDimensional 𝕜 (E ⧸ p)] :716 IsTopCompl p q := by717 let φ : E ⧸ p →L[𝕜] q := (p.quotientEquivOfIsCompl q h).toLinearMap.toContinuousLinearMap718 have := (φ ∘L p.mkQL).isTopCompl_of_proj fun x ↦ by simp [φ]719 simpa [φ] using this.symm720721/-- Assume that `p q : Submodule 𝕜 E` are algebraic complements. If `p` is closed and `q`722has finite dimension, then they are in fact topological complements.723724Note that this theorem does not help you to build a closed complement to a finite dimensional725subspace. That requires the Hahn-Banach theorem, and you don't get much control over what the726complement is. See `Submodule.ClosedComplemented.of_finiteDimensional`. -/727theorem Submodule.IsCompl.isTopCompl_of_isClosed_of_finiteDimensional {p q : Submodule 𝕜 E}728 (h : IsCompl p q) (hp : IsClosed (p : Set E)) [hq : FiniteDimensional 𝕜 q] :729 IsTopCompl p q := by730 suffices FiniteDimensional 𝕜 (E ⧸ p) from h.isTopCompl_of_finiteDimensional_quotient hp731 exact (p.quotientEquivOfIsCompl q h).symm.finiteDimensional732733theorem Submodule.ClosedComplemented.of_finiteDimensional_quotient {p : Submodule 𝕜 E}734 (hp : IsClosed (p : Set E)) [hq : FiniteDimensional 𝕜 (E ⧸ p)] : p.ClosedComplemented := by735 obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl736 exact hq.isTopCompl_of_finiteDimensional_quotient hp |>.closedComplemented737738@[deprecated (since := "2026-05-09")]739alias Submodule.ClosedComplemented.of_quotient_finiteDimensional :=740 Submodule.ClosedComplemented.of_finiteDimensional_quotient741742lemma Submodule.ClosedComplemented.of_finiteDimensional_of_le743 {A B : Submodule 𝕜 E} [FiniteDimensional 𝕜 A] (hA : A.ClosedComplemented) [T2Space A]744 (hB : B ≤ A) : B.ClosedComplemented := by745 obtain ⟨p, hp⟩ := hA746 obtain ⟨C, hBC⟩ := B.exists_isCompl747 refine ⟨((projectionOnto B C hBC).domRestrict A).toContinuousLinearMap ∘SL p, fun x ↦ ?_⟩748 simp [hp ⟨x, hB x.2⟩]749750omit [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] in751theorem ContinuousLinearMap.ker_closedComplemented_of_finiteDimensional_range [T2Space F]752 (f : E →L[𝕜] F) [FiniteDimensional 𝕜 f.range] : f.ker.ClosedComplemented := by753 suffices FiniteDimensional 𝕜 (E ⧸ f.ker) from .of_finiteDimensional_quotient f.isClosed_ker754 exact f.toLinearMap.quotKerEquivRange.symm.finiteDimensional755756end Compl