Purity of combinatorial manifolds

Combinatorial n-balls and n-spheres are pure: every face extends to an n-dimensional face. The vertex-link condition then implies the same for combinatorial n-manifolds, without assuming that the whole complex is finite.

In particular, the link of a face with k ≤ n vertices in a combinatorial n-manifold has dimension n - k; the link of a face with n + 1 vertices is void. These statements give the dimension indices needed when classifying higher-face links and the new-vertex links of stellar subdivisions.

Reference: Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapters 2--3.

theorem PreAbstractSimplicialComplex.IsCombinatorialBall.isPure {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialBall n) : K.IsPure n

A combinatorial n-ball is pure of dimension n.

theorem PreAbstractSimplicialComplex.IsCombinatorialSphere.isPure {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialSphere n) : K.IsPure n

A combinatorial n-sphere is pure of dimension n.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.isPure {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} (h : K.IsCombinatorialManifold n) : K.IsPure n

The vertex-link condition makes a combinatorial manifold pure, including in dimension zero and for infinite complexes.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.dimension_link {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} {σ : Finset ι} (h : K.IsCombinatorialManifold n) (hσ : σ ∈ K) (hcard : σ.card ≤ n) : (K.link σ).dimension = ↑(n - σ.card)

A face below top dimension in a combinatorial n-manifold has link of dimension n - σ.card. No finiteness of the manifold or ambient vertex type is required.

theorem PreAbstractSimplicialComplex.IsCombinatorialManifold.link_eq_bot_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {n : ℕ} {σ : Finset ι} (h : K.IsCombinatorialManifold n) (hσ : σ ∈ K) : K.link σ = ⊥ ↔ σ.card = n + 1

The top-dimensional faces of a combinatorial manifold are exactly its faces with void link.