Half-space PL charts on a solid simplex

The solid coordinate simplex has a chart for each vertex, defined on the complement of the opposite facet. Affine vertex swaps carry these regions to the region of mass less than one. Orthant flattening then gives half-space coordinates, including at corners. Both directions have ambient piecewise-affine extensions, so the vertex charts define a PL manifold with boundary. These are the standard ball models used to transport charts to combinatorially triangulated manifolds.

The normal coordinate vanishes exactly on the geometric boundary in each chart. The construction includes the segment, with no tangential coordinates.

Reference: C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 1–2 (polyhedral local models). The construction uses coordinateSimplexVertexSwap and orthantFlattening.

noncomputable def TauCeti.coordinateSimplexHalfSpaceMap {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : (Option ι → ℝ) ≃ₜ (ι → ℝ) × ℝ

The ambient PL coordinates at a vertex of a solid simplex: swap that vertex with the origin, split off a distinguished coordinate, and flatten the solid orthant.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceMap_none {ι : Type u_1} [Fintype ι] (x : Option ι → ℝ) : (coordinateSimplexHalfSpaceMap none) x = orthantFlattening (fun (i : ι) => x (some i), x none)

In the origin chart, split the coordinates and flatten the orthant.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceMap_some {ι : Type u_1} [Fintype ι] (j : Option ι) (x : Option ι → ℝ) : (coordinateSimplexHalfSpaceMap (some j)) x = (coordinateSimplexHalfSpaceMap none) ((coordinateSimplexVertexSwap j) x)

The remaining vertex maps first exchange their vertex with the origin.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceMap_symm_none {ι : Type u_1} [Fintype ι] (q : (ι → ℝ) × ℝ) : (coordinateSimplexHalfSpaceMap none).symm q = Option.elim' (orthantFlattening.symm q).2 (orthantFlattening.symm q).1

The inverse origin coordinates undo orthant flattening and reassemble the coordinates.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceMap_symm_some {ι : Type u_1} [Fintype ι] (j : Option ι) (q : (ι → ℝ) × ℝ) : (coordinateSimplexHalfSpaceMap (some j)).symm q = (coordinateSimplexVertexSwap j) ((coordinateSimplexHalfSpaceMap none).symm q)

The other inverse coordinate maps exchange the origin with their indexing vertex.

theorem TauCeti.isPiecewiseAffineOn_coordinateSimplexHalfSpaceMap {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : IsPiecewiseAffineOn (⇑(coordinateSimplexHalfSpaceMap v)) Set.univ

The simplex half-space coordinate map has a finite affine decomposition globally.

theorem TauCeti.isPiecewiseAffineOn_coordinateSimplexHalfSpaceMap_symm {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : IsPiecewiseAffineOn (⇑(coordinateSimplexHalfSpaceMap v).symm) Set.univ

The inverse coordinate map also has a finite affine decomposition globally.

def TauCeti.coordinateSimplexHalfSpaceChartSource {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : Set ↑(coordinateSimplex (Option ι))

The vertex-chart source is the simplex with the opposite facet deleted.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceChartSource_none {ι : Type u_1} [Fintype ι] : coordinateSimplexHalfSpaceChartSource none = {x : ↑(coordinateSimplex (Option ι)) | ∑ i : Option ι, ↑x i < 1}

The origin-vertex source excludes the total-mass-one facet.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceChartSource_some {ι : Type u_1} [Fintype ι] (j : Option ι) : coordinateSimplexHalfSpaceChartSource (some j) = {x : ↑(coordinateSimplex (Option ι)) | 0 < ↑x j}

A coordinate-vertex source excludes the facet on which its coordinate is zero.

noncomputable def TauCeti.coordinateSimplexHalfSpaceChart {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : OpenPartialHomeomorph ↑(coordinateSimplex (Option ι)) ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2}

The half-space chart at a simplex vertex. Its common target consists of the points whose inverse origin coordinates have total mass less than one.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceChart_source {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : (coordinateSimplexHalfSpaceChart v).source = coordinateSimplexHalfSpaceChartSource v

The chart has the specified vertex region as its source.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceChart_target {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) : (coordinateSimplexHalfSpaceChart v).target = {q : ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2} | ∑ i : Option ι, (coordinateSimplexHalfSpaceMap none).symm (↑q) i < 1}

All vertex charts share the same target: the half-space points whose inverse origin coordinates have total mass less than one.

@[simp]

theorem TauCeti.coe_coordinateSimplexHalfSpaceChart_apply {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) (x : ↑(coordinateSimplex (Option ι))) : ↑(↑(coordinateSimplexHalfSpaceChart v) x) = (coordinateSimplexHalfSpaceMap v) ↑x

The chart is the restriction of its ambient coordinate map.

theorem TauCeti.coe_coordinateSimplexHalfSpaceChart_symm_apply {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) {q : ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2}} (hq : q ∈ (coordinateSimplexHalfSpaceChart v).target) : ↑(↑(coordinateSimplexHalfSpaceChart v).symm q) = (coordinateSimplexHalfSpaceMap v).symm ↑q

On the target, the inverse chart agrees with its ambient PL inverse formula.

theorem TauCeti.exists_mem_coordinateSimplexHalfSpaceChartSource {ι : Type u_1} [Fintype ι] (x : ↑(coordinateSimplex (Option ι))) : ∃ (v : Option (Option ι)), x ∈ coordinateSimplexHalfSpaceChartSource v

The complements of the opposite facets cover the solid simplex.

theorem TauCeti.mem_frontier_coordinateSimplex_iff_halfSpaceChart_snd_eq_zero {ι : Type u_1} [Fintype ι] (v : Option (Option ι)) (x : ↑(coordinateSimplex (Option ι))) (hx : x ∈ coordinateSimplexHalfSpaceChartSource v) : ↑x ∈ frontier (coordinateSimplex (Option ι)) ↔ (↑(↑(coordinateSimplexHalfSpaceChart v) x)).2 = 0

In a vertex chart the geometric simplex boundary is exactly height zero.

@[instance_reducible]

noncomputable def TauCeti.coordinateSimplexHalfSpaceChartedSpace {ι : Type u_1} [Fintype ι] : ChartedSpace ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2} ↑(coordinateSimplex (Option ι))

The simplex vertex charts, with a chart chosen from the cover at each point.

@[simp]

theorem TauCeti.coordinateSimplexHalfSpaceChartedSpace_atlas {ι : Type u_1} [Fintype ι] : atlas ↑{q : (ι → ℝ) × ℝ | 0 ≤ q.2} ↑(coordinateSimplex (Option ι)) = Set.range coordinateSimplexHalfSpaceChart

The atlas consists exactly of the vertex charts.

theorem TauCeti.isPiecewiseAffineOn_coordinateSimplexHalfSpaceChart_transition {ι : Type u_1} [Fintype ι] (v w : Option (Option ι)) : have I := modelWithCornersHalfSpace (ι → ℝ); have e := (coordinateSimplexHalfSpaceChart v).symm.trans (coordinateSimplexHalfSpaceChart w); IsPiecewiseAffineOn (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source ∩ Set.range ↑I)

Coordinate changes are piecewise affine when read in the product half-space model.

theorem TauCeti.coordinateSimplexHalfSpace_hasGroupoid {ι : Type u_1} [Fintype ι] : HasGroupoid (↑(coordinateSimplex (Option ι))) (PLGroupoid (modelWithCornersHalfSpace (ι → ℝ)))

The solid simplex's vertex charts define a PL manifold with boundary.