Extending link maps across a vertex star

A map between geometric vertex links extends radially to their closed stars, taking the apex to the apex and preserving its barycentric coordinate. When the realizations have their coordinate topologies, continuous link maps have continuous extensions, including at the apex. Consequently a homeomorphism of links extends to a homeomorphism of closed stars. This supplies the conical extension of local models used in triangulated manifolds.

No compactness or nonempty-link assumption is needed: the coordinates of every link point lie in [0, 1], so all non-apex coordinates tend uniformly to zero at the apex. An isolated vertex has empty link and a singleton closed star, and is covered by the same construction. The result concerns topological homeomorphisms; it does not assert PL regularity.

References

• C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapter 2, “Pseudo-Radial Projection”, pp. 20–21 (conical extension of link models).

noncomputable def AbstractSimplicialComplex.closedStarMap {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) : ↑(L.closedStarRealization {w})

Radially extend a link map, preserving the apex coordinate and sending apex to apex.

Equations

• AbstractSimplicialComplex.closedStarMap f x = if h : ↑↑x v < 1 then let y := L.starRay w (f (K.starLinkProjection v ⟨↑x, ⋯⟩)) ⟨↑↑x v, ⋯⟩; ⟨↑y, ⋯⟩ else L.starApex w

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_starApex {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) : closedStarMap f (K.starApex v) = L.starApex w

A radial extension takes the apex to the apex.

theorem AbstractSimplicialComplex.closedStarMap_of_lt {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) (hx : ↑↑x v < 1) : closedStarMap f x = ⟨↑(L.starRay w (f (K.starLinkProjection v ⟨↑x, ⋯⟩)) ⟨↑↑x v, ⋯⟩), ⋯⟩

On a punctured star, the extension applies the link map and preserves the ray parameter.

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_apply_of_lt {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) (hx : ↑↑x v < 1) (j : κ) : ↑↑(closedStarMap f x) j = if j = w then ↑↑x v else (1 - ↑↑x v) * ↑↑(f (K.starLinkProjection v ⟨↑x, ⋯⟩)) j

Away from the apex, radial extension preserves its coordinate and scales the link image coordinates by the mass outside the apex.

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_link {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (y : ↑(K.geometricLink v)) : ↑(closedStarMap f ⟨↑y, ⋯⟩) = ↑(f y)

On a link point, radial extension agrees with the original link map.

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_apex_coordinate {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) : ↑↑(closedStarMap f x) w = ↑↑x v

The apex coordinate is unchanged by radial extension.

theorem AbstractSimplicialComplex.closedStarMap_coordinate_le {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) {j : κ} (hj : j ≠ w) : ↑↑(closedStarMap f x) j ≤ 1 - ↑↑x v

Every other coordinate of the extension is bounded by the mass outside the apex.

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_id {ι : Type u_1} [DecidableEq ι] {K : AbstractSimplicialComplex ι} {v : ι} (x : ↑(K.closedStarRealization {v})) : closedStarMap id x = x

Radial extension of the identity fixes every point of the closed star.

@[simp]

theorem AbstractSimplicialComplex.closedStarMap_comp {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [DecidableEq ι] [DecidableEq κ] [DecidableEq ν] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {N : AbstractSimplicialComplex ν} {v : ι} {w : κ} {u : ν} (g : ↑(L.geometricLink w) → ↑(N.geometricLink u)) (f : ↑(K.geometricLink v) → ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) : closedStarMap g (closedStarMap f x) = closedStarMap (g ∘ f) x

Radial extension respects composition of link maps.

theorem AbstractSimplicialComplex.continuous_closedStarMap {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (hL : Topology.IsInducing fun (x : L.Realization) => ⇑↑x) {f : ↑(K.geometricLink v) → ↑(L.geometricLink w)} (hf : Continuous f) : Continuous (closedStarMap f)

Continuous link maps extend continuously across the apex, when both realizations have their coordinate topologies.

noncomputable def AbstractSimplicialComplex.closedStarHomeomorph {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (hL : Topology.IsInducing fun (x : L.Realization) => ⇑↑x) (e : ↑(K.geometricLink v) ≃ₜ ↑(L.geometricLink w)) : ↑(K.closedStarRealization {v}) ≃ₜ ↑(L.closedStarRealization {w})

A homeomorphism between vertex links extends radially to a homeomorphism of their closed stars. This includes empty links and isolated vertices.

Equations

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

@[simp]

theorem AbstractSimplicialComplex.closedStarHomeomorph_apply {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (hL : Topology.IsInducing fun (x : L.Realization) => ⇑↑x) (e : ↑(K.geometricLink v) ≃ₜ ↑(L.geometricLink w)) (x : ↑(K.closedStarRealization {v})) : (closedStarHomeomorph hK hL e) x = closedStarMap (⇑e) x

The radial homeomorphism acts by the closed-star extension of its link homeomorphism.

@[simp]

theorem AbstractSimplicialComplex.closedStarHomeomorph_symm_apply {ι : Type u_1} {κ : Type u_2} [DecidableEq ι] [DecidableEq κ] {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} {v : ι} {w : κ} (hK : Topology.IsInducing fun (x : K.Realization) => ⇑↑x) (hL : Topology.IsInducing fun (x : L.Realization) => ⇑↑x) (e : ↑(K.geometricLink v) ≃ₜ ↑(L.geometricLink w)) (x : ↑(L.closedStarRealization {w})) : (closedStarHomeomorph hK hL e).symm x = closedStarMap (⇑e.symm) x

The inverse radial homeomorphism extends the inverse link homeomorphism.