Smooth local collars of a manifold with boundary

Boundary.Collar.Local shrinks collar coordinates around a boundary point to a product box and splits the source of the resulting chart as a product, IsProductCollarChart.homeomorphProdOpens, whose three factors — the source, its part of the boundary, and the normal interval — are read as open subspaces. That splitting is only a homeomorphism. This file constructs the corresponding smooth product decomposition for the canonical manifold structure on the boundary.

For a product collar chart φ, the diffeomorphism TauCeti.IsProductCollarChart.diffeomorphProd sends a point to its boundary retraction and normal coordinate. Its underlying equivalence is the one of TauCeti.IsProductCollarChart.homeomorphProdOpens, so no topological content is reproved here; what is new is that both directions are C^k. Its inverse combines a boundary point and a normal coordinate and reads the resulting pair back through φ.

This is the smooth local-product step in the collar-neighbourhood target of Layer 1 of the GeometricTopology roadmap. The global collar theorem still requires patching these local diffeomorphisms along the whole boundary.

Main definitions

• TauCeti.IsProductCollarChart.diffeomorphProd: the canonical smooth local collar.

Main results

• TauCeti.IsProductCollarChart.contMDiff_boundaryRetract: the boundary retraction of a product collar chart is C^k.
• TauCeti.IsProductCollarChart.map_diffeomorphProd_fst and TauCeti.IsProductCollarChart.coe_diffeomorphProd_snd: the forward coordinate formulas.
• TauCeti.IsProductCollarChart.map_diffeomorphProd_symm: the inverse coordinate formula.
• TauCeti.IsProductCollarChart.diffeomorphProd_apply_of_mem_boundary: the local collar fixes the boundary and gives it normal coordinate zero.
• TauCeti.IsProductCollarChart.coe_diffeomorphProd: the smooth local collar has the same underlying map as the topological one, so all of the latter's coordinate formulas transfer.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Theorem 6.1.
• J. Lee, Introduction to Smooth Manifolds, Springer GTM 218, 2nd ed. (2013), Theorem 9.25.

theorem TauCeti.IsProductCollarChart.contMDiff_boundaryRetract {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) : ContMDiff (modelWithCornersEuclideanHalfSpace (n + 1)) (modelWithCornersEuclideanHalfSpace (n + 1)) k fun (y : ↥h.sourceOpens) => ↑φ.symm ((↑φ ↑y).1, 0)

The boundary retraction of a product collar chart is C^k: it sets the normal coordinate to zero and reads the result back through the chart.

noncomputable def TauCeti.IsProductCollarChart.diffeomorphProd {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) : have x := ⋯; Diffeomorph (modelWithCornersEuclideanHalfSpace (n + 1)) ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) (↥h.sourceOpens) (↥h.sourceBoundaryOpens × ↥(EuclideanHalfSpace.normalIioOpens ε)) k

A product collar chart gives a C^k diffeomorphism from its open source to the product of its open boundary part and open normal interval. Its underlying equivalence is the one of the topological local collar IsProductCollarChart.homeomorphProdOpens.

Equations

• h.diffeomorphProd hk = { toEquiv := h.homeomorphProdOpens.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

theorem TauCeti.IsProductCollarChart.coe_diffeomorphProd {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) : ⇑(h.diffeomorphProd hk) = ⇑h.homeomorphProdOpens

The smooth local collar is the topological one. Its underlying map is that of IsProductCollarChart.homeomorphProdOpens, so every coordinate formula proved there transfers.

theorem TauCeti.IsProductCollarChart.coe_diffeomorphProd_fst {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (y : ↥h.sourceOpens) : ↑↑((h.diffeomorphProd hk) y).1 = ↑φ.symm ((↑φ ↑y).1, 0)

The boundary component of the smooth local collar is obtained by setting the normal coordinate to zero and reading back through the collar chart.

@[simp]

theorem TauCeti.IsProductCollarChart.coe_diffeomorphProd_snd {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (y : ↥h.sourceOpens) : ↑((h.diffeomorphProd hk) y).2 = (↑φ ↑y).2

The normal component of the smooth local collar is the normal component of the collar chart.

theorem TauCeti.IsProductCollarChart.coe_diffeomorphProd_symm {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (p : ↥h.sourceBoundaryOpens × ↥(EuclideanHalfSpace.normalIioOpens ε)) : have x := ⋯; ↑((Diffeomorph.symm (h.diffeomorphProd hk)) p) = ↑φ.symm ((↑φ ↑↑p.1).1, ↑p.2)

The inverse smooth local collar forms a collar-coordinate pair and reads it back through the chart.

@[simp]

theorem TauCeti.IsProductCollarChart.map_diffeomorphProd_fst {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (y : ↥h.sourceOpens) : ↑φ ↑↑((h.diffeomorphProd hk) y).1 = ((↑φ ↑y).1, 0)

In collar coordinates, the boundary retraction keeps the tangential coordinate and sets the normal coordinate to zero.

@[simp]

theorem TauCeti.IsProductCollarChart.map_diffeomorphProd_symm {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (p : ↥h.sourceBoundaryOpens × ↥(EuclideanHalfSpace.normalIioOpens ε)) : have x := ⋯; ↑φ ↑((Diffeomorph.symm (h.diffeomorphProd hk)) p) = ((↑φ ↑↑p.1).1, ↑p.2)

Applying the collar chart after the inverse smooth local collar recovers the supplied tangential and normal coordinates.

@[simp]

theorem TauCeti.IsProductCollarChart.diffeomorphProd_apply_of_mem_boundary {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] {φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)} {V : Set (EuclideanSpace ℝ (Fin n))} {ε : ℝ} [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (h : IsProductCollarChart k φ V ε) (hk : k ≠ 0) (y : ↥h.sourceOpens) (hy : ↑y ∈ ModelWithCorners.boundary M) : (h.diffeomorphProd hk) y = (⟨⟨↑y, hy⟩, ⋯⟩, ⟨0, ⋯⟩)

On the boundary, the smooth local collar is the identity in the boundary factor and has zero normal coordinate.