Vertex stars in combinatorial manifolds #
The closed star of a vertex in a combinatorial n-manifold, with its vertices tagged according
to whether they are the apex, is a combinatorial n-ball. In positive dimension the star is
the join of the apex with its sphere-or-ball link. In dimension zero the closed star is just
the vertex itself.
This gives a standard ball model up to stellar moves for the finite local neighbourhoods used
to construct manifold charts. The tagging agrees with map_closedStar_eq_join and is an
injective relabeling, so distinct vertices remain distinct.
References #
- C. P. Rourke, B. J. Sanderson, Introduction to Piecewise-Linear Topology, Springer (1972), Chapters 2 and 3 (joins, links, and combinatorial manifolds).
theorem
PreAbstractSimplicialComplex.IsCombinatorialManifold.isCombinatorialBall_map_closedStar
{ι : Type u_1}
[DecidableEq ι]
{K : PreAbstractSimplicialComplex ι}
{n : ℕ}
(h : K.IsCombinatorialManifold n)
{v : ι}
(hv : {v} ∈ K)
:
((K.closedStar {v}).map ⇑(TauCeti.partitionEmbedding fun (x : ι) => x ∈ {v})).IsCombinatorialBall n
The closed vertex star of a combinatorial manifold is a combinatorial ball after the injective relabeling that tags the apex on the left and all other vertices on the right.