Surjectivity of the barycentric-subdivision realization map

The canonical realization map sends a vertex of the barycentric subdivision to the barycenter of the face it represents. This file proves that the map is onto. The proof gives the classical inverse coordinates explicitly: order the nonzero barycentric coordinates of a point decreasingly, take the nested initial segments in that order, and express the point as a convex combination of their barycenters.

Ties in the ordering do not affect the resulting point: a prefix ending inside a block of equal coordinates has weight zero, while a prefix ending at the end of that block contains the same vertices in any tie order. Subdivision.Injective proves injectivity, and Subdivision.Homeomorph proves continuity of the inverse.

The construction follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2, "Derived Subdivisions".

Main result

• AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_surjective: every point in the realization of a complex is the image of a point in its barycentric subdivision.

@[reducible, inline]

abbrev AbstractSimplicialComplex.BarycentricSubdivision.VertexOrder {ι : Type u_1} {K : AbstractSimplicialComplex ι} (σ : TauCeti.SetLike.Face K) : Type u_1

A numbering of the vertices of a face.

Equations

• AbstractSimplicialComplex.BarycentricSubdivision.VertexOrder σ = (Fin (↑σ).card ≃ ↥↑σ)

noncomputable def AbstractSimplicialComplex.BarycentricSubdivision.orderedSubdivisionPoint {ι : Type u_1} {K : AbstractSimplicialComplex ι} (σ : TauCeti.SetLike.Face K) (e : VertexOrder σ) (c : ℕ → ℝ) (hc : ∀ {k : ℕ}, k < (↑σ).card → c (k + 1) ≤ c k) (hsum : ∑ k ∈ Finset.range (↑σ).card, c k = 1) (hcard : c (↑σ).card = 0) : (TauCeti.PreAbstractSimplicialComplex.barycentricSubdivision K.toPreAbstractSimplicialComplex).Realization

The point of the barycentric subdivision determined by a face, an ordering of its vertices, and a decreasing sequence of barycentric coordinates.

Equations

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

theorem AbstractSimplicialComplex.BarycentricSubdivision.barycentricSubdivisionRealizationMap_orderedSubdivisionPoint {ι : Type u_1} {K : AbstractSimplicialComplex ι} (σ : TauCeti.SetLike.Face K) (e : VertexOrder σ) (c : ℕ → ℝ) (hc : ∀ {k : ℕ}, k < (↑σ).card → c (k + 1) ≤ c k) (hsum : ∑ k ∈ Finset.range (↑σ).card, c k = 1) (hcard : c (↑σ).card = 0) (x : StandardSimplex ↑σ) (hcoord : ∀ (i : Fin (↑σ).card), c ↑i = ↑x ↑(e i)) : K.barycentricSubdivisionRealizationMap (orderedSubdivisionPoint σ e c ⋯ hsum hcard) = K.faceInclusion σ x

The shared ordered-coordinate construction maps back to the original simplex point.

theorem AbstractSimplicialComplex.BarycentricSubdivision.continuous_orderedSubdivisionPoint {ι : Type u_1} {K : AbstractSimplicialComplex ι} {α : Type u_2} [TopologicalSpace α] (σ : TauCeti.SetLike.Face K) (e : VertexOrder σ) (c : α → ℕ → ℝ) (hc : ∀ (a : α) {k : ℕ}, k < (↑σ).card → c a (k + 1) ≤ c a k) (hsum : ∀ (a : α), ∑ k ∈ Finset.range (↑σ).card, c a k = 1) (hcard : ∀ (a : α), c a (↑σ).card = 0) (hcontinuous : ∀ k ≤ (↑σ).card, Continuous fun (a : α) => c a k) : Continuous fun (a : α) => orderedSubdivisionPoint σ e (c a) ⋯ ⋯ ⋯

The shared ordered-coordinate construction is continuous when all its used coordinates are.

theorem AbstractSimplicialComplex.barycentricSubdivisionRealizationMap_surjective {ι : Type u_1} (K : AbstractSimplicialComplex ι) : Function.Surjective K.barycentricSubdivisionRealizationMap

The canonical map from the realization of the barycentric subdivision to the realization of the original complex is surjective.

The preimage is the standard barycentric decomposition: list the nonzero coordinates decreasingly as x₀ ≥ ⋯ ≥ xₘ₋₁ > 0, let σᵢ be the face on the first i + 1 vertices, and give its barycenter weight (i + 1) * (xᵢ - xᵢ₊₁), with xₘ = 0. These weights are nonnegative, sum to one, and their weighted barycenters telescope coordinatewise to the original point.