A simplex and its boundary as a ball and its sphere

The weak realization of the standard n-simplex is homeomorphic to the Euclidean closed n-ball. The same homeomorphism takes exactly the proper faces to the unit sphere, so it identifies the pair consisting of a simplex and its boundary with the ball and sphere pair. This supplies compatible geometric models for combinatorial balls and their boundaries. The same holds for the sup-norm closed ball used by Mathlib's classical CW complexes. Dimension zero is included: the simplex and ball are singletons and their boundaries empty. An injective vertex enumeration gives the same ball model for every closed face of a complex; its barycentric support detects the open ball and boundary sphere.

Dropping the last barycentric coordinate gives an explicit homeomorphism to the coordinate simplex. The omitted coordinate is one minus the sum of the others. The subsequent ball identification uses Mathlib's convex-body gauge rescaling through TauCeti.exists_homeomorph_coordinateSimplex. The first comparison reuses realizationTopHomeomorphStdSimplex and Mathlib's Convexity.StdSimplex.

simplexCoordinateReindex distinguishes the last retained coordinate, and simplexBoundaryCoordinateMap gives the shared ambient linear coordinates for the solid and boundary simplex comparisons.

Reference: C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2 (simplices and polyhedra).

def AbstractSimplicialComplex.simplexCoordinateReindex (n : ℕ) : (Fin (n + 1) → ℝ) ≃ₜ (Option (Fin n) → ℝ)

Reindex the retained simplex coordinates, distinguishing the last coordinate with none. This ambient homeomorphism is shared by the solid and boundary comparisons.

@[simp]

theorem AbstractSimplicialComplex.simplexCoordinateReindex_apply (n : ℕ) (x : Fin (n + 1) → ℝ) (i : Option (Fin n)) : (simplexCoordinateReindex n) x i = x (finSuccEquivLast.symm i)

The reindexing reads the corresponding retained barycentric coordinate.

theorem AbstractSimplicialComplex.simplexCoordinateReindex_mem_iff (n : ℕ) (x : Fin (n + 1) → ℝ) : (simplexCoordinateReindex n) x ∈ TauCeti.coordinateSimplex (Option (Fin n)) ↔ x ∈ TauCeti.coordinateSimplex (Fin (n + 1))

Reindexing preserves the coordinate simplex, so it restricts to both the solid simplex and its frontier.

def AbstractSimplicialComplex.simplexBoundaryCoordinateMap (n : ℕ) : (Fin (n + 2) → ℝ) →L[ℝ] Option (Fin n) → ℝ

The affine coordinates of a realized simplex boundary: discard the last coordinate, then apply simplexCoordinateReindex to distinguish the last retained coordinate using none.

@[simp]

theorem AbstractSimplicialComplex.simplexBoundaryCoordinateMap_apply (n : ℕ) (x : Fin (n + 2) → ℝ) (i : Option (Fin n)) : (simplexBoundaryCoordinateMap n) x i = x (finSuccEquivLast.symm i).castSucc

Each coordinate is the corresponding retained barycentric coordinate.

def AbstractSimplicialComplex.simplexBoundaryCoordinateLift (n : ℕ) : (Option (Fin n) → ℝ) →ᴬ[ℝ] Fin (n + 2) → ℝ

Restore the omitted barycentric coordinate as the missing mass, reversing simplexBoundaryCoordinateMap on the affine hyperplane of total mass one.

@[simp]

theorem AbstractSimplicialComplex.simplexBoundaryCoordinateLift_castSucc (n : ℕ) (y : Option (Fin n) → ℝ) (i : Fin (n + 1)) : (simplexBoundaryCoordinateLift n) y i.castSucc = y (finSuccEquivLast i)

The retained coordinates are restored in their original order.

@[simp]

theorem AbstractSimplicialComplex.simplexBoundaryCoordinateLift_last (n : ℕ) (y : Option (Fin n) → ℝ) : (simplexBoundaryCoordinateLift n) y (Fin.last (n + 1)) = 1 - ∑ i : Option (Fin n), y i

The last coordinate is the mass left after summing the retained coordinates.

@[simp]

