Stellar subdivision at a face preserves the realization up to homeomorphism

Proved

geometricRealization_homeomorph_of_stellarSubdivision

by Gabewhigham · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologymoment-angle-complexespl-topologysimplicial-complexes

Let $L$ be a finite abstract simplicial complex on the vertex set $[m]$ and let $\tau$ be a face of $L$ . The stellar subdivision of $L$ at $\tau$ is the complex on the vertex set $[m]$ together with one new vertex $v$ , playing the role of the barycentre of $\tau$ , whose faces are

\{\, \sigma \in L : \tau \not\subseteq \sigma \,\} \;\cup\; \{\, \{v\} \cup \gamma \;:\; \tau \not\subseteq \gamma,\ \gamma \cup \tau \in L \,\},

that is, one deletes the closed star of $\tau$ and cones the remainder off from $v$ . In the statement this description is imposed as a hypothesis, phrased for the two possible shapes of a set of vertices — one avoiding $v$ , one containing $v$ — so that no new definition is required.

The assertion is that subdividing does not change the underlying space:

|L'| \;\cong\; |L| .

The homeomorphism is the affine map fixing the old vertices and sending the new vertex to the barycentre of $\tau$ ; in barycentric coordinates

\Phi(x)_i = x_i + \frac{x_v}{|\tau|}\,[\, i \in \tau \,].

It preserves nonnegativity and the coordinate sum, and it carries the support condition defining $|L'|$ to the one defining $|L|$ . Its inverse subtracts from the coordinates indexed by $\tau$ their common minimum $c=\min_{i\in\tau} y_i$ and places $|\tau|\,c$ in the new coordinate. The two maps are mutually inverse because on $|L'|$ some coordinate indexed by $\tau$ always vanishes: no face of $L'$ contains all of $\tau$ , whether or not it contains $v$ . Both realizations are compact Hausdorff, so a continuous bijection between them is a homeomorphism.

The hypothesis on $L'$ is satisfiable precisely when $\tau$ is a face of $L$ with at least two vertices, and it already forces $\tau$ to be a nonempty face of $L$ , so these conditions are not assumed separately.

Stellar subdivision is the standard device for removing an unwanted face of a triangulation while leaving a prescribed subcomplex untouched, and this invariance is what keeps the ambient space unchanged during such a process.

Formalization Note The realization is the mission's barycentric-coordinate model; the new vertex is the last element of $[m+1]$ and the old vertices form its initial segment.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem geometricRealization_homeomorph_of_stellarSubdivision {m : ℕ}
    (L : AbstractSimplicialComplex (Fin m))
    (L' : AbstractSimplicialComplex (Fin (m + 1))) (τ : Finset (Fin m))
    (hyp : ∀ γ : Finset (Fin m),
      ((γ.map Fin.castSuccEmb ∈ L') ↔ (γ ∈ L ∧ ¬ τ ⊆ γ)) ∧
        ((insert (Fin.last m) (γ.map Fin.castSuccEmb) ∈ L') ↔ (¬ τ ⊆ γ ∧ γ ∪ τ ∈ L))) :
    Nonempty (GeometricRealization L' ≃ₜ GeometricRealization L) := by sorry

Source

Standard invariance of the underlying polyhedron under stellar subdivision: C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer 1972, Chapter 2 (subdivisions, pp. 14-20: a subdivision of a complex has the same underlying polyhedron); L. C. Glaser, Geometrical Combinatorial Topology Volume I, Van Nostrand 1970, Chapter I (starring / stellar subdivision).

View graph