Invariance of domain

Brouwer's invariance of domain: a continuous injective map from an open subset of ℝⁿ to ℝⁿ has open image. More generally, let M and N be topological manifolds without boundary, charted on finite-dimensional real normed spaces of the same dimension. Then a map f : M → N which is continuous and injective on an open set U maps U to an open set (IsOpen.image_of_continuousOn_of_injOn), and a continuous injection M → N is an open embedding (Continuous.isOpenEmbedding_of_injective).

Consequently, interiors of subsets are intrinsic: if A ⊆ M and B ⊆ N are homeomorphic, a point of A lies in the interior of A exactly when its image lies in the interior of B (Homeomorph.coe_apply_mem_interior_iff), and likewise for frontiers (Homeomorph.coe_apply_mem_frontier_iff). This identifies, for instance, the boundary surface of a handlebody embedded in a 3-manifold with the frontier of its image.

The proof is the one in Hatcher. Embed the target F in the sphere Sⁿ, its one-point compactification (onePointEquivSphereOfFinrankEq). For a closed ball D in the domain on which f is continuous and injective, with boundary sphere S, the complement of f(S) in Sⁿ is not connected by the Jordan–Brouwer separation theorem (TauCeti.not_isPreconnected_compl_range_sphere). It is the disjoint union of the complement of f(D), which is path connected because it is acyclic (TauCeti.isPathConnected_sphere_compl_range_closedBall), and of the image of the open ball, which is path connected as the image of a convex set. So these are its two path components, and the image of the open ball is open, as a path component of an open subset of a manifold.

Main results

• IsOpen.image_of_continuousOn_of_injOn: invariance of domain for manifolds without boundary modelled on finite-dimensional real normed spaces of the same dimension.
• Continuous.isOpenEmbedding_of_injective: a continuous injection between such manifolds is an open embedding, and IsOpen.isOpenEmbedding_domRestrict_of_continuousOn_of_injOn is its form for a map continuous and injective on an open set.
• Continuous.surjective_of_injective: a continuous injection of a compact manifold into a connected manifold of the same dimension is surjective.
• Homeomorph.coe_apply_mem_interior_iff and Homeomorph.coe_apply_mem_frontier_iff: a homeomorphism between subsets of such manifolds matches their interiors and their frontiers.
• Topology.IsOpenEmbedding.finrank_le_of_isEmbedding and Topology.IsOpenEmbedding.finrank_eq: invariance of dimension, a nonempty open subset of ℝᵐ embeds into ℝⁿ only if m ≤ n.

References

• A. Hatcher, Algebraic Topology, Section 2.B, Theorem 2B.3.
• L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912), 305–313.

theorem IsOpen.image_of_continuousOn_of_injOn {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {f : M → N} {U : Set M} (hU : IsOpen U) (hf : ContinuousOn f U) (hinj : Set.InjOn f U) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) : IsOpen (f '' U)

Invariance of domain. Let M and N be topological manifolds without boundary, charted on real normed spaces E and F with F finite dimensional and finrank ℝ E = finrank ℝ F. If f : M → N is continuous and injective on an open set U, then f '' U is open. For M and N normed spaces, this is Brouwer's theorem that a continuous injection from an open subset of ℝⁿ to ℝⁿ has open image. (If E is infinite dimensional then F is trivial, N is discrete and U is empty.)

theorem Continuous.isOpenEmbedding_of_injective {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {f : M → N} (hf : Continuous f) (hinj : Function.Injective f) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) : Topology.IsOpenEmbedding f

Invariance of domain, global form. A continuous injection between topological manifolds without boundary, charted on real normed spaces of the same finrank, the second finite dimensional, is an open embedding.

theorem IsOpen.isOpenEmbedding_domRestrict_of_continuousOn_of_injOn {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {f : M → N} {U : Set M} (hU : IsOpen U) (hf : ContinuousOn f U) (hinj : Set.InjOn f U) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) : Topology.IsOpenEmbedding (U.domRestrict f)

Invariance of domain, restricted to an open set. Let M and N be topological manifolds without boundary, charted on real normed spaces of the same finrank, the second finite dimensional. If f : M → N is continuous and injective on an open set U, then its restriction to U is an open embedding.

theorem Continuous.surjective_of_injective {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] [CompactSpace M] [Nonempty M] [T2Space N] [PreconnectedSpace N] {f : M → N} (hf : Continuous f) (hinj : Function.Injective f) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) : Function.Surjective f

A continuous injection of a compact manifold into a connected one is onto. Let M and N be topological manifolds without boundary, charted on real normed spaces of the same finrank, the second finite dimensional, with M compact and nonempty and N Hausdorff and connected. Then a continuous injection M → N is surjective: its image is open by invariance of domain, and closed as a compact subset of a Hausdorff space.

theorem Homeomorph.coe_apply_mem_interior_iff {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {A : Set M} {B : Set N} (e : ↑A ≃ₜ ↑B) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) (x : ↑A) : ↑(e x) ∈ interior B ↔ ↑x ∈ interior A

Invariance of interior points. Let A and B be homeomorphic subsets of topological manifolds without boundary, charted on finite-dimensional real normed spaces of the same dimension. Then a point of A lies in the interior of A exactly when its image lies in the interior of B.

theorem Homeomorph.coe_apply_mem_frontier_iff {E : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] [TopologicalSpace M] [ChartedSpace E M] [TopologicalSpace N] [ChartedSpace F N] {A : Set M} {B : Set N} (e : ↑A ≃ₜ ↑B) (hEF : Module.finrank ℝ E = Module.finrank ℝ F) (x : ↑A) : ↑(e x) ∈ frontier B ↔ ↑x ∈ frontier A

Invariance of the frontier. Let A and B be homeomorphic subsets of topological manifolds without boundary, charted on finite-dimensional real normed spaces of the same dimension. Then a point of A lies in the frontier of A exactly when its image lies in the frontier of B.

theorem Topology.IsOpenEmbedding.finrank_le_of_isEmbedding {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {X : Type u_5} [TopologicalSpace X] [Nonempty X] {g : X → F} (hg : IsOpenEmbedding g) {f : X → E} (hf : IsEmbedding f) : Module.finrank ℝ F ≤ Module.finrank ℝ E

Invariance of dimension. If a nonempty space has an open embedding into a real normed space F and an embedding into a finite-dimensional real normed space E, then finrank ℝ F ≤ finrank ℝ E. In particular a nonempty open subset of ℝᵐ is homeomorphic to no subset of ℝⁿ for n < m.

theorem Topology.IsOpenEmbedding.finrank_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {X : Type u_5} [TopologicalSpace X] [Nonempty X] {f : X → E} (hf : IsOpenEmbedding f) {g : X → F} (hg : IsOpenEmbedding g) : Module.finrank ℝ E = Module.finrank ℝ F

Invariance of dimension. A nonempty space with open embeddings into finite-dimensional real normed spaces E and F forces finrank ℝ E = finrank ℝ F.