A product half-space model #

The closed half-space in E × ℝ, with the last coordinate nonnegative, is a model with corners. Its inverse clips the last coordinate at zero. Keeping the tangential space explicit allows polyhedral boundary charts to use product coordinates directly.

Restricted to the points of positive height, the model is an open partial homeomorphism onto the open half-space in E × ℝ. Its inverse turns a chart with values of positive last coordinate into a half-space chart missing the boundary.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Chapter 1.

source

noncomputable def TauCeti.modelWithCornersHalfSpace (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] :

ModelWithCorners ℝ (E × ℝ) ↑{q : E × ℝ | 0 ≤ q.2}

The half-space model with tangential space E and nonnegative last coordinate.

Instances For

source

@[simp]

theorem TauCeti.modelWithCornersHalfSpace_apply (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (q : ↑{q : E × ℝ | 0 ≤ q.2}) :

↑(modelWithCornersHalfSpace E) q = ↑q

The half-space model embeds by the subtype inclusion.

source

theorem TauCeti.modelWithCornersHalfSpace_symm_apply (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] (q : E × ℝ) :

↑(modelWithCornersHalfSpace E).symm q = ⟨(q.1, max q.2 0), ⋯⟩

The inverse clips negative heights to zero.

source

theorem TauCeti.coe_modelWithCornersHalfSpace_symm_apply (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] {q : E × ℝ} (hq : 0 ≤ q.2) :

↑(↑(modelWithCornersHalfSpace E).symm q) = q

On the half-space, the model inverse leaves the ambient coordinates unchanged.

source

@[simp]

theorem TauCeti.range_modelWithCornersHalfSpace (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] :

Set.range ↑(modelWithCornersHalfSpace E) = {q : E × ℝ | 0 ≤ q.2}

The range of the model is the closed half-space.

source

noncomputable def TauCeti.halfSpaceInteriorChart (E : Type u_1) [NormedAddCommGroup E] [NormedSpace ℝ E] :

OpenPartialHomeomorph (↑{q : E × ℝ | 0 ≤ q.2}) (E × ℝ)

The model of the half-space, restricted to the points of positive height: an open partial homeomorphism onto the open half-space {q | 0 < q.2} in E × ℝ.

Instances For

source

@[simp]