Descending PL maps through vertex relabelings

A map between injectively relabeled polyhedra with a PL ambient coordinate formula induces a map between the original polyhedra with a PL coordinate formula. Extend the input by zero, apply the given formula, and restrict the output coordinates. For a homeomorphism, applying the same result to its inverse transports the inverse PL formula as well.

This removes the auxiliary vertex labels used to compare polyhedra by stellar moves, so that their PL identifications can be used on the original sphere and ball links. The polyhedra may lie in arbitrary containing weak realizations. No finiteness, compactness, or global comparison with the coordinate topology is required, and unused ambient vertices contribute no points.

The same coordinate transport realizes a PLHomeomorphic relation inside arbitrary ambient complexes, or as a homeomorphism to the full realization of its target complex. These forms are the interface used to transport standard PL charts to a subpolyhedron.

The coordinate transport uses relabelingHomeomorph and its extension and restriction formulas, together with TauCeti.IsPLOn.comp.

Reference: C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology, Chapters 1–2.

theorem PreAbstractSimplicialComplex.isPLOn_restriction_comp_extendByZero {α : Type u_1} {β : Type u_2} {κ : Type u_3} {ν : Type u_4} [DecidableEq κ] [DecidableEq ν] {K : AbstractSimplicialComplex α} {L : AbstractSimplicialComplex β} {A : AbstractSimplicialComplex κ} {B : AbstractSimplicialComplex ν} (P : PreAbstractSimplicialComplex α) (Q : PreAbstractSimplicialComplex β) (e : α ↪ κ) (d : β ↪ ν) (hK : P ≤ K.toPreAbstractSimplicialComplex) (hL : Q ≤ L.toPreAbstractSimplicialComplex) (hA : P.map ⇑e ≤ A.toPreAbstractSimplicialComplex) (hB : Q.map ⇑d ≤ B.toPreAbstractSimplicialComplex) (h : { x : A.Realization // (↑x).support ∈ P.map ⇑e } → { y : B.Realization // (↑y).support ∈ Q.map ⇑d }) (f : (κ → ℝ) → ν → ℝ) (hf : TauCeti.IsPLOn f (Set.range fun (x : { x : A.Realization // (↑x).support ∈ P.map ⇑e }) => ⇑↑↑x)) (hcoord : ∀ (x : { x : A.Realization // (↑x).support ∈ P.map ⇑e }), f ⇑↑↑x = ⇑↑↑(h x)) : TauCeti.IsPLOn (⇑(Function.ExtendByZero.restriction ℝ ⇑d) ∘ f ∘ ⇑(Function.ExtendByZero.continuousLinearMap ℝ ℝ ⇑e)) (Set.range fun (x : { x : K.Realization // (↑x).support ∈ P }) => ⇑↑↑x) ∧ ∀ (x : { x : K.Realization // (↑x).support ∈ P }), (⇑(Function.ExtendByZero.restriction ℝ ⇑d) ∘ f ∘ ⇑(Function.ExtendByZero.continuousLinearMap ℝ ℝ ⇑e)) ⇑↑↑x = ⇑↑↑((⇑(Q.relabelingHomeomorph d hL hB).symm ∘ h ∘ ⇑(P.relabelingHomeomorph e hK hA)) x)

A PL coordinate formula for a map of relabeled polyhedra descends to the original polyhedra. Its explicit formula extends the input coordinates by zero and restricts the output coordinates. For a homeomorphism, use the theorem with its inverse and the two relabelings exchanged to descend the inverse formula.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.of_common_relabeling {α : Type u_1} {κ : Type u_3} [DecidableEq κ] {A B : PreAbstractSimplicialComplex α} {e d : α ↪ κ} (h : (A.map ⇑e).PLHomeomorphic (B.map ⇑d)) : A.PLHomeomorphic B

A PL homeomorphism after two injective relabelings descends to a PL homeomorphism before relabeling. The two complexes may use different embeddings into the common target vertex type.

The descended coordinate formulas extend the input by zero along the source embedding, apply the given formula, and restrict along the target embedding.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.relabeling {γ : Type u_5} {δ : Type u_6} [DecidableEq δ] (P : PreAbstractSimplicialComplex γ) (e : γ ↪ δ) : P.PLHomeomorphic (P.map ⇑e)

Injectively relabeling the vertices of a complex does not change its PL homeomorphism type.

The forward ambient formula extends barycentric coordinates by zero; the inverse formula restricts them to the original vertex labels.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.exists_homeomorph_ambient {γ : Type u_5} {δ : Type u_6} {P : PreAbstractSimplicialComplex γ} {Q : PreAbstractSimplicialComplex δ} {C : AbstractSimplicialComplex γ} {D : AbstractSimplicialComplex δ} (h : P.PLHomeomorphic Q) (hP : P ≤ C.toPreAbstractSimplicialComplex) (hQ : Q ≤ D.toPreAbstractSimplicialComplex) : ∃ (e : { x : C.Realization // (↑x).support ∈ P } ≃ₜ { y : D.Realization // (↑y).support ∈ Q }) (f : (γ → ℝ) → δ → ℝ) (g : (δ → ℝ) → γ → ℝ), TauCeti.IsPLOn f (Set.range fun (x : { x : C.Realization // (↑x).support ∈ P }) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (Set.range fun (y : { y : D.Realization // (↑y).support ∈ Q }) => ⇑↑↑y) ∧ (∀ (x : { x : C.Realization // (↑x).support ∈ P }), f ⇑↑↑x = ⇑↑↑(e x)) ∧ ∀ (y : { y : D.Realization // (↑y).support ∈ Q }), g ⇑↑↑y = ⇑↑↑(e.symm y)

Realize a PL homeomorphism inside arbitrary ambient simplicial complexes containing its two polyhedra. The coordinate formulas and their PL domains are transported unchanged.

theorem PreAbstractSimplicialComplex.PLHomeomorphic.exists_homeomorph_realization {γ : Type u_5} {δ : Type u_6} {P : PreAbstractSimplicialComplex γ} {C : AbstractSimplicialComplex γ} {D : AbstractSimplicialComplex δ} (h : P.PLHomeomorphic D.toPreAbstractSimplicialComplex) (hP : P ≤ C.toPreAbstractSimplicialComplex) : ∃ (e : { x : C.Realization // (↑x).support ∈ P } ≃ₜ D.Realization) (f : (γ → ℝ) → δ → ℝ) (g : (δ → ℝ) → γ → ℝ), TauCeti.IsPLOn f (Set.range fun (x : { x : C.Realization // (↑x).support ∈ P }) => ⇑↑↑x) ∧ TauCeti.IsPLOn g (Set.range fun (y : D.Realization) => ⇑↑y) ∧ (∀ (x : { x : C.Realization // (↑x).support ∈ P }), f ⇑↑↑x = ⇑↑(e x)) ∧ ∀ (y : D.Realization), g ⇑↑y = ⇑↑↑(e.symm y)

Realize the target of a PL homeomorphism as its full simplicial realization rather than as the equivalent support-restricted subtype.