theorem AbstractSimplicialComplex.simplexBoundaryCoordinateMap_simplexBoundaryCoordinateLift (n : ℕ) (y : Option (Fin n) → ℝ) : (simplexBoundaryCoordinateMap n) ((simplexBoundaryCoordinateLift n) y) = y

Discarding the restored missing-mass coordinate recovers the original coordinates.

@[simp]

theorem AbstractSimplicialComplex.simplexBoundaryCoordinateLift_simplexBoundaryCoordinateMap (n : ℕ) (x : Fin (n + 2) → ℝ) (hx : ∑ i : Fin (n + 2), x i = 1) : (simplexBoundaryCoordinateLift n) ((simplexBoundaryCoordinateMap n) x) = x

Restoring the missing mass recovers a barycentric vector of total mass one.

noncomputable def AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex (n : ℕ) : ⊤.Realization ≃ₜ ↑(TauCeti.coordinateSimplex (Fin n))

Dropping the last barycentric coordinate identifies the weak realization of a standard n-simplex with the full-dimensional coordinate simplex.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex_apply (n : ℕ) (x : ⊤.Realization) (i : Fin n) : ↑((realizationTopHomeomorphCoordinateSimplex n) x) i = ↑x i.castSucc

The coordinate-simplex comparison reads the first barycentric coordinates.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex_symm_last (n : ℕ) (y : ↑(TauCeti.coordinateSimplex (Fin n))) : ↑((realizationTopHomeomorphCoordinateSimplex n).symm y) (Fin.last n) = 1 - ∑ i : Fin n, ↑y i

The inverse comparison restores the last coordinate as the missing mass.

theorem AbstractSimplicialComplex.mem_openStarRealization_top_last_iff_sum_lt_one (n : ℕ) (x : ⊤.Realization) : x ∈ ⊤.openStarRealization (Fin.last n) ↔ ∑ i : Fin n, ↑((realizationTopHomeomorphCoordinateSimplex n) x) i < 1

In the standard n-simplex, the open star of the last vertex is described in the dropped barycentric coordinates by the strict sum inequality.

theorem AbstractSimplicialComplex.image_openStarRealization_top_last (n : ℕ) : ⇑(realizationTopHomeomorphCoordinateSimplex n) '' ⊤.openStarRealization (Fin.last n) = {y : ↑(TauCeti.coordinateSimplex (Fin n)) | ∑ i : Fin n, ↑y i < 1}

The coordinate homeomorphism maps the open star of the last vertex of the standard n-simplex onto the points of the coordinate simplex whose coordinate sum is less than one.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex_symm_castSucc (n : ℕ) (y : ↑(TauCeti.coordinateSimplex (Fin n))) (i : Fin n) : ↑((realizationTopHomeomorphCoordinateSimplex n).symm y) i.castSucc = ↑y i

The inverse comparison preserves the retained coordinates.

theorem AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex_exists_affine (n : ℕ) : ∃ (A : (Fin (n + 2) → ℝ) →L[ℝ] Fin (n + 1) → ℝ) (B : (Fin (n + 1) → ℝ) →ᴬ[ℝ] Fin (n + 2) → ℝ), (∀ (z : Fin (n + 2) → ℝ) (i : Fin (n + 1)), A z i = z i.castSucc) ∧ ∀ (y : ↑(TauCeti.coordinateSimplex (Fin (n + 1)))), B ↑y = ⇑↑((realizationTopHomeomorphCoordinateSimplex (n + 1)).symm y)

Dropping the last barycentric coordinate is linear, and its affine inverse restores the missing mass on the coordinate simplex.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphCoordinateSimplex_mem_frontier_iff (n : ℕ) (x : ⊤.Realization) : ↑((realizationTopHomeomorphCoordinateSimplex n) x) ∈ frontier (TauCeti.coordinateSimplex (Fin n)) ↔ (↑x).support ≠ Finset.univ

A simplex point maps to the geometric frontier exactly when its support is a proper face. This includes the empty boundary of the zero-simplex.

noncomputable def AbstractSimplicialComplex.realizationTopHomeomorphClosedBall (n : ℕ) : ⊤.Realization ≃ₜ ↑(Metric.closedBall 0 1)

