Relabelling vertices gives a based homeomorphism of moment-angle complexes

Proved

momentAngleComplex_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 suppose a bijection $e : [m] \to [m']$ is an isomorphism of complexes, meaning 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 associated moment-angle complexes are homeomorphic by a homeomorphism carrying the all-ones basepoint to the all-ones basepoint:

\mathcal Z_L \;\cong\; \mathcal Z_{L'}, \qquad (1,\dots,1) \mapsto (1,\dots,1).

The homeomorphism is the permutation of complex coordinates along $e$ . A point of $\mathcal Z_L$ is a vector $z \in \mathbb C^{[m]}$ for which there is a face (or the empty face) $\sigma$ with $|z_i| \le 1$ for $i \in \sigma$ and $|z_i| = 1$ otherwise; relabelling the coordinates replaces $\sigma$ by its image $e(\sigma)$ , which is a face of $L'$ exactly by the isomorphism hypothesis. The inverse relabelling is the corresponding map for $e^{-1}$ , and both are continuous coordinatewise. The all-ones point is fixed by any permutation of coordinates.

Because the homeomorphism is basepoint-preserving, it also identifies the based loop spaces $\Omega \mathcal Z_L \cong \Omega \mathcal Z_{L'}$ , and hence all the homological invariants used in this mission. The role of the statement is to let a construction performed on a structured vertex set be transported to the standard vertex set $[m]$ in which the mission's theorems are phrased.

Formalization Note The moment-angle complex is the mission's subspace of $(D^2)^m$ , the basepoint is the all-ones point, and the conclusion asserts the existence of a homeomorphism sending basepoint to basepoint.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem momentAngleComplex_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') :
    ∃ f : Complex L ≃ₜ Complex L', f (basepoint L) = basepoint L' := by sorry

Source

Immediate functoriality of the polyhedral product construction under isomorphisms of simplicial complexes; see V. M. Buchstaber and T. E. Panov, Toric Topology, Mathematical Surveys and Monographs 204, AMS 2015, Section 4.2 (definition of the polyhedral product and moment-angle complex Z_K, pp. 111-114), where the construction depends only on the isomorphism type of K.

View graph