Realizations of finite simplices

This file compares the closed coordinate simplex on any finite vertex set, including the empty set, with Mathlib's standard simplex on that set. It also identifies the geometric realization of the full abstract complex on a finite vertex type with Mathlib's standard simplex of barycentric coordinate functions. Specializing to two vertices gives a homeomorphism from the standard one-simplex to the unit interval. Its boundary, the bottom abstract complex on Fin 2, is then identified with the unit zero-sphere.

These are the first realization round-trips in layer 11 of the geometric-topology roadmap. The roadmap asks that the realization of the boundary of the standard n-simplex be homeomorphic to Sⁿ⁻¹; realizationOneSimplexBoundaryHomeomorphSphereZero establishes the base case n = 1. The interval identification also supplies the standard topological model for the simplicial interval used in the later product-and-collapse formulation of Zeeman's conjecture.

The barycentric simplex uses Mathlib's Convexity.StdSimplex, and its homeomorphism with the unit interval is Mathlib's Convexity.StdSimplex.homeomorphI. The zero-sphere identification is the elementary equivalence between its two points and Fin 2.

Main results

• Finset.standardSimplexHomeomorph: a closed coordinate simplex is homeomorphic to Mathlib's standard simplex on its finite vertex set.
• realizationTopHomeomorphStdSimplex: the full complex realizes to Mathlib's standard simplex.
• realizationOneSimplexHomeomorphUnitInterval: the standard one-simplex realizes to [0, 1].
• realizationOneSimplexBoundaryHomeomorphSphereZero: its boundary realizes to S⁰.

noncomputable def Finset.standardSimplexHomeomorph {α : Type u_1} (σ : Finset α) : AbstractSimplicialComplex.StandardSimplex σ ≃ₜ Convexity.StdSimplex ℝ ↥σ

A closed coordinate simplex is homeomorphic to Mathlib's standard simplex on its finite vertex set, including when that set is empty.

Equations

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

@[simp]

theorem Finset.standardSimplexHomeomorph_weights {α : Type u_1} (σ : Finset α) (x : AbstractSimplicialComplex.StandardSimplex σ) (a : ↥σ) : (σ.standardSimplexHomeomorph x).weights a = ↑x ↑a

The finite-simplex comparison reads the original coordinate at each vertex of the face.

@[simp]

theorem Finset.standardSimplexHomeomorph_symm_val {α : Type u_1} (σ : Finset α) (w : Convexity.StdSimplex ℝ ↥σ) : ↑(σ.standardSimplexHomeomorph.symm w) = Finsupp.mapDomain Subtype.val w.weights

The inverse finite-simplex comparison extends the finite coordinate vector by zero.

noncomputable def AbstractSimplicialComplex.realizationTopHomeomorphStdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] : ⊤.Realization ≃ₜ Convexity.StdSimplex ℝ ι

The realization of the full abstract complex on a finite vertex type is homeomorphic to Mathlib's standard simplex of nonnegative coordinate functions summing to one.

Equations

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

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphStdSimplex_apply {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : ⊤.Realization) (i : ι) : (realizationTopHomeomorphStdSimplex x).weights i = ↑x i

The full-complex realization homeomorphism reads the same barycentric coordinates.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphStdSimplex_symm_apply_val {ι : Type u_1} [Fintype ι] [Nonempty ι] (x : Convexity.StdSimplex ℝ ι) (i : ι) : ↑(realizationTopHomeomorphStdSimplex.symm x) i = x.weights i

The inverse full-complex realization homeomorphism has the prescribed barycentric coordinates.

noncomputable def AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval : ⊤.Realization ≃ₜ ↑unitInterval

The realization of the standard one-simplex is homeomorphic to the unit interval. The zeroth vertex maps to 0 and the first vertex maps to 1; see the two endpoint lemmas below.

Equations

• AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval = AbstractSimplicialComplex.realizationTopHomeomorphStdSimplex.trans Convexity.StdSimplex.homeomorphI

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval_coe (x : ⊤.Realization) : ↑(realizationOneSimplexHomeomorphUnitInterval x) = ↑x 1

The one-simplex homeomorphism is its second barycentric coordinate.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval_symm_apply_val_zero (x : ↑unitInterval) : ↑(realizationOneSimplexHomeomorphUnitInterval.symm x) 0 = 1 - ↑x

The zeroth barycentric coordinate of the interval inverse is one minus the interval coordinate.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval_symm_apply_val_one (x : ↑unitInterval) : ↑(realizationOneSimplexHomeomorphUnitInterval.symm x) 1 = ↑x

The first barycentric coordinate of the interval inverse is the interval coordinate.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval_vertex_zero : realizationOneSimplexHomeomorphUnitInterval (⊤.vertex 0) = 0

The zeroth vertex of the realized one-simplex is the left endpoint of the interval.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexHomeomorphUnitInterval_vertex_one : realizationOneSimplexHomeomorphUnitInterval (⊤.vertex 1) = 1

The first vertex of the realized one-simplex is the right endpoint of the interval.

noncomputable def AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero : ⊥.Realization ≃ₜ ↑(Metric.sphere 0 1)

The realization of the boundary of the standard one-simplex is homeomorphic to the unit zero-sphere. By simplexBoundary_univ_fin_two, the underlying precomplex of the source is exactly the boundary of the simplex on the two vertices.

Equations

• AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero = AbstractSimplicialComplex.realizationBotHomeomorph.trans AbstractSimplicialComplex.finTwoHomeomorphSphereZero✝

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero_vertex_zero : ↑(realizationOneSimplexBoundaryHomeomorphSphereZero (⊥.vertex 0)) = 1

The zeroth boundary vertex maps to 1 on the zero-sphere.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero_vertex_one : ↑(realizationOneSimplexBoundaryHomeomorphSphereZero (⊥.vertex 1)) = -1

The first boundary vertex maps to -1 on the zero-sphere.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero_symm_apply_one : realizationOneSimplexBoundaryHomeomorphSphereZero.symm ⟨1, realizationOneSimplexBoundaryHomeomorphSphereZero_symm_apply_one._proof_1⟩ = ⊥.vertex 0

The inverse zero-sphere homeomorphism sends 1 to the zeroth boundary vertex.

@[simp]

theorem AbstractSimplicialComplex.realizationOneSimplexBoundaryHomeomorphSphereZero_symm_apply_neg_one : realizationOneSimplexBoundaryHomeomorphSphereZero.symm ⟨-1, realizationOneSimplexBoundaryHomeomorphSphereZero_symm_apply_neg_one._proof_1⟩ = ⊥.vertex 1

The inverse zero-sphere homeomorphism sends -1 to the first boundary vertex.