Linear coordinate formulas for relabeling polyhedra

The homeomorphism of polyhedra induced by an injective vertex relabeling has ambient continuous linear formulas in both directions: extension by zero and coordinate restriction. These formulas apply to arbitrary ambient vertex sets and weak realizations, including precomplexes that leave vertices unused. No global comparison between the weak and coordinate topologies is required.

Together with TauCeti.isPLOn_extendByZero_iff, the formulas transport PL coordinate maps through changes of ambient vertex sets. In particular, relabeling does not lose the PL regularity of identifications obtained from stellar moves.

Reference: Rourke–Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

theorem PreAbstractSimplicialComplex.relabelingHomeomorph_coe_eq_extendByZero {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (e : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑e ≤ L.toPreAbstractSimplicialComplex) (x : { x : K.Realization // (↑x).support ∈ P }) : ⇑↑↑((P.relabelingHomeomorph e hK hL) x) = (Function.ExtendByZero.continuousLinearMap ℝ ℝ ⇑e) ⇑↑↑x

Relabeling of polyhedra extends the ambient coordinate vector by zero.

theorem PreAbstractSimplicialComplex.relabelingHomeomorph_symm_coe_eq_restriction {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (e : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑e ≤ L.toPreAbstractSimplicialComplex) (y : { y : L.Realization // (↑y).support ∈ P.map ⇑e }) : ⇑↑↑((P.relabelingHomeomorph e hK hL).symm y) = (Function.ExtendByZero.restriction ℝ ⇑e) ⇑↑↑y

Inverse relabeling of polyhedra restricts the ambient coordinate vector along the vertex embedding.

theorem PreAbstractSimplicialComplex.range_coe_map_eq_image_extendByZero {α : Type u_1} {β : Type u_2} [DecidableEq β] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} (P : PreAbstractSimplicialComplex α) (e : α ↪ β) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : P.map ⇑e ≤ L.toPreAbstractSimplicialComplex) : (Set.range fun (y : { y : L.Realization // (↑y).support ∈ P.map ⇑e }) => ⇑↑↑y) = ⇑(Function.ExtendByZero.continuousLinearMap ℝ ℝ ⇑e) '' Set.range fun (x : { x : K.Realization // (↑x).support ∈ P }) => ⇑↑↑x

The coordinate range of a relabeled polyhedron is the extension by zero of the original coordinate range. This includes precomplexes with unused ambient vertices.