Local collars of a manifold with boundary

Boundary.Collar.Chart reads a manifold with boundary in tangential and inward-normal coordinates, and Boundary.Collar.Manifold proves those coordinates are a C^k atlas. What they do not provide is a collar: the target of a collar chart is an arbitrary open subset of the product model, so it does not exhibit any neighbourhood as a product. This file shrinks a collar chart around a boundary point until its target is a genuine product box V × [0, ε), and reads off the resulting local product structure.

The shrinking is the elementary half of the collar-neighbourhood theorem: the boxes V × [0, ε) are a neighbourhood basis of a point of the product model lying on the boundary factor, because the sets [0, ε) are a neighbourhood basis of the origin of the one-dimensional half-space model. The remaining, global half is to patch these boxes into a single neighbourhood of the whole boundary, which is what Hirsch's bump-function argument does and what this file does not do.

Main definitions

• TauCeti.EuclideanHalfSpace.interiorEmbedding: a homeomorphism of ℝⁿ⁺¹ onto the open half-space, through which charts of a boundaryless manifold become interior half-space charts.
• TauCeti.EuclideanHalfSpace.normalRay: the inward normal ray [0, ∞) → EuclideanHalfSpace 1, the parametrization by which the one-dimensional half-space model is a half-line.
• TauCeti.EuclideanHalfSpace.normalIio: the initial segment [0, ε) of the one-dimensional half-space model, cut out by the normal coordinate, and TauCeti.EuclideanHalfSpace.normalIioOpens: the same segment as an open subspace.
• TauCeti.IsProductCollarChart: a collar chart whose target is a product box V × [0, ε), is C^k in both directions, and cuts out the boundary as the zero slice of its normal coordinate.
• TauCeti.EuclideanHalfSpace.homeomorphNormalIio: that segment, read by its normal coordinate as the real interval [0, ε).
• TauCeti.IsProductCollarChart.homeomorphProd: the local collar itself, a homeomorphism of the source of a product collar chart onto (its part of) the boundary times [0, ε).
• TauCeti.IsProductCollarChart.sourceOpens and TauCeti.IsProductCollarChart.sourceBoundaryOpens: the source of a product collar chart and its boundary part, as open subspaces of the ambient manifold and of the canonical boundary manifold.
• TauCeti.IsProductCollarChart.homeomorphProdOpens: the local collar with all three of those factors read as open subspaces. This is the packaging the smooth local collar of Boundary.Collar.Diffeomorph is built on.

Main results

• TauCeti.EuclideanHalfSpace.exists_normalIio_subset: the segments [0, ε) are a neighbourhood basis of the origin of the one-dimensional half-space model.
• TauCeti.exists_isProductCollarChart_of_mem_boundary: every boundary point has a product collar chart. This is the shrinking step.
• TauCeti.IsProductCollarChart.image_source_inter_boundary: a product collar chart carries the boundary onto the zero slice V × {0} of its box.
• TauCeti.IsProductCollarChart.map_homeomorphProd_fst: the first component of the local collar is the boundary retraction, in coordinates the map setting the normal coordinate to zero.
• TauCeti.exists_homeomorph_prod_Ico_of_mem_boundary: a boundary point has a neighbourhood U homeomorphic to (U ∩ ∂M) × [0, ε), the local collar neighbourhood.

Implementation notes

The height ε of the box is kept as a parameter rather than normalised to 1. Rescaling the normal coordinate is a diffeomorphism of the model half-space, so nothing is lost, and carrying ε avoids inserting a rescaling into every chart produced here; the patching step chooses its own heights anyway.

TauCeti.IsProductCollarChart.homeomorphProd is only a homeomorphism, not a diffeomorphism: its target (U ∩ ∂M) × [0, ε) is a product of a piece of the boundary manifold of Boundary.Charts with an interval, and identifying that manifold structure with the one the chart transports is a separate step. What is smooth here is the chart itself, through IsProductCollarChart.contMDiffOn and IsProductCollarChart.contMDiffOn_symm. That identification is carried out downstream in Boundary.Collar.Diffeomorph, where TauCeti.IsProductCollarChart.diffeomorphProd upgrades homeomorphProdOpens to a C^k diffeomorphism.

