Smooth embeddings are locally flat

Local flatness (TauCeti.IsLocallyFlat) was isolated because topological embeddings can be wild: the Alexander horned sphere is a topologically embedded 2-sphere that no ambient chart flattens. Smooth embeddings are never wild, and this file proves it: a C^n embedding of manifolds into a boundaryless ambient manifold is locally flat, the complementary model space of the local flatness being the complement supplied by the immersion.

The proof is the shrinking argument that the two hypotheses of Manifold.IsSmoothEmbedding are there for. Being an immersion is already a normal-form statement in Mathlib: f is an immersion at x when charts φ of the domain and ψ of the ambient space can be chosen around x and f x so that in those charts f reads as the standard inclusion u ↦ (u, 0), through a continuous linear equivalence (E × F) ≃L[𝕜] E' of the ambient model space. Transporting ψ along that equivalence gives an ambient chart valued in E × F carrying f '' φ.source into the standard slice, so half of a slice chart comes for free. The other half — that the chart sees nothing but the image on the slice — fails for that chart, and is what the shrinking supplies:

• the chart is cut down to the part of its source lying over the target of φ, which forces a point of the slice to be the image of a point of φ.source;
• the chart is cut down again to an open set meeting Set.range f only in f '' φ.source, which is where being a topological embedding enters, and without which a point of the slice could be the image of a far-away point of the domain. That is exactly what happens for the figure-eight immersion t ↦ (sin 2t, sin t) of the open interval (-π, π) into the plane: it is injective, the crossing point of the figure eight being attained only at t = 0, but the two ends t → ±π accumulate at that same crossing point, so no neighbourhood of it in the plane meets the image in a single arc, and no chart flattens the image there.

Only the ambient manifold has to be boundaryless, its charts being required to be homeomorphisms onto open sets of the model space E'. The domain need not be: with boundary or corners in the domain the same argument flattens the image onto Set.range I ×ˢ {0}, the standard slice cut down to the range of the domain's model with corners. That is a slice embedding in the sense of TauCeti.IsSliceEmbedding, and is local flatness exactly when the domain model is boundaryless. The relative statement is the general one proved here, and local flatness of a smooth embedding is read off it.

Main results

• TauCeti.exists_isSliceChart_of_isEmbedding_of_isImmersionAtOfComplement: the slice chart at a point, the shrinking argument itself and the engine of the file.
• TauCeti.IsSliceEmbedding.of_isImmersionOfComplement_of_isEmbedding: a C^n immersion that is a topological embedding flattens its image onto Set.range I ×ˢ {0}, for a boundaryless ambient manifold and an arbitrary domain model with corners.
• TauCeti.IsLocallyFlat.of_isImmersionOfComplement_of_isEmbedding and TauCeti.IsLocallyFlat.of_isSmoothEmbedding: between boundaryless manifolds, a C^n embedding is locally flat, the complementary model being the complement of the immersion.
• TauCeti.isLocallyClosed_range_of_isSmoothEmbedding: the image of a C^n embedding into a boundaryless manifold is locally closed.
• TauCeti.SmoothEmbedding.isLocallyFlat: the same for the bundled smooth embeddings that the roadmap's geometric knot presentations are built from.
• TauCeti.isOpenEmbedding_of_isImmersionOfComplement_of_isEmbedding and TauCeti.isLocallyFlat_subtypeVal: the codimension-zero end, where local flatness is openness of the embedding.

Implementation notes

The ambient chart produced here is an OpenPartialHomeomorph N (E × F) rather than a member of a prescribed atlas, which is all TauCeti.IsSliceChart asks for. It is built from the immersion's Manifold.IsImmersionAtOfComplement.codChart, which does lie in the maximal atlas, by postcomposing with the homeomorphism G ≃ₜ E' of a boundaryless model with corners and with the immersion's own linear equivalence (E × F) ≃L[𝕜] E', and then restricting to an open set. Both postcompositions are homeomorphisms, so the result is again a chart of the maximal topological atlas.

Boundarylessness of the ambient manifold is used only through ModelWithCorners.toHomeomorph. Without it, the ambient chart composed with the model is a PartialEquiv whose target is a piece of a half-space rather than an open set, and the statement to prove would be one about a manifold with boundary as ambient space, where flatness at a boundary point of the ambient space is a genuinely different condition.

The immersion hypothesis is taken in the form Manifold.IsImmersionOfComplement, which fixes the complement F globally, rather than Manifold.IsImmersion, which merely asserts one exists: TauCeti.IsLocallyFlat names its complementary model space, so it needs a complement that does not vary from point to point. The Manifold.IsSmoothEmbedding corollaries pass Manifold.IsImmersion.complement for it.

References

• R. Daverman and G. Venema, Embeddings in Manifolds, AMS Graduate Studies in Mathematics 106 (2009), Chapter 1, where smooth submanifolds are the motivating example of local flatness.
• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, for the local normal form of an immersion that Mathlib's Manifold.IsImmersionAt takes as its definition.

