Neat smooth embeddings of half-space charted spaces are locally flat

TauCeti.IsLocallyFlat.of_isSmoothEmbedding proves that a smooth embedding into a boundaryless manifold is locally flat. This file treats neat embeddings between charted spaces modelled on Euclidean half-spaces 𝓡∂ k and 𝓡∂ m, meeting the boundary of the ambient space exactly in their own boundary: f ⁻¹' ∂N = ∂M. The maximal-atlas charts in the immersion's normal form supply the smoothness needed here; global IsManifold instances are unnecessary. Such an embedding is locally flat with tangential model the half-space EuclideanHalfSpace k. Ambient charts take values in EuclideanHalfSpace k × F, with F the complement of the immersion, and carry the image of f exactly onto EuclideanHalfSpace k × {0}.

A properly embedded slice disc D² → D⁴ in manifolds with boundary is the motivating example. At a boundary point the standard picture of a neat submanifold is (ℝᵏ⁻¹ × [0, ∞)) × {0} ⊆ (ℝᵏ⁻¹ × [0, ∞)) × ℝᵐ⁻ᵏ.

The immersion normal form Manifold.IsImmersionAtOfComplement reads f in charts as u ↦ L (u, 0) for a linear equivalence L : E × F ≃L E'. When the ambient model has boundary, the ambient chart only covers a piece of the half-space range (𝓡∂ m), so L⁻¹ composed with it is not an open map into E × F. What is needed is a linear equivalence A : E' ≃L E × F that still reads f as u ↦ (u, 0) and carries the half-space range (𝓡∂ m) onto range (𝓡∂ k) × F, at least near the point considered. TauCeti.exists_isSliceChart_of_isImmersionAtOfComplement_of_straightening shows that such a straightening A gives a slice chart. It works for arbitrary models with corners.

For the half-space models a straightening always exists at a point of a neat embedding.

• At an interior point the image point is interior too, by neatness, and A = L⁻¹ works on a small open set where both half-space conditions hold strictly.
• At a boundary point, the boundary coordinate ν u = (L (u, 0)) 0 of the ambient chart pulled back along the immersion is nonnegative near the point and vanishes at it. A linear functional with this property on a neighbourhood in the half-space is a nonnegative multiple c • u 0 of the domain's boundary coordinate. Neatness at interior points forces c > 0. The shear (u, w) ↦ (u + c⁻¹ (L (0, w)) 0 • e₀, w) composed with L⁻¹ then rescales the ambient boundary coordinate to the domain's one and is a straightening.

Both cases use that interior and boundary points can be detected in the charts of the immersion, which only lie in the maximal atlas: this is TauCeti.ModelWithCorners.isInteriorPoint_euclideanHalfSpace_iff_of_mem_maximalAtlas. The multiple of the boundary coordinate is supplied by ContinuousLinearMap.exists_pos_eq_mul_apply_zero_of_eventually_pos.

Main results

• TauCeti.exists_isSliceChart_of_isImmersionAtOfComplement_of_straightening: a straightening of the ambient model gives a slice chart valued in H × F.
• TauCeti.exists_isSliceChart_of_isImmersionAtOfComplement_of_preimage_boundary: the slice chart of a neat embedding of half-space charted spaces at a point.
• TauCeti.IsLocallyFlat.of_isImmersionOfComplement_of_isEmbedding_of_preimage_boundary and TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary: a neat C^n embedding of half-space charted spaces, n ≠ 0, is locally flat with tangential model the half-space.
• TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary_of_sub_eq: a neat C^n embedding of half-space charted spaces of dimensions k and m is locally flat with complementary model EuclideanSpace ℝ (Fin (m - k)).

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Chapter 1, Section 4, for neat submanifolds of manifolds with boundary.
• R. Daverman and G. Venema, Embeddings in Manifolds, AMS Graduate Studies in Mathematics 106 (2009), Chapter 1, for local flatness of embeddings of manifolds with boundary.

theorem TauCeti.exists_isSliceChart_of_isImmersionAtOfComplement_of_straightening {𝕜 : 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} (hf : Topology.IsEmbedding f) {x : M} (h : Manifold.IsImmersionAtOfComplement F I J n f x) (A : E' ≃L[𝕜] E × F) (hAL : ∀ (u : E), A (h.equiv (u, 0)) = (u, 0)) {O : Set E'} (hO : IsOpen O) (hxO : ↑(h.codChart.extend J) (f x) ∈ O) (hA : ∀ v ∈ O, v ∈ Set.range ↑J ↔ (A v).1 ∈ Set.range ↑I) : ∃ (Φ : OpenPartialHomeomorph N (H × F)), f x ∈ Φ.source ∧ IsSliceChart Φ (Set.univ ×ˢ {0}) (Set.range f)