References

• M. Hirsch, Differential Topology, Springer GTM 33 (1976), Theorem 6.1 (the collar neighbourhood theorem, whose local half is proved here).
• J. Lee, Introduction to Smooth Manifolds, Springer GTM 218, 2nd ed. (2013), Theorem 9.25.

def TauCeti.EuclideanHalfSpace.normalRay (r : ℝ) : EuclideanHalfSpace 1

The inward normal ray of the one-dimensional half-space model: the point of EuclideanHalfSpace 1 at normal distance r from the boundary, for r ≤ 0 the origin.

Truncating at 0 is what makes the ray a globally defined continuous map on ℝ; it is used only for 0 ≤ r, where normalRay_normalCoord inverts it.

@[simp]

theorem TauCeti.EuclideanHalfSpace.normalRay_coe_apply (r : ℝ) : (↑(normalRay r)).ofLp 0 = max r 0

The normal coordinate of a point of the normal ray.

@[simp]

theorem TauCeti.EuclideanHalfSpace.val_zero_apply : (↑0).ofLp 0 = 0

The origin of the one-dimensional half-space model has vanishing normal coordinate.

@[simp]

theorem TauCeti.EuclideanHalfSpace.normalRay_zero : normalRay 0 = 0

The normal ray starts at the origin.

@[simp]

theorem TauCeti.EuclideanHalfSpace.normalRay_normalCoord (t : EuclideanHalfSpace 1) : normalRay ((↑t).ofLp 0) = t

The normal ray parametrizes the one-dimensional half-space model by its normal coordinate.

theorem TauCeti.EuclideanHalfSpace.normalRay_eq_symm (r : ℝ) : normalRay r = ↑(modelWithCornersEuclideanHalfSpace 1).symm ((PiLp.equivOfUnique 2 ℝ fun (x : Fin 1) => ℝ).symm r)

The normal ray is the inverse of the model with corners of the half-line, applied to the reals viewed as ℝ¹.

theorem TauCeti.EuclideanHalfSpace.continuous_normalRay : Continuous normalRay

The normal ray is continuous.

@[simp]

theorem TauCeti.EuclideanHalfSpace.eq_zero_iff {t : EuclideanHalfSpace 1} : t = 0 ↔ (↑t).ofLp 0 = 0

A point of the one-dimensional half-space model vanishes exactly when its normal coordinate does.

def TauCeti.EuclideanHalfSpace.normalIio (ε : ℝ) : Set (EuclideanHalfSpace 1)

The initial segment [0, ε) of the one-dimensional half-space model: the points whose normal coordinate is smaller than ε. It is empty for ε ≤ 0, and is the model factor of the collar boxes below.

@[simp]

theorem TauCeti.EuclideanHalfSpace.mem_normalIio {ε : ℝ} {t : EuclideanHalfSpace 1} : t ∈ normalIio ε ↔ (↑t).ofLp 0 < ε

Membership in the initial segment is one inequality on the normal coordinate.

theorem TauCeti.EuclideanHalfSpace.isOpen_normalIio (ε : ℝ) : IsOpen (normalIio ε)

The initial segments are open, being sublevel sets of the continuous normal coordinate.

def TauCeti.EuclideanHalfSpace.normalIioOpens (ε : ℝ) : TopologicalSpace.Opens (EuclideanHalfSpace 1)

The initial segment [0, ε) of the one-dimensional half-space model as an open subspace. It is empty for ε ≤ 0.

@[simp]

theorem TauCeti.EuclideanHalfSpace.mem_normalIioOpens {ε : ℝ} {t : EuclideanHalfSpace 1} : t ∈ normalIioOpens ε ↔ (↑t).ofLp 0 < ε

Membership in the open initial segment is one inequality on the normal coordinate.

theorem TauCeti.EuclideanHalfSpace.zero_mem_normalIio {ε : ℝ} (hε : 0 < ε) : 0 ∈ normalIio ε

An initial segment of positive height contains the origin.

Not @[simp]: mem_normalIio and val_zero_apply already reduce this to 0 < ε.

theorem TauCeti.EuclideanHalfSpace.nonempty_normalIio {ε : ℝ} (hε : 0 < ε) : (normalIio ε).Nonempty