theorem TauCeti.exists_isSliceChart_of_isEmbedding_of_isImmersionAtOfComplement {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [J.Boundaryless] (hf : Topology.IsEmbedding f) {x : M} (h : Manifold.IsImmersionAtOfComplement F I J n f x) : ∃ (Φ : OpenPartialHomeomorph N (E × F)), f x ∈ Φ.source ∧ IsSliceChart Φ (Set.range ↑I ×ˢ {0}) (Set.range f)

The slice chart of a smooth embedding. If f is a topological embedding and a C^n immersion at x with complement F, then around f x there is a chart of the ambient manifold, valued in the split model space E × F, carrying Set.range f exactly onto the slice Set.range I ×ˢ {0}.

This is the content of the file; everything below is a specialisation of it. The immersion normal form provides a chart in which f '' h.domChart.source lies on the slice, and the two restrictions performed here cut that chart down until nothing else does: first to the part lying over the target of the domain chart, so that a point of the slice is the image of a point of h.domChart.source, and then to an open set meeting Set.range f only in f '' h.domChart.source, which exists because f is an embedding.

theorem TauCeti.IsSliceEmbedding.of_isImmersionOfComplement_of_isEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [J.Boundaryless] (h : Manifold.IsImmersionOfComplement F I J n f) (hf : Topology.IsEmbedding f) : IsSliceEmbedding (Set.range ↑I ×ˢ {0}) f

A C^n immersion with complement F that is a topological embedding flattens its image onto the slice Set.range I ×ˢ {0} of the split ambient model space E × F.

Only the ambient manifold is assumed boundaryless. The domain may have boundary or corners, and then its model cuts the slice down to Set.range I ×ˢ {0}, which is the honest local picture of, say, a closed half-plane embedded in ℝ³.

theorem TauCeti.IsLocallyFlat.of_isImmersionOfComplement_of_isEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [I.Boundaryless] [J.Boundaryless] (h : Manifold.IsImmersionOfComplement F I J n f) (hf : Topology.IsEmbedding f) : IsLocallyFlat E F f

A smooth embedding of boundaryless manifolds is locally flat, the complementary model space of the local flatness being the complement F of the immersion. In particular a smooth embedding is never wild: there is no smooth analogue of the Alexander horned sphere.

theorem TauCeti.IsSliceEmbedding.of_isSmoothEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [J.Boundaryless] (h : Manifold.IsSmoothEmbedding I J n f) : IsSliceEmbedding (Set.range ↑I ×ˢ {0}) f

A C^n embedding into a boundaryless manifold flattens its image onto Set.range I ×ˢ {0}, the complementary model space being the complement carried by the immersion.

theorem TauCeti.IsLocallyFlat.of_isSmoothEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [I.Boundaryless] [J.Boundaryless] (h : Manifold.IsSmoothEmbedding I J n f) : IsLocallyFlat E ⋯.complement f

A C^n embedding of boundaryless manifolds is locally flat. This is the form the geometric-topology roadmap asks for: the low-codimension subtleties of topological embeddings are confined to TauCeti.IsLocallyFlat, and everything smooth satisfies it. The complementary model space is the complement Manifold.IsImmersion.complement chosen by the immersion, playing the role of the normal directions.

theorem TauCeti.isLocallyClosed_range_of_isSmoothEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [J.Boundaryless] (h : Manifold.IsSmoothEmbedding I J n f) : IsLocallyClosed (Set.range f)

The image of a C^n embedding into a boundaryless manifold is locally closed: it is closed in some open neighbourhood of itself. This is inherited from the slice picture, the slice Set.range I ×ˢ {0} being closed whatever the domain model, and is one of the properties a wild embedding can fail.

theorem TauCeti.SmoothEmbedding.isLocallyFlat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} [I.Boundaryless] [J.Boundaryless] (e : SmoothEmbedding I J n M N) : IsLocallyFlat E ⋯.complement ⇑e

A bundled smooth embedding of boundaryless manifolds is locally flat. This is the shape layer 4 of the geometric-topology roadmap consumes: a geometric knot presentation is a smooth embedding of the circle into an ambient manifold, and this says it is in particular a locally flat topological embedding, so the topological statements about it are not vacuous.

theorem TauCeti.isOpenEmbedding_of_isImmersionOfComplement_of_isEmbedding {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_5} [TopologicalSpace H] {G : Type u_6} [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 E' G} {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} [I.Boundaryless] [J.Boundaryless] [Subsingleton F] (h : Manifold.IsImmersionOfComplement F I J n f) (hf : Topology.IsEmbedding f) : Topology.IsOpenEmbedding f

Codimension zero. A C^n immersion with trivial complement which is a topological embedding is an open embedding: with no normal directions left the slice is the whole model space, so the flattening charts see nothing but the image.

theorem TauCeti.isLocallyFlat_subtypeVal {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_5} [TopologicalSpace H] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) [I.Boundaryless] [IsManifold I n M] (s : TopologicalSpace.Opens M) : IsLocallyFlat E PUnit.{u_9 + 1} Subtype.val

The inclusion of an open subset of a boundaryless manifold is locally flat with trivial complementary model. This is the codimension-zero end of the predicate, and confirms against TauCeti.isLocallyFlat_iff_isOpenEmbedding that the general theorem above is stated with the conventions that make an open embedding flat rather than merely embedded.