The weak realization of the standard n-simplex is homeomorphic to the Euclidean unit closed n-ball. Its proper-face boundary is taken to the sphere.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphClosedBall_norm_eq_one_iff (n : ℕ) (x : ⊤.Realization) : ‖↑((realizationTopHomeomorphClosedBall n) x)‖ = 1 ↔ (↑x).support ≠ Finset.univ

Under the simplex-to-ball homeomorphism, exactly the proper faces land on the sphere.

noncomputable def AbstractSimplicialComplex.realizationTopHomeomorphPiClosedBall (n : ℕ) : ⊤.Realization ≃ₜ ↑(Metric.closedBall 0 1)

The weak realization of the standard n-simplex is homeomorphic to the closed unit ball of Fin n → ℝ with the sup norm, the domain of Mathlib's classical CW characteristic maps. Its proper-face boundary is taken to the sphere.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphPiClosedBall_norm_eq_one_iff (n : ℕ) (x : ⊤.Realization) : ‖↑((realizationTopHomeomorphPiClosedBall n) x)‖ = 1 ↔ (↑x).support ≠ Finset.univ

Under the simplex-to-sup-norm-ball homeomorphism, exactly the proper faces land on the sphere.

noncomputable def AbstractSimplicialComplex.simplexClosedBallHomeomorph {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ↑(Metric.closedBall 0 1) ≃ₜ { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }

The sup-norm closed unit ball parametrizes the closed simplex on an explicitly enumerated face. Its boundary corresponds to the proper faces.

theorem AbstractSimplicialComplex.simplexClosedBallHomeomorph_val {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (x : ↑(Metric.closedBall 0 1)) : ↑↑((K.simplexClosedBallHomeomorph f hf) x) = Finsupp.mapDomain ⇑f ↑((realizationTopHomeomorphPiClosedBall n).symm x)

Barycentric coordinates are obtained from the fixed standard ball model by pushing its coordinate vector along the vertex enumeration.

theorem AbstractSimplicialComplex.simplexClosedBallHomeomorph_support_ne_iff {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (x : ↑(Metric.closedBall 0 1)) : (↑↑((K.simplexClosedBallHomeomorph f hf) x)).support ≠ Finset.image (⇑f) Finset.univ ↔ ‖↑x‖ = 1

The boundary sphere corresponds exactly to barycentric support smaller than the face.

@[simp]

theorem AbstractSimplicialComplex.simplexClosedBallHomeomorph_support_eq_iff {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (x : ↑(Metric.closedBall 0 1)) : (↑↑((K.simplexClosedBallHomeomorph f hf) x)).support = Finset.image (⇑f) Finset.univ ↔ ‖↑x‖ < 1

The open ball corresponds exactly to the points with full barycentric support.

theorem AbstractSimplicialComplex.norm_simplexClosedBallHomeomorph_symm_lt_one_iff {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (y : { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }) : ‖↑((K.simplexClosedBallHomeomorph f hf).symm y)‖ < 1 ↔ (↑↑y).support = Finset.image (⇑f) Finset.univ

The inverse closed-simplex homeomorphism lands in the open ball exactly at the points with full barycentric support.

theorem AbstractSimplicialComplex.norm_simplexClosedBallHomeomorph_symm_eq_one_iff {ι : Type u_1} [DecidableEq ι] (K : AbstractSimplicialComplex ι) {n : ℕ} (f : Fin (n + 1) ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (y : { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }) : ‖↑((K.simplexClosedBallHomeomorph f hf).symm y)‖ = 1 ↔ (↑↑y).support ⊂ Finset.image (⇑f) Finset.univ

The inverse closed-simplex homeomorphism lands on the sphere exactly at the points of proper faces.

theorem PreAbstractSimplicialComplex.nonempty_homeomorph_simplex_closedBall {ι : Type u_1} {A : AbstractSimplicialComplex ι} {n : ℕ} {V : Finset ι} (hV : V.card = n + 1) (hA : simplex V ≤ A.toPreAbstractSimplicialComplex) : Nonempty ({ x : A.Realization // (↑x).support ∈ simplex V } ≃ₜ ↑(Metric.closedBall 0 1))

The polyhedron of a simplex with n + 1 vertices is homeomorphic to the Euclidean closed n-ball, inside any ambient realization containing it.