Geometric stars and radial coordinates

Open vertex stars cover the realization, and closed stars consist of points whose carriers lie in the corresponding combinatorial closed star. Finite closed stars are compact.

The closed star of a vertex is a cone on its link. Removing the apex gives a product of that link with [0, 1): the interval coordinate is the barycentric coordinate at the apex, and the link coordinate is obtained by deleting that coordinate and normalizing the rest. These coordinates are the radial part of the local models of triangulated manifolds.

The equivalence works for arbitrary vertex types. It is a homeomorphism whenever the weak realization topology agrees with the coordinate topology, in particular for finite vertex types. The geometric star and link are subsets of the original realization, so no extra vertices are introduced into either local model. An isolated vertex has empty link and empty punctured star, as the product formula requires.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2, “Pseudo-Radial Projection”, pp. 20–21 (the star is the cone on the link).

def AbstractSimplicialComplex.openStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : Set K.Realization

The open star of a vertex consists of points with positive barycentric coordinate at that vertex. Equivalently, their carriers contain the vertex.

Equations

• K.openStarRealization v = {x : K.Realization | 0 < ↑x v}

@[simp]

theorem AbstractSimplicialComplex.mem_openStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) {v : ι} {x : K.Realization} : x ∈ K.openStarRealization v ↔ 0 < ↑x v

Membership in the open star is positivity of the corresponding coordinate.

theorem AbstractSimplicialComplex.mem_openStarRealization_iff_mem_support {ι : Type u_1} (K : AbstractSimplicialComplex ι) {v : ι} {x : K.Realization} : x ∈ K.openStarRealization v ↔ v ∈ (↑x).support

A point lies in the open star exactly when its carrier contains the vertex.

theorem AbstractSimplicialComplex.isOpen_openStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : IsOpen (K.openStarRealization v)

Open stars are open for the weak topology, since coordinates are continuous.

theorem AbstractSimplicialComplex.exists_mem_openStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) (x : K.Realization) : ∃ (v : ι), x ∈ K.openStarRealization v

Every realization point belongs to an open vertex star.

@[simp]

theorem AbstractSimplicialComplex.iUnion_openStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) : ⋃ (v : ι), K.openStarRealization v = Set.univ

The open vertex stars cover the realization.

def AbstractSimplicialComplex.closedStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (σ : Finset ι) : Set K.Realization

The realized closed star of a finite vertex set consists of points whose carriers lie in its closed star.

Equations

• K.closedStarRealization σ = {x : K.Realization | (↑x).support ∈ K.closedStar σ}

@[simp]

theorem AbstractSimplicialComplex.mem_closedStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] {σ : Finset ι} {x : K.Realization} : x ∈ K.closedStarRealization σ ↔ (↑x).support ∈ K.closedStar σ

Membership in the realized closed star is closed-star membership of the carrier.

theorem AbstractSimplicialComplex.openStarRealization_subset_closedStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : K.openStarRealization v ⊆ K.closedStarRealization {v}

Each open star lies in its closed star.

theorem AbstractSimplicialComplex.isCompact_closedStarRealization {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] {σ : Finset ι} (hfin : (K.closedStar σ).faces.Finite) : IsCompact (K.closedStarRealization σ)

The realization of a finite closed star is compact.

theorem AbstractSimplicialComplex.mem_closedStarRealization_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] {σ : Finset ι} {x : K.Realization} : x ∈ K.closedStarRealization σ ↔ (↑x).support ∪ σ ∈ K

Closed-star membership is determined by adjoining the finite vertex set to the carrier.