An initial segment of positive height is nonempty.

theorem TauCeti.EuclideanHalfSpace.exists_normalIio_subset {W : Set (EuclideanHalfSpace 1)} (hW : IsOpen W) (h0 : 0 ∈ W) : ∃ (ε : ℝ), 0 < ε ∧ normalIio ε ⊆ W

The segments [0, ε) are a neighbourhood basis of the origin of the one-dimensional half-space model. This is the only point-set input to the shrinking step: it is what turns an arbitrary neighbourhood of a boundary point into a product box.

def TauCeti.EuclideanHalfSpace.homeomorphNormalIio (ε : ℝ) : ↑(normalIio ε) ≃ₜ ↑(Set.Ico 0 ε)

The initial segment [0, ε) of the one-dimensional half-space model is the real interval [0, ε), by the normal coordinate. It is the identification through which a local collar reads as a product with a half-open interval.

@[simp]

theorem TauCeti.EuclideanHalfSpace.coe_homeomorphNormalIio {ε : ℝ} (t : ↑(normalIio ε)) : ↑((homeomorphNormalIio ε) t) = (↑↑t).ofLp 0

The interval identification is the normal coordinate.

noncomputable def TauCeti.EuclideanHalfSpace.interiorEmbedding (n : ℕ) (v : EuclideanSpace ℝ (Fin (n + 1))) : EuclideanHalfSpace (n + 1)

A homeomorphism of ℝⁿ⁺¹ onto the open half-space {x | 0 < x 0}, exponentiating the zeroth coordinate and keeping the others. Composing the charts of a boundaryless manifold with it gives charts in the half-space model whose points are all interior points.

@[simp]

theorem TauCeti.EuclideanHalfSpace.interiorEmbedding_coe_apply_zero (n : ℕ) (v : EuclideanSpace ℝ (Fin (n + 1))) : (↑(interiorEmbedding n v)).ofLp 0 = Real.exp (v.ofLp 0)

The zeroth coordinate of interiorEmbedding is the exponential of the zeroth coordinate.

@[simp]

theorem TauCeti.EuclideanHalfSpace.interiorEmbedding_coe_apply_succ (n : ℕ) (v : EuclideanSpace ℝ (Fin (n + 1))) (i : Fin n) : (↑(interiorEmbedding n v)).ofLp i.succ = v.ofLp i.succ

The other coordinates of interiorEmbedding are unchanged.

theorem TauCeti.EuclideanHalfSpace.isOpenEmbedding_interiorEmbedding (n : ℕ) : Topology.IsOpenEmbedding (interiorEmbedding n)

interiorEmbedding is an open embedding, with image the open half-space (TauCeti.EuclideanHalfSpace.range_interiorEmbedding).

theorem TauCeti.EuclideanHalfSpace.range_interiorEmbedding (n : ℕ) : Set.range (interiorEmbedding n) = {y : EuclideanHalfSpace (n + 1) | 0 < (↑y).ofLp 0}

The image of interiorEmbedding is the open half-space, the interior of the model.

structure TauCeti.IsProductCollarChart {n : ℕ} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] (k : WithTop ℕ∞) (φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)) (V : Set (EuclideanSpace ℝ (Fin n))) (ε : ℝ) : Prop

A product collar chart on a manifold with boundary: a C^k chart in tangential and inward-normal coordinates whose target is a box V × [0, ε), and in which the boundary is the zero slice of the normal coordinate.

Unlike TauCeti.collarChart, whose target is whatever open set the ambient chart happens to have, the target here is a product, so the source is a product neighbourhood: that is what makes such a chart a local collar, TauCeti.IsProductCollarChart.homeomorphProd.

The regularity k is an argument rather than a field of the chart, so that one chart can be a product collar chart at several regularities.

• height_pos : 0 < ε

  The collar has positive height.

• target_eq : φ.target = V ×ˢ EuclideanHalfSpace.normalIio ε

  The chart is onto the product box V × [0, ε).

• contMDiffOn : ContMDiffOn (modelWithCornersEuclideanHalfSpace (n + 1)) ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) k (↑φ) φ.source

  The chart is C^k.

