Relabeling polyhedra with unused vertices

Injective relabeling of a precomplex induces a homeomorphism of its polyhedron. The polyhedra carry the subspace topologies of arbitrary ambient weak realizations containing the respective complexes. Thus the result applies to links and stellar moves, which can omit ambient vertices, and to embeddings into enlarged vertex types. No finiteness assumption is needed.

The forward map pushes barycentric coordinates along the vertex embedding; its inverse pulls coordinates back. Continuity is tested on closed simplices using the weak subcomplex topology. In particular, changing the ambient complex leaves the topology of the actual polyhedron intact. These identifications transport intrinsic combinatorial sphere and ball models to geometric link models without adjoining unwanted isolated points. An explicit enumeration of a face identifies the realization of the full simplex on the enumerating type with the closed simplex of that face.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2 (polyhedra and simplicial maps).

The construction uses Mathlib's Finsupp.lcomapDomain and the affine simplex maps of TauCeti.AlgebraicTopology.SimplicialComplex.Realization.Map.

noncomputable def PreAbstractSimplicialComplex.relabelingHomeomorph {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑f ≤ L.toPreAbstractSimplicialComplex) : { x : K.Realization // (↑x).support ∈ P } ≃ₜ { y : L.Realization // (↑y).support ∈ P.map ⇑f }

An injective relabeling identifies the actual polyhedra of a precomplex and its image, inside any ambient weak realizations containing them. Vertices unused by the precomplex contribute no points.

theorem PreAbstractSimplicialComplex.le_top {ι : Type u_3} (Q : PreAbstractSimplicialComplex ι) : Q ≤ ⊤.toPreAbstractSimplicialComplex

Every precomplex is contained in the top abstract simplicial complex.

noncomputable def PreAbstractSimplicialComplex.topRealizationHomeomorph {ι : Type u_3} (P : PreAbstractSimplicialComplex ι) {A : AbstractSimplicialComplex ι} (hA : P ≤ A.toPreAbstractSimplicialComplex) : { x : ⊤.Realization // (↑x).support ∈ P } ≃ₜ { x : A.Realization // (↑x).support ∈ P }

Changing the ambient abstract complex does not change the polyhedron of a precomplex.

noncomputable def PreAbstractSimplicialComplex.realizationRelabelingHomeomorph {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) {R : PreAbstractSimplicialComplex β} (hmap : P.map ⇑f = R) (hP : P = K.toPreAbstractSimplicialComplex) (hR : R ≤ L.toPreAbstractSimplicialComplex) : K.Realization ≃ₜ { y : L.Realization // (↑y).support ∈ R }

An injective relabeling carrying the underlying precomplex of K onto R identifies the realization of K with the polyhedron of R, inside any ambient weak realization containing R.

@[simp]

theorem PreAbstractSimplicialComplex.relabelingHomeomorph_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑f ≤ L.toPreAbstractSimplicialComplex) (x : { x : K.Realization // (↑x).support ∈ P }) : ↑↑((P.relabelingHomeomorph f hK hL) x) = Finsupp.mapDomain ⇑f ↑↑x

Relabeling pushes forward the finitely supported barycentric coordinate vector.

@[simp]

theorem PreAbstractSimplicialComplex.topRealizationHomeomorph_val {α : Type u_1} (P : PreAbstractSimplicialComplex α) {A : AbstractSimplicialComplex α} (hA : P ≤ A.toPreAbstractSimplicialComplex) (x : { x : ⊤.Realization // (↑x).support ∈ P }) : ⇑↑↑((P.topRealizationHomeomorph hA) x) = ⇑↑↑x

Changing the ambient complex leaves the barycentric coordinate vector unchanged.

@[simp]

theorem PreAbstractSimplicialComplex.topRealizationHomeomorph_symm_val {α : Type u_1} (P : PreAbstractSimplicialComplex α) {A : AbstractSimplicialComplex α} (hA : P ≤ A.toPreAbstractSimplicialComplex) (x : { x : A.Realization // (↑x).support ∈ P }) : ⇑↑↑((P.topRealizationHomeomorph hA).symm x) = ⇑↑↑x

The inverse change of ambient complex also preserves barycentric coordinates.

@[simp]

theorem PreAbstractSimplicialComplex.relabelingHomeomorph_symm_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑f ≤ L.toPreAbstractSimplicialComplex) (y : { y : L.Realization // (↑y).support ∈ P.map ⇑f }) : ↑↑((P.relabelingHomeomorph f hK hL).symm y) = Finsupp.comapDomain ⇑f ↑↑y ⋯

Inverse relabeling pulls back the barycentric coordinate vector.

@[simp]

theorem PreAbstractSimplicialComplex.realizationRelabelingHomeomorph_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) {R : PreAbstractSimplicialComplex β} (hmap : P.map ⇑f = R) (hP : P = K.toPreAbstractSimplicialComplex) (hR : R ≤ L.toPreAbstractSimplicialComplex) (x : K.Realization) : ↑↑((P.realizationRelabelingHomeomorph f hmap hP hR) x) = Finsupp.mapDomain ⇑f ↑x

The relabeling of a realization pushes forward the barycentric coordinate vector.

@[simp]

theorem PreAbstractSimplicialComplex.realizationRelabelingHomeomorph_symm_val {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (f : α ↪ β) {R : PreAbstractSimplicialComplex β} (hmap : P.map ⇑f = R) (hP : P = K.toPreAbstractSimplicialComplex) (hR : R ≤ L.toPreAbstractSimplicialComplex) (y : { y : L.Realization // (↑y).support ∈ R }) : ↑((P.realizationRelabelingHomeomorph f hmap hP hR).symm y) = Finsupp.comapDomain ⇑f ↑↑y ⋯

The inverse relabeling of a realization pulls back the barycentric coordinate vector.

noncomputable def PreAbstractSimplicialComplex.ambientHomeomorph {α : Type u_1} (P : PreAbstractSimplicialComplex α) [DecidableEq α] {K' L' : AbstractSimplicialComplex α} (hK : P ≤ K'.toPreAbstractSimplicialComplex) (hL : P ≤ L'.toPreAbstractSimplicialComplex) : { x : K'.Realization // (↑x).support ∈ P } ≃ₜ { x : L'.Realization // (↑x).support ∈ P }

Changing the containing weak realization preserves the polyhedron of a precomplex and its barycentric coordinates. No finiteness assumption is needed.

@[simp]

theorem PreAbstractSimplicialComplex.ambientHomeomorph_val {α : Type u_1} (P : PreAbstractSimplicialComplex α) [DecidableEq α] {K' L' : AbstractSimplicialComplex α} (hK : P ≤ K'.toPreAbstractSimplicialComplex) (hL : P ≤ L'.toPreAbstractSimplicialComplex) (x : { x : K'.Realization // (↑x).support ∈ P }) : ↑↑((P.ambientHomeomorph hK hL) x) = ↑↑x

Changing the ambient complex leaves the barycentric coordinate vector unchanged.

noncomputable def AbstractSimplicialComplex.realizationTopHomeomorphFace {α : Type u_1} {ι : Type u_2} [Fintype α] [DecidableEq ι] (K : AbstractSimplicialComplex ι) (f : α ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) : ⊤.Realization ≃ₜ { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }

An enumeration of a face of K identifies the realization of the full simplex on the enumerating type with the closed simplex of that face in the weak realization of K.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphFace_val {α : Type u_1} {ι : Type u_2} [Fintype α] [DecidableEq ι] (K : AbstractSimplicialComplex ι) (f : α ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (x : ⊤.Realization) : ↑↑((K.realizationTopHomeomorphFace f hf) x) = Finsupp.mapDomain ⇑f ↑x

The face homeomorphism pushes forward the barycentric coordinate vector.

@[simp]

theorem AbstractSimplicialComplex.realizationTopHomeomorphFace_symm_val {α : Type u_1} {ι : Type u_2} [Fintype α] [DecidableEq ι] (K : AbstractSimplicialComplex ι) (f : α ↪ ι) (hf : Finset.image (⇑f) Finset.univ ∈ K) (y : { x : K.Realization // (↑x).support ⊆ Finset.image (⇑f) Finset.univ }) : ↑((K.realizationTopHomeomorphFace f hf).symm y) = Finsupp.comapDomain ⇑f ↑↑y ⋯

The inverse face homeomorphism pulls back the barycentric coordinate vector.