Cone coordinates for geometric vertex stars

The barycentric coordinates of a closed vertex star become coordinates on the cone over its geometric link after deleting the apex coordinate. This affine map and its basic properties are shared by the piecewise-linear radial maps into stars and the radial ball models.

def AbstractSimplicialComplex.starToCone {ι : Type u_1} [DecidableEq ι] (v : ι) : (ι → ℝ) →ᴬ[ℝ] (ι → ℝ) × ℝ

Read a star as a cone by deleting its apex coordinate and recording the remaining mass.

@[simp]

theorem AbstractSimplicialComplex.starToCone_apply {ι : Type u_1} [DecidableEq ι] (v : ι) (x : ι → ℝ) : (starToCone v) x = (x - x v • Pi.single v 1, 1 - x v)

The coordinate formula for starToCone.

theorem AbstractSimplicialComplex.starToCone_of_lt {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (x : ↑(K.closedStarRealization {v})) (hx : ↑↑x v < 1) : (starToCone v) ⇑↑↑x = ((1 - ↑↑x v) • ⇑↑↑(K.starLinkProjection v ⟨↑x, ⋯⟩), 1 - ↑↑x v)

Away from the apex, starToCone is the link coordinate scaled by the cone height.

theorem AbstractSimplicialComplex.starToCone_of_not_lt {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (x : ↑(K.closedStarRealization {v})) (hx : ¬↑↑x v < 1) : (starToCone v) ⇑↑↑x = 0

At the apex, starToCone is the cone apex.

theorem AbstractSimplicialComplex.starToCone_mem {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (x : ↑(K.closedStarRealization {v})) : (starToCone v) ⇑↑↑x ∈ Set.cone ℝ (Set.range fun (y : ↑(K.geometricLink v)) => ⇑↑↑y)

The image of a closed star under starToCone lies in the cone over its link.