Piecewise-linear coordinate formulas under injective relabeling

An injective relabeling extends a coordinate vector by zero on unused vertices. Conjugate a coordinate formula by extension on its output and restriction on its input. The resulting formula is PL on the relabeled set exactly when the original formula is PL. Both index types may be infinite: extension and restriction are continuous linear maps for their product topologies.

This is the coordinate transport needed to compare PL maps of polyhedra described on different ambient vertex sets, including a common enlarged set used for stellar moves.

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

theorem TauCeti.isPLOn_extendByZero_iff {ι : Type u_1} {κ : Type u_2} {α : Type u_3} {β : Type u_4} (e : ι ↪ κ) (d : α ↪ β) {f : (ι → ℝ) → α → ℝ} {s : Set (ι → ℝ)} : IsPLOn (fun (y : κ → ℝ) => Function.extend (⇑d) (f (y ∘ ⇑e)) 0) (⇑(Function.ExtendByZero.continuousLinearMap ℝ ℝ ⇑e) '' s) ↔ IsPLOn f s

Extending output coordinates by zero and pulling input coordinates back along injections preserves and reflects PL regularity on the relabeled domain.