The product collar of a Euclidean half-space

This file identifies the standard (n + 1)-dimensional Euclidean half-space with the product of its n-dimensional boundary model and the one-dimensional Euclidean half-space. It is the model calculation behind collar charts: the last factor is the inward normal coordinate, and its zero slice is exactly the boundary parametrization from Boundary.Model.

The equivalence is constructed first in the ambient Euclidean spaces by splitting off the zeroth coordinate. Restricting it to the half-spaces gives, with Mathlib's product model-with-corners structure, a diffeomorphism. The characteristic lemmas record both coordinate projections and identify the zero slice, so later collar constructions do not need to unfold the coordinate implementation.

This is the standard-model prerequisite for the collar-neighbourhood target in Layer 1 of the GeometricTopology roadmap. The global collar theorem requires patching these local product coordinates on an arbitrary manifold and is not proved here.

Main definitions

• EuclideanHalfSpace.collarAmbientEquiv: the ambient linear equivalence ℝⁿ × ℝ¹ ≃ ℝⁿ⁺¹ putting the normal coordinate in coordinate zero.
• EuclideanHalfSpace.collarDiffeomorph: the same identification as a diffeomorphism of manifolds with corners.
• EuclideanHalfSpace.collarModelChartedSpace: the model half-space charted over the product, with that identification as its single chart.

Main results

• EuclideanHalfSpace.collarDiffeomorph_apply_zero_eq_boundaryParam: the zero-normal slice is the boundary parametrization.
• EuclideanHalfSpace.collarDiffeomorph_symm_apply_fst: the inverse recovers the boundary projection.
• EuclideanHalfSpace.collarDiffeomorph_apply_zero: the inward normal is coordinate zero.
• EuclideanHalfSpace.model_collarDiffeomorph: read in the models with corners, the collar diffeomorphism is collarAmbientEquiv.
• EuclideanHalfSpace.contMDiff_collarDiffeomorph_modelProd and EuclideanHalfSpace.contMDiff_collarDiffeomorph_symm_modelProd: its smoothness for the product model charted over itself, the chart structure used by charts of product manifolds.
• EuclideanHalfSpace.collarModelChartedSpace_chartAt and EuclideanHalfSpace.collarModelChartedSpace_atlas: its preferred chart and its atlas.
• EuclideanHalfSpace.exists_continuousLinearEquiv_image_range_prod: the product model ℝⁿ × [0, ∞) and the half-space model are linearly equivalent, with matching ranges.

Downstream target

The collar-neighbourhood theorem that these coordinates feed into is proved in M. Hirsch, Differential Topology, Springer GTM 33 (1976), Theorem 6.1, and J. Lee, Introduction to Smooth Manifolds, Springer GTM 218, 2nd ed. (2013), Theorem 9.25. That theorem is not proved here.

noncomputable def TauCeti.EuclideanHalfSpace.collarAmbientEquiv (n : ℕ) : (EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin 1)) ≃L[ℝ] EuclideanSpace ℝ (Fin (n + 1))

The ambient linear equivalence ℝⁿ × ℝ¹ ≃ ℝⁿ⁺¹ underlying the collar identification: the boundary coordinates go to the positive-index coordinates and the normal coordinate to coordinate zero.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_apply_zero (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (t : EuclideanSpace ℝ (Fin 1)) : ((collarAmbientEquiv n) (x, t)).ofLp 0 = t.ofLp 0

The ambient collar equivalence sends the normal coordinate to coordinate zero.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_apply_succ (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) (t : EuclideanSpace ℝ (Fin 1)) (i : Fin n) : ((collarAmbientEquiv n) (x, t)).ofLp i.succ = x.ofLp i

The ambient collar equivalence sends the boundary coordinates to the positive-index coordinates.

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_apply_zero_eq_boundaryParam (n : ℕ) (x : EuclideanSpace ℝ (Fin n)) : (collarAmbientEquiv n) (x, 0) = (euclideanHalfSpaceBoundaryParam n) x

At normal coordinate zero, the ambient collar equivalence is the boundary parametrization.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_symm_apply_fst (n : ℕ) (y : EuclideanSpace ℝ (Fin (n + 1))) : ((collarAmbientEquiv n).symm y).1 = (euclideanHalfSpaceBoundaryProj n) y

The boundary component of the inverse ambient collar equivalence is the boundary projection.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_symm_apply_snd_apply_zero (n : ℕ) (y : EuclideanSpace ℝ (Fin (n + 1))) : ((collarAmbientEquiv n).symm y).2.ofLp 0 = y.ofLp 0

The inverse ambient collar equivalence recovers coordinate zero as the normal coordinate.

theorem TauCeti.EuclideanHalfSpace.collarAmbientEquiv_symm_apply_snd_apply_zero_nonneg (n : ℕ) (y : EuclideanHalfSpace (n + 1)) : 0 ≤ ((collarAmbientEquiv n).symm ↑y).2.ofLp 0

On the half-space, the normal coordinate recovered by the inverse ambient collar equivalence is nonnegative.

noncomputable def TauCeti.EuclideanHalfSpace.collarDiffeomorph (n : ℕ) {k : WithTop ℕ∞} : Diffeomorph ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) (modelWithCornersEuclideanHalfSpace (n + 1)) (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) (EuclideanHalfSpace (n + 1)) k

The product collar identification is smooth in both directions for Mathlib's standard models with corners, at every finite or infinite regularity.

theorem TauCeti.EuclideanHalfSpace.coe_collarDiffeomorph_apply (n : ℕ) {k : WithTop ℕ∞} (p : EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) : ↑((collarDiffeomorph n) p) = (collarAmbientEquiv n) (p.1, ↑p.2)