def AbstractSimplicialComplex.geometricLink {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : Set K.Realization

The polyhedron of the link of v, inside the realization of K.

Equations

• K.geometricLink v = {x : K.Realization | ↑x v = 0 ∧ x ∈ K.closedStarRealization {v}}

@[simp]

theorem AbstractSimplicialComplex.mem_geometricLink {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : K.Realization) : x ∈ K.geometricLink v ↔ ↑x v = 0 ∧ x ∈ K.closedStarRealization {v}

Geometric link membership is closed-star membership with zero apex coordinate.

@[simp]

theorem AbstractSimplicialComplex.geometricLink_apex {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : ↑(K.geometricLink v)) : ↑↑x v = 0

The apex coordinate of a geometric link point is zero.

theorem AbstractSimplicialComplex.mem_geometricLink_iff {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : K.Realization) : x ∈ K.geometricLink v ↔ (↑x).support ∈ K.link {v}

A point lies in the geometric link exactly when its carrier is a link face.

noncomputable def AbstractSimplicialComplex.starApex {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : ↑(K.closedStarRealization {v})

The apex, regarded as a point of its geometric closed star.

Equations

• K.starApex v = ⟨K.vertex v, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.starApex_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : ↑(K.starApex v) = K.vertex v

The underlying realization point of the closed-star apex is its vertex.

def AbstractSimplicialComplex.puncturedClosedStar {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : Set K.Realization

The punctured geometric closed star, expressed by the apex coordinate being less than one.

Equations

• K.puncturedClosedStar v = {x : K.Realization | x ∈ K.closedStarRealization {v} ∧ ↑x v < 1}

@[simp]

theorem AbstractSimplicialComplex.mem_puncturedClosedStar {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : K.Realization) : x ∈ K.puncturedClosedStar v ↔ x ∈ K.closedStarRealization {v} ∧ ↑x v < 1

Membership in the punctured closed star.

noncomputable def AbstractSimplicialComplex.starLinkProjection {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : ↑(K.puncturedClosedStar v)) : ↑(K.geometricLink v)

Radial projection from a punctured vertex star onto its geometric link.

Equations

• K.starLinkProjection v x = ⟨⟨(AbstractSimplicialComplex.normalizedLinkSimplex✝ K v x).weights, ⋯⟩, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.starLinkProjection_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : ↑(K.puncturedClosedStar v)) (w : ι) : ↑↑(K.starLinkProjection v x) w = if w = v then 0 else (1 - ↑↑x v)⁻¹ * ↑↑x w

Barycentric coordinates of radial projection onto the link.

noncomputable def AbstractSimplicialComplex.starRay {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (y : ↑(K.geometricLink v)) (t : ↑(Set.Ico 0 1)) : ↑(K.puncturedClosedStar v)

Move from a link point towards the apex, with apex coordinate t < 1.

Equations

• K.starRay v y t = ⟨⟨(1 - ↑t) • ↑↑y + Finsupp.single v ↑t, ⋯⟩, ⋯⟩

@[simp]

theorem AbstractSimplicialComplex.starRay_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (y : ↑(K.geometricLink v)) (t : ↑(Set.Ico 0 1)) (w : ι) : ↑↑(K.starRay v y t) w = (1 - ↑t) * ↑↑y w + if v = w then ↑t else 0

Coordinates of a ray from the link to its star apex.

@[simp]

theorem AbstractSimplicialComplex.starLinkProjection_starRay {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (y : ↑(K.geometricLink v)) (t : ↑(Set.Ico 0 1)) : K.starLinkProjection v (K.starRay v y t) = y

Radial projection recovers the link point of a ray.

@[simp]

theorem AbstractSimplicialComplex.starRay_starLinkProjection {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : ↑(K.puncturedClosedStar v)) : K.starRay v (K.starLinkProjection v x) ⟨↑↑x v, ⋯⟩ = x

The ray determined by a point's radial projection and apex coordinate recovers that point.

noncomputable def AbstractSimplicialComplex.puncturedClosedStarEquiv {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : ↑(K.puncturedClosedStar v) ≃ ↑(K.geometricLink v) × ↑(Set.Ico 0 1)

The punctured closed star is the product of its geometric link and [0, 1). The interval coordinate is the coordinate at the apex.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AbstractSimplicialComplex.puncturedClosedStarEquiv_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (x : ↑(K.puncturedClosedStar v)) : (K.puncturedClosedStarEquiv v) x = (K.starLinkProjection v x, ⟨↑↑x v, ⋯⟩)

The general radial equivalence records projection and the apex coordinate.

@[simp]

theorem AbstractSimplicialComplex.puncturedClosedStarEquiv_symm_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (p : ↑(K.geometricLink v) × ↑(Set.Ico 0 1)) : (K.puncturedClosedStarEquiv v).symm p = K.starRay v p.1 p.2

The inverse radial equivalence is the ray from the link to the apex.

theorem AbstractSimplicialComplex.puncturedClosedStar_eq_sdiff_vertex {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : K.puncturedClosedStar v = K.closedStarRealization {v} \ {K.vertex v}

The coordinate description of the punctured star removes exactly the apex.

theorem AbstractSimplicialComplex.closedStarRealization_singleton_eq_insert_range_starRay {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) : K.closedStarRealization {v} = insert (K.vertex v) (Set.range fun (p : ↑(K.geometricLink v) × ↑(Set.Ico 0 1)) => ↑(K.starRay v p.1 p.2))

The whole closed star consists of the apex and the rays from its link. This includes the case of an isolated vertex, where the ray family is empty.

theorem AbstractSimplicialComplex.continuous_starLinkProjection {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) : Continuous (K.starLinkProjection v)

Radial projection is continuous when the realization has its coordinate topology.

theorem AbstractSimplicialComplex.continuous_starRay {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) : Continuous fun (p : ↑(K.geometricLink v) × ↑(Set.Ico 0 1)) => K.starRay v p.1 p.2

The star rays vary continuously when the realization has its coordinate topology.

noncomputable def AbstractSimplicialComplex.puncturedClosedStarHomeomorph {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) : ↑(K.puncturedClosedStar v) ≃ₜ ↑(K.geometricLink v) × ↑(Set.Ico 0 1)

A vertex star with its apex removed is homeomorphic to its geometric link cross [0, 1), provided the realization has its coordinate topology. The homeomorphism uses radial barycentric coordinates; isClosedEmbedding_realization_coe supplies the hypothesis for finite vertex types.

Equations

• K.puncturedClosedStarHomeomorph v hK = { toEquiv := K.puncturedClosedStarEquiv v, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem AbstractSimplicialComplex.puncturedClosedStarHomeomorph_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (x : ↑(K.puncturedClosedStar v)) : (K.puncturedClosedStarHomeomorph v hK) x = (K.starLinkProjection v x, ⟨↑↑x v, ⋯⟩)

The forward homeomorphism records the radial projection and the apex coordinate.

@[simp]

theorem AbstractSimplicialComplex.puncturedClosedStarHomeomorph_symm_apply {ι : Type u_1} (K : AbstractSimplicialComplex ι) [DecidableEq ι] (v : ι) (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (p : ↑(K.geometricLink v) × ↑(Set.Ico 0 1)) : (K.puncturedClosedStarHomeomorph v hK).symm p = K.starRay v p.1 p.2

The inverse homeomorphism takes a link point along its ray towards the apex.