Coning piecewise-affine maps

The geometric cone on s ⊆ E is the apex together with the rays (t • x, t), where x ∈ s and t > 0. A map of bases extends by preserving the height and scaling its value by that height. A finite piecewise-affine decomposition on any subset of a real topological vector space extends to a finite piecewise-linear one on the entire cone, including the apex. In particular, a PL map on a compact base extends to a PL map on its cone.

This supplies the PL regularity needed when extending maps of links to maps of vertex stars. The PL extension assumes a compact base in a real coordinate product. The affine map coneToJoin b reads a cone point as a point of the join of the base with a point b, placing the apex at b.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 1, “Joins and Cones”, pp. 1–2, Example 1.5(4), p. 5, and Chapter 2, “Pseudo-Radial Projection”, pp. 20–21.

theorem TauCeti.IsPiecewiseAffineOn.coneMap {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {s : Set E} {f : E → F} (hf : IsPiecewiseAffineOn f s) : IsPiecewiseAffineOn (TauCeti.coneMap ℝ f) (Set.cone ℝ s)

A finite piecewise-affine map extends piecewise affinely over the whole geometric cone, including the apex. No boundedness, closedness or polyhedral assumption on the base is needed.

def TauCeti.coneToJoin {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (b : F) : F × ℝ →ᴬ[ℝ] F

The affine map (p, t) ↦ p - t • b + b from cone coordinates to the join with b. It sends the apex to b and the ray point (t • x, t) to t • x + (1 - t) • b, so the cone point at height t over x goes to the point at parameter 1 - t on the segment from x to b.

@[simp]

theorem TauCeti.coneToJoin_apply {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] (b : F) (p : F × ℝ) : (coneToJoin b) p = p.1 - p.2 • b + b

theorem TauCeti.IsPLOn.coneMap {ι : Type u_1} {F : Type u_2} [AddCommGroup F] [Module ℝ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {s : Set (ι → ℝ)} {f : (ι → ℝ) → F} (hf : IsPLOn f s) (hs : IsCompact s) : IsPLOn (TauCeti.coneMap ℝ f) (Set.cone ℝ s)

A PL map on a compact base extends to a PL map of geometric cones, including at the apex. The target may be any real topological vector space.