Stellar equivalence of simplicial complexes

Starring a face at a fresh vertex (PreAbstractSimplicialComplex.stellarSubdivision) is one stellar move. Two complexes are stellar equivalent when a finite sequence of stellar moves and inverse stellar moves carries one to the other. This is the combinatorial relation that layer 11 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md) needs in order to say that a complex is a combinatorial ball or sphere, namely that it becomes the standard simplex, respectively the boundary of the standard simplex, after subdivision.

The relation is built as Relation.EqvGen of the one-move relation, so a proof of StellarEquivalent K L is generated by stellar moves under reflexivity, symmetry, and transitivity, and induction over that closure is how every invariance result below is proved.

What this relation is, and what it is not

Newman's and Alexander's theorem is that stellar equivalence coincides with the existence of a common subdivision, hence — once realizations are available — with PL homeomorphism. That theorem is not proved here, and nothing below asserts it: the definition is taken as the combinatorial one, following Lickorish, Simplicial moves on complexes and manifolds, Geom. Topol. Monogr. 2 (1999), 299-320, and Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. Naming the relation after the moves that generate it, rather than after that theorem, keeps the two apart.

A stellar move demands a fresh vertex, one spanning no face of the complex yet. That hypothesis is what makes the move honest. The same-type relation records literal move sequences, while StellarEquivalentUpToRelabeling compares complexes intrinsically: it first embeds both into a common enlarged vertex type and allows arbitrary injective relabelings.

Main definitions

• PreAbstractSimplicialComplex.IsStellarMove: one starring of a face at a fresh vertex.
• PreAbstractSimplicialComplex.StellarEquivalent: a finite chain of such moves.
• PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling: intrinsic stellar equivalence in a common enlarged vertex type.

Main results

• PreAbstractSimplicialComplex.equivalence_stellarEquivalent: stellar equivalence is an equivalence relation.
• PreAbstractSimplicialComplex.StellarEquivalent.dimension_eq: stellar equivalent complexes have the same dimension.
• PreAbstractSimplicialComplex.StellarEquivalent.finite_faces_iff: stellar equivalence preserves and reflects finiteness of the face collection.
• PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.induction_on: invariants of intrinsic stellar equivalence follow from the common-relabeling generators.
• PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.dimension_eq, finite_faces_iff, and ne_bot_iff: intrinsic stellar equivalence preserves dimension, face finiteness, and nonvoidness.

def PreAbstractSimplicialComplex.IsStellarMove {ι : Type u_1} [DecidableEq ι] (K L : PreAbstractSimplicialComplex ι) : Prop

L is obtained from K by one stellar move: L is the starring of K at a face σ using a vertex v that K does not already use.

Equations

• K.IsStellarMove L = ∃ (σ : Finset ι) (v : ι), σ ∈ K ∧ {v} ∉ K ∧ L = K.stellarSubdivision σ v

theorem PreAbstractSimplicialComplex.isStellarMove_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} : K.IsStellarMove L ↔ ∃ (σ : Finset ι) (v : ι), σ ∈ K ∧ {v} ∉ K ∧ L = K.stellarSubdivision σ v

The witness description of a stellar move.

theorem PreAbstractSimplicialComplex.isStellarMove_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : K.IsStellarMove (K.stellarSubdivision σ v)

Starring a face at a fresh vertex is a stellar move.

theorem PreAbstractSimplicialComplex.IsStellarMove.dimension_eq {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.IsStellarMove L) : L.dimension = K.dimension

A stellar move preserves the dimension.

theorem PreAbstractSimplicialComplex.IsStellarMove.finite_faces_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.IsStellarMove L) : K.faces.Finite ↔ L.faces.Finite

A stellar move preserves and reflects finiteness of the face collection.

def PreAbstractSimplicialComplex.StellarEquivalent {ι : Type u_1} [DecidableEq ι] (K L : PreAbstractSimplicialComplex ι) : Prop

Stellar equivalence: K and L are joined by a finite sequence of stellar moves and inverse stellar moves.

Equations

• K.StellarEquivalent L = Relation.EqvGen PreAbstractSimplicialComplex.IsStellarMove K L

theorem PreAbstractSimplicialComplex.StellarEquivalent.refl {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) : K.StellarEquivalent K

Every simplicial complex is stellar equivalent to itself.