• contMDiffOn_symm : ContMDiffOn ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) (modelWithCornersEuclideanHalfSpace (n + 1)) k (↑φ.symm) φ.target

  The inverse of the chart is C^k.

• mem_boundary_iff (y : M) : y ∈ φ.source → (y ∈ ModelWithCorners.boundary M ↔ (↑(↑φ y).2).ofLp 0 = 0)

  The boundary is the zero slice of the normal coordinate.

def TauCeti.IsProductCollarChart.sourceOpens {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 ε) : TopologicalSpace.Opens M

The source of a product collar chart, regarded as an open submanifold of the ambient manifold.

@[simp]

theorem TauCeti.IsProductCollarChart.mem_sourceOpens {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 ε) {x : M} : x ∈ h.sourceOpens ↔ x ∈ φ.source

Membership in the open source of a product collar chart is membership in the chart source.

def TauCeti.IsProductCollarChart.sourceBoundaryOpens {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 ε) : TopologicalSpace.Opens ↑(ModelWithCorners.boundary M)

The part of the boundary in the source of a product collar chart, regarded as an open submanifold of the canonical boundary manifold.

@[simp]

theorem TauCeti.IsProductCollarChart.mem_sourceBoundaryOpens {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 ε) {x : ↑(ModelWithCorners.boundary M)} : x ∈ h.sourceBoundaryOpens ↔ ↑x ∈ φ.source

A boundary point belongs to the boundary part of the chart source exactly when its ambient point belongs to the chart source.

theorem TauCeti.IsProductCollarChart.fst_mem_base {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 ε) {y : M} (hy : y ∈ φ.source) : (↑φ y).1 ∈ V

The tangential coordinate of a point in the source of a product collar chart lies in its base.

theorem TauCeti.IsProductCollarChart.mk_mem_target {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 ε) {y : M} (hy : y ∈ φ.source) {t : EuclideanHalfSpace 1} (ht : t ∈ EuclideanHalfSpace.normalIio ε) : ((↑φ y).1, t) ∈ φ.target

Replacing the normal coordinate of a point in a product collar chart by another coordinate in its normal interval stays in the chart target.

theorem TauCeti.IsProductCollarChart.fst_zero_mem_target {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 ε) {y : M} (hy : y ∈ φ.source) : ((↑φ y).1, 0) ∈ φ.target

Setting the normal coordinate of a point in a product collar chart to zero stays in the chart target.

theorem TauCeti.IsProductCollarChart.isOpen_base {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 ε) : IsOpen V

The base of a product collar chart is open: it is a factor of the open target.

theorem TauCeti.IsProductCollarChart.image_source_inter_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) : ↑φ '' (φ.source ∩ ModelWithCorners.boundary M) = V ×ˢ {0}

A product collar chart carries the boundary onto the zero slice of its box.

noncomputable def TauCeti.IsProductCollarChart.homeomorphBase {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 ε) : ↑(φ.source ∩ ModelWithCorners.boundary M) ≃ₜ ↑V

The boundary points of the source of a product collar chart, as a subtype, are homeomorphic to its base.

@[simp]

theorem TauCeti.IsProductCollarChart.coe_homeomorphBase {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 ε) (y : ↑(φ.source ∩ ModelWithCorners.boundary M)) : ↑(h.homeomorphBase y) = (↑φ ↑y).1

The identification of the boundary part with the base is the tangential coordinate.

Proved by rfl for want of a usable evaluation lemma for Homeomorph.Set.prod: the @[simps]-generated Homeomorph.Set.prod_apply is stated for the subtype {p // p.1 ∈ V ∧ p.2 ∈ {0}}, which does not unify with the ↥(V ×ˢ {0}) occurring here, so neither simp nor rw can fire it and the composite has to be evaluated definitionally.

noncomputable def TauCeti.IsProductCollarChart.homeomorphProd {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 ε) : ↑φ.source ≃ₜ ↑(φ.source ∩ ModelWithCorners.boundary M) × ↑(EuclideanHalfSpace.normalIio ε)

The local collar. A product collar chart splits its source as the product of its part of the boundary with the interval [0, ε).

noncomputable def TauCeti.IsProductCollarChart.homeomorphProdOpens {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 ε) : ↥h.sourceOpens ≃ₜ ↥h.sourceBoundaryOpens × ↥(EuclideanHalfSpace.normalIioOpens ε)

The local collar with its source, boundary part, and normal interval packaged as open subspaces. Its underlying map is homeomorphProd; only the subtype packaging changes.

theorem TauCeti.IsProductCollarChart.coe_homeomorphProdOpens_fst_eq_homeomorphProd_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↥h.sourceOpens) : ↑↑(h.homeomorphProdOpens y).1 = ↑(h.homeomorphProd ⟨↑y, ⋯⟩).1

