A linear map which is locally an embedding is an embedding

Fix 𝕜 a NontriviallyNormedField, E, F two topological vector spaces over 𝕜, and f : E → F a 𝕜-linear map. We show that, if there is a neighborhood V of 0 : E such that the restriction V → F is an embedding, then f itself is an embedding.

Note that this result is false for topological groups, as shown by the following counterexamples:

• first, in the group setting, there are local embeddings (even local homeomorphisms) which are not globally injective; an example is the quotient map ℝ → 𝕋 := ℝ ⧸ ℤ;
• even if assume that f is globally injective, the theorem still fails. Consider for example f : ℝ → 𝕋 × 𝕋 given by x ↦ ([x], [α * x]), with α irrational. f is injective, and locally an embedding by the inverse function theorem, yet it is not globally an embedding: any neighborhood of f(0) = (0, 0) contains infinitely many points f(n), n ∈ ℤ, since α * n gets arbitrarily close to being an integer infinitely many times.

Main results

• ContinuousSMul.topology_eq_of_induced_eq: let t₁, t₂ be two vector space topologies on E, and assume that there is a t₁-neighborhood of 0 V in restriction to which the two topologies coincide. Then t₁ = t₂.
• LinearMap.isInducing_of_restrict_nhds_zero: consider a linear map f : E → F, and assume there is a neighborhood of 0 V in E such that V.domRestrict f : V → F satisfies Topology.IsInducing. Then f satisfies Topology.IsInducing.
• LinearMap.isEmbedding_of_restrict_nhds_zero: consider a linear map f : E → F, and assume there is a neighborhood of 0 V in E such that V.domRestrict f : V → F is a topological embedding. Then f is a topological embedding.

TODO

We will also need the fact that if the restriction V → F is a closed embedding, then f : E → F is a closed embedding. This will follow from the fact that a subgroup which is locally closed at 0 is in fact closed, which we don't have yet

Implementation details

The content of this file is essentially (variations of) N. Bourbaki, Théories Spectrales, Chapitre III, § 5, n° 1, lemme 1, except Bourbaki's proof is very specific to 𝕜 = ℝ or 𝕜 = ℂ, since it relies crucially on balanced sets being connected.

Nevertheless, we are able to adapt their proof to arbitrary nontrivially normed fields. The key argument, replacing the fact that a connected set cannot be covered nontrivially by disjoint open sets, is that a balanced set W cannot intersect nontrivially both c • V and Vᶜ, when V is a neighborhood of 0 and 0 < ‖c‖ < 1. We refer to the (highly commented!) proof for more details.

References

• N. Bourbaki, Théories Spectrales, Chapitre III, § 5, n° 1, lemme 1

theorem ContinuousSMul.topology_eq_of_nhds_inf_principal_eq (𝕜₁ : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜₁] [AddCommGroup E] [Module 𝕜₁ E] (t₁ t₂ : TopologicalSpace E) [IsTopologicalAddGroup E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₁ E] {V : Set E} (V_mem : V ∈ nhds 0) (H : nhds 0 ⊓ Filter.principal V = nhds 0 ⊓ Filter.principal V) : t₁ = t₂

Consider a vector space E over a NontriviallyNormedField 𝕜, and t₁, t₂ two vector space topologies on E.

Assume that there is a t₁-neighborhood of zero V such that the two topogies induce the same filter of neighborhoods of 0 in the subspace V. Then t₁ = t₂.

theorem ContinuousSMul.topology_eq_of_induced_eq (𝕜₁ : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜₁] [AddCommGroup E] [Module 𝕜₁ E] (t₁ t₂ : TopologicalSpace E) [IsTopologicalAddGroup E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₁ E] {V : Set E} (V_mem : V ∈ nhds 0) (H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂) : t₁ = t₂

Consider a vector space E over a NontriviallyNormedField 𝕜, and t₁, t₂ two topologies on E which are compatible with the vector space structure.

Assume that there is a t₁-neighborhood of zero V such that the two topogies induce the same topology on the subspace V. Then t₁ = t₂.

theorem LinearMap.isInducing_of_restrict_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] [AddCommGroup E] [AddCommGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} {f : E →ₛₗ[σ] F} [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup E] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] [RingHomIsometric σ] {V : Set E} (V_mem : V ∈ nhds 0) (H : Topology.IsInducing (V.domRestrict ⇑f)) : Topology.IsInducing ⇑f

theorem LinearMap.isEmbedding_of_restrict_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [NontriviallyNormedField 𝕜₁] [NontriviallyNormedField 𝕜₂] [AddCommGroup E] [AddCommGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} {f : E →ₛₗ[σ] F} [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup E] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] [RingHomIsometric σ] {V : Set E} (V_mem : V ∈ nhds 0) (H : Topology.IsEmbedding (V.domRestrict ⇑f)) : Topology.IsEmbedding ⇑f