Flattening the boundary of an orthant

The boundary of the nonnegative orthant in (ι → ℝ) × ℝ is PL homeomorphic to ι → ℝ. The forward map subtracts the last coordinate from every other coordinate. Its inverse adjoins a zero coordinate and subtracts the minimum of all the coordinates. The minimum includes the adjoined zero, so the construction also works when ι is empty.

This is the local polyhedral model at a vertex of a simplex boundary: below the opposite facet, the simplex boundary is a neighbourhood of the apex in the orthant boundary. Both coordinate maps have explicit affine formulas on polyhedral cells.

The finite-minimum decomposition reuses Finset.infCell and Finset.infAffine_eq_of_mem_infCell.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 1--2 (polyhedral local models and vertex stars).

@[simp]

theorem TauCeti.mem_frontier_nonnegOrthant_iff {ι : Type u_1} [Finite ι] (p : (ι → ℝ) × ℝ) : p ∈ frontier (Set.Ici 0) ↔ (∀ (i : ι), 0 ≤ p.1 i) ∧ 0 ≤ p.2 ∧ (p.2 = 0 ∨ ∃ (i : ι), p.1 i = 0)

A point of the orthant boundary has nonnegative coordinates, at least one of which is zero.

def TauCeti.orthantProjection {ι : Type u_1} : (ι → ℝ) × ℝ →L[ℝ] ι → ℝ

The linear flattening map subtracting the last coordinate from the others.

@[simp]

theorem TauCeti.orthantProjection_apply {ι : Type u_1} (p : (ι → ℝ) × ℝ) (i : ι) : orthantProjection p i = p.1 i - p.2

Each flat coordinate is the difference from the last orthant coordinate.

def TauCeti.orthantLift {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : (ι → ℝ) × ℝ

Lift flat coordinates to the boundary of the nonnegative orthant. Adjoin zero and subtract the minimum coordinate, making every coordinate nonnegative and one zero.

theorem TauCeti.orthantLift_def {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : orthantLift y = have m := Finset.univ.inf' ⋯ (Option.elim' 0 y); (fun (i : ι) => y i - m, -m)

The explicit inverse formula, using the minimum of zero and the given coordinates.

theorem TauCeti.orthantLift_of_nonneg {ι : Type u_1} [Fintype ι] {y : ι → ℝ} (hy : ∀ (i : ι), 0 ≤ y i) : orthantLift y = (y, 0)

Nonnegative flat coordinates lift to the face with last coordinate zero.

@[simp]

theorem TauCeti.orthantLift_zero {ι : Type u_1} [Fintype ι] : orthantLift 0 = 0

theorem TauCeti.isPiecewiseAffineOn_orthantLift {ι : Type u_1} [Fintype ι] : IsPiecewiseAffineOn orthantLift Set.univ

The lift is piecewise affine on the whole coordinate space, with one minimum cell for each coordinate, including the adjoined zero coordinate.

theorem TauCeti.orthantLift_mem_frontier {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : orthantLift y ∈ frontier (Set.Ici 0)

The lift lands on the actual topological boundary of the orthant.

@[simp]

theorem TauCeti.orthantProjection_orthantLift {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : orthantProjection (orthantLift y) = y

Projecting a lifted point recovers its flat coordinates.

@[simp]

theorem TauCeti.orthantLift_fst_sub_snd {ι : Type u_1} [Fintype ι] (y : ι → ℝ) (i : ι) : (orthantLift y).1 i - (orthantLift y).2 = y i

Subtracting the last lifted coordinate recovers each original coordinate.

theorem TauCeti.orthantLift_orthantProjection {ι : Type u_1} [Fintype ι] {p : (ι → ℝ) × ℝ} (hp : p ∈ frontier (Set.Ici 0)) : orthantLift (orthantProjection p) = p

Lifting the flat coordinates of an orthant boundary point recovers that point.

def TauCeti.orthantBoundaryHomeomorph {ι : Type u_1} [Fintype ι] : ↑(frontier (Set.Ici 0)) ≃ₜ (ι → ℝ)

A PL homeomorphism flattening the boundary of the nonnegative orthant. With ι = Fin n, this identifies an (n + 1)-orthant boundary with ℝⁿ, including n = 0.

@[simp]

theorem TauCeti.orthantBoundaryHomeomorph_apply {ι : Type u_1} [Fintype ι] (p : ↑(frontier (Set.Ici 0))) (i : ι) : orthantBoundaryHomeomorph p i = (↑p).1 i - (↑p).2

The homeomorphism reads the linear flattening coordinates.

@[simp]

theorem TauCeti.coe_orthantBoundaryHomeomorph_symm_apply {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : ↑(orthantBoundaryHomeomorph.symm y) = orthantLift y

The inverse homeomorphism is the minimum-subtraction lift.