The boundary component of the open-subspace local collar agrees with that of homeomorphProd.

theorem TauCeti.IsProductCollarChart.coe_homeomorphProdOpens_snd_eq_homeomorphProd_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↥h.sourceOpens) : ↑(h.homeomorphProdOpens y).2 = ↑(h.homeomorphProd ⟨↑y, ⋯⟩).2

The normal component of the open-subspace local collar agrees with that of homeomorphProd.

@[simp]

theorem TauCeti.IsProductCollarChart.coe_homeomorphProd_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↑φ.source) : ↑(h.homeomorphProd y).2 = (↑φ ↑y).2

The second component of the local collar is the normal coordinate.

Proved by rfl for the same reason as coe_homeomorphBase: Homeomorph.Set.prod_apply does not match the ↥(V ×ˢ EuclideanHalfSpace.normalIio ε) this composite passes through.

@[simp]

theorem TauCeti.IsProductCollarChart.map_homeomorphProd_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↑φ.source) : ↑φ ↑(h.homeomorphProd y).1 = ((↑φ ↑y).1, 0)

The first component of the local collar is the boundary retraction: in coordinates it sets the normal coordinate to zero. Together with coe_homeomorphProd_snd this pins the homeomorphism down: it is the chart, read in the box.

@[simp]

theorem TauCeti.IsProductCollarChart.coe_homeomorphProdOpens_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↥h.sourceOpens) : ↑(h.homeomorphProdOpens y).2 = (↑φ ↑y).2

The second component of the open-subspace local collar is the normal coordinate.

@[simp]

theorem TauCeti.IsProductCollarChart.map_homeomorphProdOpens_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))} {ε : ℝ} (h : IsProductCollarChart k φ V ε) (y : ↥h.sourceOpens) : ↑φ ↑↑(h.homeomorphProdOpens y).1 = ((↑φ ↑y).1, 0)

The first component of the open-subspace local collar is the boundary retraction in collar coordinates.

theorem TauCeti.exists_isProductCollarChart_of_mem_boundary {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (hk : k ≠ 0) {x : M} (hx : x ∈ ModelWithCorners.boundary M) : ∃ (φ : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1)) (V : Set (EuclideanSpace ℝ (Fin n))) (ε : ℝ), x ∈ φ.source ∧ IsProductCollarChart k φ V ε

Every boundary point has a product collar chart. Shrinking the collar chart of the preferred ambient chart until its target is a box V × [0, ε) is possible because the target is open and the boundary point is read in it as a point of the zero slice, where the boxes are a neighbourhood basis.

This is the local half of the collar neighbourhood theorem; the global statement patches these boxes along the whole boundary.

theorem TauCeti.exists_homeomorph_prod_Ico_of_mem_boundary {n : ℕ} {k : WithTop ℕ∞} {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace (n + 1)) M] [IsManifold (modelWithCornersEuclideanHalfSpace (n + 1)) k M] (hk : k ≠ 0) {x : M} (hx : x ∈ ModelWithCorners.boundary M) : ∃ (U : Set M) (ε : ℝ), IsOpen U ∧ x ∈ U ∧ 0 < ε ∧ Nonempty (↑U ≃ₜ ↑(U ∩ ModelWithCorners.boundary M) × ↑(Set.Ico 0 ε))

A local collar neighbourhood of a boundary point. Every boundary point of a C^k manifold with boundary, k ≠ 0, has an open neighbourhood U homeomorphic to the product of its part U ∩ ∂M of the boundary with a half-open interval [0, ε).

This is the local collar; the collar neighbourhood theorem is the statement that the U can be taken to be a single neighbourhood of the whole boundary, with U ∩ ∂M = ∂M.