The slice chart of a straightened immersion. Let f be a topological embedding and a C^n immersion at x with complement F, written in charts as u ↦ L (u, 0). Suppose that the linear equivalence A : E' ≃L E × F reads L (u, 0) as (u, 0) and, on an open set O around the chart image of f x, carries the range of the ambient model onto range I × F. Then around f x there is an ambient chart valued in H × F carrying Set.range f exactly onto H × {0}.

This is the form of the slice-chart argument of TauCeti.exists_isSliceChart_of_isEmbedding_of_isImmersionAtOfComplement that allows the ambient manifold to have boundary or corners: the straightening replaces the boundarylessness of the ambient model.

theorem TauCeti.exists_isSliceChart_of_isImmersionAtOfComplement_of_preimage_boundary {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {k m : ℕ} [NeZero k] [NeZero m] {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace k) M] {N : Type u_3} [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace m) N] {n : WithTop ℕ∞} {f : M → N} (hn : n ≠ 0) (hf : Topology.IsEmbedding f) (hb : f ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M) {x : M} (h : Manifold.IsImmersionAtOfComplement F (modelWithCornersEuclideanHalfSpace k) (modelWithCornersEuclideanHalfSpace m) n f x) : ∃ (Φ : OpenPartialHomeomorph N (EuclideanHalfSpace k × F)), f x ∈ Φ.source ∧ IsSliceChart Φ (Set.univ ×ˢ {0}) (Set.range f)

The slice chart of a neat embedding. Let f be a topological embedding between charted spaces modelled on Euclidean half-spaces, which is a C^n immersion at x, n ≠ 0, with complement F and meets the boundary of N exactly in the boundary of M. Then around f x there is an ambient chart valued in EuclideanHalfSpace k × F carrying Set.range f exactly onto EuclideanHalfSpace k × {0}.

theorem TauCeti.IsLocallyFlat.of_isImmersionOfComplement_of_isEmbedding_of_preimage_boundary {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {k m : ℕ} [NeZero k] [NeZero m] {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace k) M] {N : Type u_3} [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace m) N] {n : WithTop ℕ∞} {f : M → N} (hn : n ≠ 0) (h : Manifold.IsImmersionOfComplement F (modelWithCornersEuclideanHalfSpace k) (modelWithCornersEuclideanHalfSpace m) n f) (hf : Topology.IsEmbedding f) (hb : f ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M) : IsLocallyFlat (EuclideanHalfSpace k) F f

A neat C^n immersion between half-space charted spaces is locally flat if it is a topological embedding and n ≠ 0. The tangential model is the half-space EuclideanHalfSpace k, so that boundary points of M are flattened onto the boundary of the slice, and the complementary model is the complement F of the immersion.

theorem TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary {k m : ℕ} [NeZero k] [NeZero m] {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace k) M] {N : Type u_3} [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace m) N] {n : WithTop ℕ∞} {f : M → N} (hn : n ≠ 0) (h : Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace k) (modelWithCornersEuclideanHalfSpace m) n f) (hb : f ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M) : IsLocallyFlat (EuclideanHalfSpace k) ⋯.complement f

A neat C^n embedding between half-space charted spaces is locally flat, n ≠ 0: if f meets the boundary of N exactly in the boundary of M, it is locally flat with tangential model the half-space EuclideanHalfSpace k and complementary model the complement chosen by the immersion.

theorem TauCeti.IsLocallyFlat.of_isSmoothEmbedding_of_preimage_boundary_of_sub_eq {k m : ℕ} [NeZero k] [NeZero m] {M : Type u_2} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace k) M] {N : Type u_3} [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace m) N] {n : WithTop ℕ∞} {f : M → N} (hn : n ≠ 0) (h : Manifold.IsSmoothEmbedding (modelWithCornersEuclideanHalfSpace k) (modelWithCornersEuclideanHalfSpace m) n f) (hb : f ⁻¹' ModelWithCorners.boundary N = ModelWithCorners.boundary M) {j : ℕ} (hj : m - k = j) : IsLocallyFlat (EuclideanHalfSpace k) (EuclideanSpace ℝ (Fin j)) f

A neat C^n embedding between half-space charted spaces is locally flat with Euclidean complement, n ≠ 0: if f meets the boundary of N exactly in the boundary of M and j = m - k, it is locally flat with tangential model the half-space EuclideanHalfSpace k and complementary model ℝʲ.