Half-space PL charts on the weak realization of a solid simplex

The weak realization of the standard (n + 1)-simplex has a PL atlas with model the half-space in (Fin n → ℝ) × ℝ. Its vertex-chart domains are exactly the open stars. Dropping the last barycentric coordinate and reindexing the others identifies the realization with the coordinate simplex; the existing polyhedral half-space charts then flatten its corners. Proper-face support is equivalent to normal coordinate zero on each chart source. These give the solid standard simplex models for transporting PL charts along simplicial subdivisions.

The construction reuses realizationTopHomeomorphCoordinateSimplex, the ambient simplexBoundaryCoordinateMap, and coordinateSimplexHalfSpaceChart. Reference: C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 1–2 (simplices and polyhedral local models).

noncomputable def AbstractSimplicialComplex.simplexHalfSpacePLChart (n : ℕ) (v : Option (Option (Fin n))) : OpenPartialHomeomorph ⊤.Realization ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2}

The solid simplex vertex chart, expressed on the actual weak realization.

@[simp]

theorem AbstractSimplicialComplex.simplexHalfSpacePLChart_source (n : ℕ) (v : Option (Option (Fin n))) : (simplexHalfSpacePLChart n v).source = ⊤.openStarRealization (v.elim (Fin.last (n + 1)) fun (i : Option (Fin n)) => (finSuccEquivLast.symm i).castSucc)

Each chart has precisely the open star of its indexing vertex as source. none indexes the omitted vertex; some i indexes the retained vertex corresponding to i.

@[simp]

theorem AbstractSimplicialComplex.simplexHalfSpacePLChart_target (n : ℕ) (v : Option (Option (Fin n))) : (simplexHalfSpacePLChart n v).target = {q : ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2} | ∑ i : Option (Fin n), (TauCeti.coordinateSimplexHalfSpaceMap none).symm (↑q) i < 1}

All solid simplex vertex charts share the same open subset of the half-space model as target.

@[simp]

theorem AbstractSimplicialComplex.coe_simplexHalfSpacePLChart_apply (n : ℕ) (v : Option (Option (Fin n))) (x : ⊤.Realization) : ↑(↑(simplexHalfSpacePLChart n v) x) = (TauCeti.coordinateSimplexHalfSpaceMap v) ((simplexBoundaryCoordinateMap n) ⇑↑x)

The chart's ambient coordinates are given by the existing polyhedral flattening map.

theorem AbstractSimplicialComplex.coe_simplexHalfSpacePLChart_none_eq_zero (n : ℕ) (x : ⊤.Realization) (hx : ⇑↑x = Pi.single (Fin.last (n + 1)) 1) : ↑(↑(simplexHalfSpacePLChart n none) x) = 0

The chart at the omitted vertex sends that vertex to the origin.

theorem AbstractSimplicialComplex.coe_simplexHalfSpacePLChart_symm_apply (n : ℕ) (v : Option (Option (Fin n))) {q : ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2}} (hq : q ∈ (simplexHalfSpacePLChart n v).target) : ⇑↑(↑(simplexHalfSpacePLChart n v).symm q) = (simplexBoundaryCoordinateLift n) ((TauCeti.coordinateSimplexHalfSpaceMap v).symm ↑q)

On a chart target, the ambient inverse flattening and affine missing-mass lift recover every barycentric coordinate of the inverse chart.

theorem AbstractSimplicialComplex.support_ne_univ_iff_simplexHalfSpacePLChart_snd_eq_zero (n : ℕ) (v : Option (Option (Fin n))) (x : ⊤.Realization) (hx : x ∈ (simplexHalfSpacePLChart n v).source) : (↑x).support ≠ Finset.univ ↔ (↑(↑(simplexHalfSpacePLChart n v) x)).2 = 0

On a vertex chart's source, proper-face support is exactly normal coordinate zero.

theorem AbstractSimplicialComplex.isPiecewiseAffineOn_simplexHalfSpacePLChart_transition (n : ℕ) (v w : Option (Option (Fin n))) : have I := TauCeti.modelWithCornersHalfSpace (Fin n → ℝ); have e := (simplexHalfSpacePLChart n v).symm.trans (simplexHalfSpacePLChart n w); TauCeti.IsPiecewiseAffineOn (↑I ∘ ↑e ∘ ↑I.symm) (↑I.symm ⁻¹' e.source ∩ Set.range ↑I)

Coordinate changes have finite affine decompositions in the ambient half-space model.

@[instance_reducible]

noncomputable def AbstractSimplicialComplex.simplexHalfSpacePLChartedSpace (n : ℕ) : ChartedSpace ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2} ⊤.Realization

The finite vertex atlas on the solid simplex's weak realization.

@[simp]

theorem AbstractSimplicialComplex.simplexHalfSpacePLChartedSpace_atlas (n : ℕ) : atlas ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2} ⊤.Realization = Set.range (simplexHalfSpacePLChart n)

The atlas consists exactly of the prescribed half-space vertex charts.

theorem AbstractSimplicialComplex.realizationTopHalfSpace_hasGroupoid (n : ℕ) : HasGroupoid ⊤.Realization (TauCeti.PLGroupoid (TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)))

The weak realization of the solid standard (n + 1)-simplex is a PL manifold with boundary, with its barycentric open-star atlas. The case n = 0 is the segment.

theorem AbstractSimplicialComplex.isPLOn_comp_simplexHalfSpace_symm {ι : Type u_1} {n : ℕ} (v : Option (Option (Fin n))) {T : Set ↑{q : (Fin n → ℝ) × ℝ | 0 ≤ q.2}} {G : (Fin (n + 2) → ℝ) → ι → ℝ} (hG : TauCeti.IsPLOn G (Set.range fun (y : ⊤.Realization) => ⇑↑y)) (hT : T ⊆ (simplexHalfSpacePLChart n v).target) : TauCeti.IsPLOn (G ∘ ⇑(simplexBoundaryCoordinateLift n) ∘ ⇑(TauCeti.coordinateSimplexHalfSpaceMap v).symm) (↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)).symm ⁻¹' T ∩ Set.range ↑(TauCeti.modelWithCornersHalfSpace (Fin n → ℝ)))

The inverse of the simplex half-space chart, followed by the coordinate lift and a PL map G on the standard simplex, is PL on the model coordinates of any set T of targets of the chart at the vertex v.