Geometric cones and radial extensions

The geometric cone s.cone 𝕜 on a subset of a module over a partially ordered division semiring 𝕜 consists of its apex and the rays (t • x, t) with x ∈ s and t > 0. When 0 < 1 in 𝕜, the base s sits in the cone at height one. The radial extension coneMap 𝕜 f preserves height and scales the base value by that height. It depends only on the restriction of f to the base, respects composition, and carries maps of bases and their left inverses to maps of cones and their left inverses.

These constructions provide cone models for extending maps of links across vertex stars, independently of any PL regularity assumptions.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 1, “Joins and Cones”, pp. 1–2.

def Set.cone (𝕜 : Type u_1) {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] (s : Set E) : Set (E × 𝕜)

The geometric cone on a set, with its apex at height zero. When 0 < 1 in 𝕜, the base sits at height one (Set.mk_one_mem_cone_iff). The cone on the empty set consists of the apex alone.

theorem Set.mem_cone {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] {s : Set E} {p : E × 𝕜} : p ∈ cone 𝕜 s ↔ p = 0 ∨ 0 < p.2 ∧ p.2⁻¹ • p.1 ∈ s

Cone membership separates the apex from points with a normalized base point.

@[simp]

theorem Set.zero_mem_cone {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] (s : Set E) : 0 ∈ cone 𝕜 s

The apex lies in every cone.

@[simp]

theorem Set.cone_empty (𝕜 : Type u_1) {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] : cone 𝕜 ∅ = {0}

The empty base contributes only the cone apex.

@[simp]

theorem Set.smul_mem_cone_iff {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] {s : Set E} (x : E) {t : 𝕜} (ht : 0 < t) : (t • x, t) ∈ cone 𝕜 s ↔ x ∈ s

At positive height, cone membership is membership of the normalized point in the base.

@[simp]

theorem Set.mk_one_mem_cone_iff {𝕜 : Type u_1} {E : Type u_2} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [PartialOrder 𝕜] [ZeroLEOneClass 𝕜] {s : Set E} (x : E) : (x, 1) ∈ cone 𝕜 s ↔ x ∈ s

When 0 < 1, the base of the cone is its slice at height one.

def TauCeti.coneMap (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) (p : E × 𝕜) : F × 𝕜

A map of bases extends radially to a height-preserving map of geometric cones.

@[simp]

theorem TauCeti.coneMap_fst {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) (p : E × 𝕜) : (coneMap 𝕜 f p).1 = p.2 • f (p.2⁻¹ • p.1)

The first component of the radial extension is its scaled base value.

@[simp]

theorem TauCeti.coneMap_snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) (p : E × 𝕜) : (coneMap 𝕜 f p).2 = p.2

The radial extension preserves height.

@[simp]

theorem TauCeti.coneMap_zero (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) : coneMap 𝕜 f 0 = 0

The radial extension fixes the apex.

@[simp]

theorem TauCeti.coneMap_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) (x : E) (t : 𝕜) : coneMap 𝕜 f (t • x, t) = (t • f x, t)

The radial extension agrees with the scaled base map on each ray, including at height zero.

@[simp]

theorem TauCeti.coneMap_one (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] (f : E → F) (x : E) : coneMap 𝕜 f (x, 1) = (f x, 1)

At height one, radial extension is the original base map.

theorem TauCeti.coneMap_comp (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} {G : Type u_4} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] (g : F → G) (f : E → F) : coneMap 𝕜 (g ∘ f) = coneMap 𝕜 g ∘ coneMap 𝕜 f

Radial extension respects composition, including at height zero.

theorem Set.EqOn.coneMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [PartialOrder 𝕜] {s : Set E} {f g : E → F} (h : EqOn f g s) : EqOn (TauCeti.coneMap 𝕜 f) (TauCeti.coneMap 𝕜 g) (cone 𝕜 s)

Radial extensions agree on a cone whenever their base maps agree on its base.

theorem Set.MapsTo.coneMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [PartialOrder 𝕜] {s : Set E} {u : Set F} {f : E → F} (hf : MapsTo f s u) : MapsTo (TauCeti.coneMap 𝕜 f) (cone 𝕜 s) (cone 𝕜 u)

Radial extension carries a cone to the cone on any set containing the base image.

theorem Set.LeftInvOn.coneMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [DivisionSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [PartialOrder 𝕜] {s : Set E} {f : E → F} {g : F → E} (h : LeftInvOn g f s) : LeftInvOn (TauCeti.coneMap 𝕜 g) (TauCeti.coneMap 𝕜 f) (cone 𝕜 s)

A left inverse on bases extends to a left inverse on their cones.