Relabelling vertices does not change the realization up to homeomorphism

Proved

geometricRealization_homeomorph_of_vertexRelabelling

by Gabewhigham · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologymoment-angle-complexessimplicial-complexes

Let $L$ be a finite abstract simplicial complex on the vertex set $[m]$ and $L'$ one on $[m']$ , and let $e : [m] \to [m']$ be a bijection of vertex sets which is an isomorphism of complexes, in the sense that a finite set of vertices is a face of $L$ if and only if its image under $e$ is a face of $L'$ .

Then the barycentric-coordinate geometric realizations are homeomorphic:

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

The homeomorphism is the linear relabelling of coordinates: a point of $|L|$ is a vector of nonnegative barycentric coordinates summing to $1$ whose support is a face, and permuting the coordinates along $e$ preserves nonnegativity, the coordinate sum, and — by the isomorphism hypothesis — the condition that the support be a face. The inverse is the relabelling along $e^{-1}$ , and both maps are continuous because each coordinate of the image is a coordinate of the source.

Consequently every property of a complex defined through its realization is invariant under vertex relabelling; in particular, if $|L|$ is homeomorphic to $S^4$ then so is $|L'|$ , so being a simplicial four-sphere depends only on the isomorphism type of the complex, not on the chosen numbering of its vertices. This is what allows a construction carried out on a structured vertex set to be transported to the standard vertex set $[m]$ used in the statements of this mission.

Formalization Note The realization is the mission's barycentric-coordinate model, the isomorphism hypothesis is stated as an equivalence of face membership under the induced map on finite vertex sets, and the conclusion asserts that the type of homeomorphisms between the two realizations is nonempty.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem geometricRealization_homeomorph_of_vertexRelabelling {m m' : ℕ}
    (L : AbstractSimplicialComplex (Fin m)) (L' : AbstractSimplicialComplex (Fin m'))
    (e : Fin m ≃ Fin m')
    (h : ∀ σ : Finset (Fin m), σ ∈ L ↔ σ.map e.toEmbedding ∈ L') :
    Nonempty (GeometricRealization L ≃ₜ GeometricRealization L') := by sorry

Source

Standard invariance of the geometric realization under simplicial isomorphism: see e.g. J. R. Munkres, Elements of Algebraic Topology, Addison-Wesley 1984, Section 3 (an isomorphism of abstract simplicial complexes induces a homeomorphism of their geometric realizations, Theorem 3.1 and the discussion of geometric realizations of abstract complexes on pp. 15-16).

View graph