theorem PreAbstractSimplicialComplex.StellarEquivalent.trans {ι : Type u_1} [DecidableEq ι] {K L M : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) (h' : L.StellarEquivalent M) : K.StellarEquivalent M

Stellar equivalences compose.

theorem PreAbstractSimplicialComplex.StellarEquivalent.symm {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) : L.StellarEquivalent K

Stellar equivalence is symmetric.

theorem PreAbstractSimplicialComplex.IsStellarMove.stellarEquivalent {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.IsStellarMove L) : K.StellarEquivalent L

A single stellar move is a stellar equivalence.

theorem PreAbstractSimplicialComplex.IsStellarMove.map {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (h : K.IsStellarMove L) (f : ι → κ) (hf : Function.Injective f) : (K.map f).IsStellarMove (L.map f)

An injective relabeling carries a stellar move to the corresponding stellar move between the image complexes.

theorem PreAbstractSimplicialComplex.stellarEquivalent_stellarSubdivision {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : {v} ∉ K) : K.StellarEquivalent (K.stellarSubdivision σ v)

A complex is stellar equivalent to any of its starrings at a fresh vertex.

theorem PreAbstractSimplicialComplex.equivalence_stellarEquivalent {ι : Type u_1} [DecidableEq ι] : Equivalence StellarEquivalent

Stellar equivalence is an equivalence relation.

theorem PreAbstractSimplicialComplex.StellarEquivalent.induction_on {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) {P : PreAbstractSimplicialComplex ι → PreAbstractSimplicialComplex ι → Prop} (rel : ∀ (A B : PreAbstractSimplicialComplex ι), A.IsStellarMove B → P A B) (refl : ∀ (A : PreAbstractSimplicialComplex ι), P A A) (symm : ∀ (A B : PreAbstractSimplicialComplex ι), P A B → P B A) (trans : ∀ (A B C : PreAbstractSimplicialComplex ι), P A B → P B C → P A C) : P K L

To prove a property of stellar equivalent complexes, it suffices to prove it for a stellar move and show that it is reflexive, symmetric, and transitive.

theorem PreAbstractSimplicialComplex.StellarEquivalent.map {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (h : K.StellarEquivalent L) (f : ι → κ) (hf : Function.Injective f) : (K.map f).StellarEquivalent (L.map f)

An injective relabeling carries a stellar equivalence to one between the image complexes.

theorem PreAbstractSimplicialComplex.StellarEquivalent.dimension_eq {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) : L.dimension = K.dimension

Stellar equivalent complexes have the same dimension.

theorem PreAbstractSimplicialComplex.StellarEquivalent.finite_faces_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) : K.faces.Finite ↔ L.faces.Finite

Stellar equivalence preserves and reflects finiteness of the face collection.

theorem PreAbstractSimplicialComplex.StellarEquivalent.ne_bot {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) (hL : L ≠ ⊥) : K ≠ ⊥

A complex stellar equivalent to a complex with a face has a face itself.

Intrinsic stellar equivalence

def PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling {ι : Type u_1} [DecidableEq ι] (K L : PreAbstractSimplicialComplex ι) : Prop

Stellar equivalence up to relabeling. At each generating step, the two complexes are injectively relabeled inside the common enlarged vertex type ι ⊕ ℕ. The generator existentially quantifies these relabelings, and the equivalence closure lets such comparisons compose.

Equations

• K.StellarEquivalentUpToRelabeling L = Relation.EqvGen (fun (A B : PreAbstractSimplicialComplex ι) => ∃ (f : ι ↪ ι ⊕ ℕ) (g : ι ↪ ι ⊕ ℕ), (A.map ⇑f).StellarEquivalent (B.map ⇑g)) K L

theorem PreAbstractSimplicialComplex.StellarEquivalent.stellarEquivalentUpToRelabeling {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalent L) : K.StellarEquivalentUpToRelabeling L

A same-type stellar equivalence gives an intrinsic stellar equivalence.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.refl {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) : K.StellarEquivalentUpToRelabeling K

Every complex is intrinsically stellar equivalent to itself.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.symm {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) : L.StellarEquivalentUpToRelabeling K

Intrinsic stellar equivalence is symmetric.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.trans {ι : Type u_1} [DecidableEq ι] {K L M : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) (h' : L.StellarEquivalentUpToRelabeling M) : K.StellarEquivalentUpToRelabeling M

Intrinsic stellar equivalences compose.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.of_common_relabeling {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (f g : ι ↪ ι ⊕ ℕ) (h : (K.map ⇑f).StellarEquivalent (L.map ⇑g)) : K.StellarEquivalentUpToRelabeling L

A stellar equivalence after injectively relabeling both complexes into the common enlarged vertex type gives an intrinsic stellar equivalence.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.induction_on {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) {P : PreAbstractSimplicialComplex ι → PreAbstractSimplicialComplex ι → Prop} (rel : ∀ (A B : PreAbstractSimplicialComplex ι) (f g : ι ↪ ι ⊕ ℕ), (A.map ⇑f).StellarEquivalent (B.map ⇑g) → P A B) (refl : ∀ (A : PreAbstractSimplicialComplex ι), P A A) (symm : ∀ (A B : PreAbstractSimplicialComplex ι), P A B → P B A) (trans : ∀ (A B C : PreAbstractSimplicialComplex ι), P A B → P B C → P A C) : P K L

To prove a property of intrinsically stellar equivalent complexes, it suffices to prove it for a common-relabeling generator and show that it is reflexive, symmetric, and transitive.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.map {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {κ : Type u_2} [DecidableEq κ] (h : K.StellarEquivalentUpToRelabeling L) (f : ι → κ) (hf : Function.Injective f) : (K.map f).StellarEquivalentUpToRelabeling (L.map f)

An injective relabeling transports intrinsic stellar equivalence.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.dimension_eq {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) : L.dimension = K.dimension

Intrinsically stellar equivalent complexes have the same dimension.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.finite_faces_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) : K.faces.Finite ↔ L.faces.Finite

Intrinsic stellar equivalence preserves and reflects finiteness of the face collection.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.ne_bot_iff {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) : K ≠ ⊥ ↔ L ≠ ⊥

Intrinsic stellar equivalence preserves and reflects nonvoidness.

theorem PreAbstractSimplicialComplex.StellarEquivalentUpToRelabeling.ne_bot {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} (h : K.StellarEquivalentUpToRelabeling L) (hL : L ≠ ⊥) : K ≠ ⊥

A complex intrinsically stellar equivalent to a nonvoid complex is nonvoid.