Flattening a solid orthant to a half-space

Subtracting the last coordinate gives tangential coordinates. The least of all original coordinates gives the normal coordinate. Together these define an ambient PL homeomorphism carrying the nonnegative orthant onto a closed half-space, with its frontier carried onto the boundary hyperplane. The inverse adds the normal coordinate to the boundary lift.

This gives boundary charts for polyhedral balls: near a vertex a simplex is an orthant, and flattening the solid orthant provides coordinates in a manifold with boundary. The construction includes the one-dimensional orthant, with no tangential coordinates.

The inverse reuses orthantLift and its finite affine decomposition. Reference: C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 1–2 (polyhedral local models).

def TauCeti.orthantFlattening {ι : Type u_1} [Fintype ι] : (ι → ℝ) × ℝ ≃ₜ (ι → ℝ) × ℝ

An ambient PL homeomorphism flattening the nonnegative orthant to a half-space. Its tangential coordinate is orthantProjection; its normal coordinate is the minimum of all orthant coordinates.

@[simp]

theorem TauCeti.orthantFlattening_apply {ι : Type u_1} [Fintype ι] (p : (ι → ℝ) × ℝ) : orthantFlattening p = (orthantProjection p, p.2 - (orthantLift (orthantProjection p)).2)

The flattening subtracts the boundary lift's last coordinate from the height.

@[simp]

theorem TauCeti.orthantFlattening_symm_apply {ι : Type u_1} [Fintype ι] (q : (ι → ℝ) × ℝ) : orthantFlattening.symm q = ((orthantLift q.1).1 + fun (x : ι) => q.2, (orthantLift q.1).2 + q.2)

The inverse adds the height to every coordinate of the orthant boundary lift.

theorem TauCeti.isPiecewiseAffineOn_orthantFlattening {ι : Type u_1} [Fintype ι] : IsPiecewiseAffineOn (⇑orthantFlattening) Set.univ

Flattening is piecewise affine on the whole ambient space.

theorem TauCeti.isPiecewiseAffineOn_orthantFlattening_symm {ι : Type u_1} [Fintype ι] : IsPiecewiseAffineOn (⇑orthantFlattening.symm) Set.univ

The inverse flattening is piecewise affine on the whole ambient space.

theorem TauCeti.orthantFlattening_snd_eq_inf' {ι : Type u_1} [Fintype ι] (p : (ι → ℝ) × ℝ) : (orthantFlattening p).2 = Finset.univ.inf' ⋯ (Option.elim' p.2 p.1)

The normal coordinate is the minimum of the original coordinates, including the last one.

theorem TauCeti.mem_nonnegOrthant_iff_nonneg_orthantFlattening_snd {ι : Type u_1} [Fintype ι] (p : (ι → ℝ) × ℝ) : p ∈ Set.Ici 0 ↔ 0 ≤ (orthantFlattening p).2

The orthant condition becomes nonnegativity of the normal coordinate.

theorem TauCeti.orthantFlattening_image_nonnegOrthant {ι : Type u_1} [Fintype ι] : ⇑orthantFlattening '' Set.Ici 0 = {q : (ι → ℝ) × ℝ | 0 ≤ q.2}

The ambient flattening takes the nonnegative orthant onto the closed half-space.

theorem TauCeti.mem_frontier_nonnegOrthant_iff_orthantFlattening_snd_eq_zero {ι : Type u_1} [Fintype ι] (p : (ι → ℝ) × ℝ) : p ∈ frontier (Set.Ici 0) ↔ (orthantFlattening p).2 = 0

The orthant frontier is exactly where the flattened normal coordinate vanishes.

def TauCeti.orthantHalfSpaceHomeomorph {ι : Type u_1} [Fintype ι] : ↑(Set.Ici 0) ≃ₜ ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2}

The solid nonnegative orthant is PL homeomorphic to a closed half-space. Both maps are restrictions of the ambient piecewise-affine flattening and its inverse.

@[simp]

theorem TauCeti.coe_orthantHalfSpaceHomeomorph_apply {ι : Type u_1} [Fintype ι] (p : ↑(Set.Ici 0)) : ↑(orthantHalfSpaceHomeomorph p) = orthantFlattening ↑p

The half-space homeomorphism uses the ambient flattening formula.

@[simp]

theorem TauCeti.coe_orthantHalfSpaceHomeomorph_symm_apply {ι : Type u_1} [Fintype ι] (q : ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2}) : ↑(orthantHalfSpaceHomeomorph.symm q) = orthantFlattening.symm ↑q

Its inverse uses the ambient inverse flattening formula.