Read in the ambient Euclidean spaces, the collar diffeomorphism is the linear equivalence collarAmbientEquiv.

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_symm_apply_coe (n : ℕ) {k : WithTop ℕ∞} (y : EuclideanHalfSpace (n + 1)) : (((collarDiffeomorph n).symm y).1, ↑((collarDiffeomorph n).symm y).2) = (collarAmbientEquiv n).symm ↑y

Read in the ambient Euclidean spaces, the inverse collar diffeomorphism is the inverse of the linear equivalence collarAmbientEquiv.

theorem TauCeti.EuclideanHalfSpace.contMDiff_collarDiffeomorph_modelProd (n : ℕ) {k : WithTop ℕ∞} : ContMDiff ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) (modelWithCornersEuclideanHalfSpace (n + 1)) k fun (p : ModelProd (EuclideanSpace ℝ (Fin n)) (EuclideanHalfSpace 1)) => (collarDiffeomorph n) p

The collar diffeomorphism is smooth from the product model ModelProd charted over itself, the chart structure of charts of manifolds modelled on (𝓡 n).prod (𝓡∂ 1).

theorem TauCeti.EuclideanHalfSpace.contMDiff_collarDiffeomorph_symm_modelProd (n : ℕ) {k : WithTop ℕ∞} : ContMDiff (modelWithCornersEuclideanHalfSpace (n + 1)) ((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) k fun (y : EuclideanHalfSpace (n + 1)) => (collarDiffeomorph n).symm y

The inverse collar diffeomorphism is smooth to the product model ModelProd charted over itself, the chart structure of charts of manifolds modelled on (𝓡 n).prod (𝓡∂ 1).

theorem TauCeti.EuclideanHalfSpace.model_collarDiffeomorph (n : ℕ) {k : WithTop ℕ∞} (p : EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) : ↑(modelWithCornersEuclideanHalfSpace (n + 1)) ((collarDiffeomorph n) p) = (collarAmbientEquiv n) (↑((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) p)

The collar diffeomorphism intertwines the models with corners: read through the model of the half-space and the product model of ℝⁿ × [0, ∞), it is the linear equivalence collarAmbientEquiv.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_apply_zero (n : ℕ) {k : WithTop ℕ∞} (p : EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) : (↑((collarDiffeomorph n) p)).ofLp 0 = (↑p.2).ofLp 0

The collar diffeomorphism sends the inward normal coordinate to coordinate zero.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_apply_succ (n : ℕ) {k : WithTop ℕ∞} (p : EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) (i : Fin n) : (↑((collarDiffeomorph n) p)).ofLp i.succ = p.1.ofLp i

The collar diffeomorphism sends the boundary coordinates to the positive-index coordinates.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_symm_apply_fst (n : ℕ) {k : WithTop ℕ∞} (y : EuclideanHalfSpace (n + 1)) : ((collarDiffeomorph n).symm y).1 = boundaryProj n y

The boundary component of the inverse collar diffeomorphism is the boundary projection.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_symm_apply_snd_apply_zero (n : ℕ) {k : WithTop ℕ∞} (y : EuclideanHalfSpace (n + 1)) : (↑((collarDiffeomorph n).symm y).2).ofLp 0 = (↑y).ofLp 0

The inverse collar diffeomorphism recovers the inward normal coordinate at zero.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarDiffeomorph_apply_zero_eq_boundaryParam (n : ℕ) {k : WithTop ℕ∞} (x : EuclideanSpace ℝ (Fin n)) : (collarDiffeomorph n) (x, 0) = boundaryParam n x

At normal coordinate zero, the collar diffeomorphism is the boundary parametrization.

@[instance_reducible]

noncomputable def TauCeti.EuclideanHalfSpace.collarModelChartedSpace (n : ℕ) : ChartedSpace (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) (EuclideanHalfSpace (n + 1))

The model half-space as a charted space over the product, with the collar identification as its single chart.

Deliberately not an instance: EuclideanHalfSpace (n + 1) already carries the charted space structure over itself, and a second one found by instance search would make every statement about its charts ambiguous. Use it explicitly with letI.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarModelChartedSpace_chartAt (n : ℕ) (y : EuclideanHalfSpace (n + 1)) : chartAt (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) y = (collarDiffeomorph n).symm.toHomeomorph.toOpenPartialHomeomorph

The preferred chart of collarModelChartedSpace at every point is the collar identification.

@[simp]

theorem TauCeti.EuclideanHalfSpace.collarModelChartedSpace_atlas (n : ℕ) : atlas (EuclideanSpace ℝ (Fin n) × EuclideanHalfSpace 1) (EuclideanHalfSpace (n + 1)) = {(collarDiffeomorph n).symm.toHomeomorph.toOpenPartialHomeomorph}

The atlas of collarModelChartedSpace is the collar identification alone.

theorem TauCeti.EuclideanHalfSpace.exists_continuousLinearEquiv_image_range_prod (n : ℕ) : ∃ (A : (EuclideanSpace ℝ (Fin n) × EuclideanSpace ℝ (Fin 1)) ≃L[ℝ] EuclideanSpace ℝ (Fin (n + 1))), ⇑A '' Set.range ↑((modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))).prod (modelWithCornersEuclideanHalfSpace 1)) = Set.range ↑(modelWithCornersEuclideanHalfSpace (n + 1))

The product model ℝⁿ × [0, ∞) is linearly the half-space model of dimension n + 1: a continuous linear equivalence of the ambient spaces carries the range of (𝓡 n).prod (𝓡∂ 1) onto the range {y | 0 ≤ y 0} of 𝓡∂ (n + 1).