The realization of a simplex boundary

This file proves that the geometric realization of the boundary of the standard (n + 1)-simplex is homeomorphic to the unit n-sphere. It completes the "realization round-trips" acceptance check in layer 11 of the geometric-topology roadmap.

The proof uses barycentric coordinates twice. First, they identify the weak realization of the abstract boundary with the frontier of the convex hull of an affine basis of EuclideanSpace ℝ (Fin (n + 1)). On each facet the inverse is the ordinary barycentric-coordinate map, and a finite closed-cover argument proves that these local inverses assemble continuously. Second, Mathlib's exists_homeomorph_image_interior_closure_frontier_eq_unitBall sends the frontier of this full-dimensional convex simplex to the unit sphere.

The simplex-boundary model follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

Main definitions

• AbstractSimplicialComplex.standardSuccSimplexBoundary: the boundary complex of the standard (n + 1)-simplex, with vertex type Fin (n + 2).
• AbstractSimplicialComplex.realizationStandardSuccSimplexBoundaryHomeomorphSphere: its realization is homeomorphic to the unit sphere in EuclideanSpace ℝ (Fin (n + 1)).

@[instance_reducible]

noncomputable def AbstractSimplicialComplex.finDecidableEq (n : ℕ) : DecidableEq (Fin n)

Decide equality on Fin n classically, at high priority, throughout this file. The realization of a complex is indexed by a DecidableEq instance on its vertex type, and the arguments below combine terms whose instances would otherwise be the syntactically different instDecidableEqFin; forcing a single classical instance keeps them definitionally equal.

Equations

• AbstractSimplicialComplex.finDecidableEq n = Classical.decEq (Fin n)

noncomputable def AbstractSimplicialComplex.realizationStandardSuccSimplexBoundaryHomeomorphSphere (n : ℕ) : (standardSuccSimplexBoundary n).Realization ≃ₜ ↑(Metric.sphere 0 1)

The realization of the boundary of the standard (n + 1)-simplex is homeomorphic to the unit n-sphere in EuclideanSpace ℝ (Fin (n + 1)).

Equations

• One or more equations did not get rendered due to their size.