Links and stars in abstract simplices

This file computes the closed star, link, and deletion constructions on the standard abstract simplex and its boundary. These formulas are the standard-model calculations used by the recursive link condition for combinatorial manifolds in layer 11 of the geometric-topology roadmap. In particular, the link of a subset in a simplex is the simplex on the complementary vertices, while the link in the boundary is the boundary of that complementary simplex.

The constructions use PreAbstractSimplicialComplex, since taking a link changes the vertices that occur. The formulas follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

Main results

• closedStar_simplex: the closed star of a subset is the whole simplex.
• link_simplex: the link of a subset is the simplex on its complementary vertices.
• deletion_simplex_self: deleting the full vertex set leaves the simplex boundary.
• link_simplexBoundary: the link of a subset is the boundary on its complementary vertices.

@[simp]

theorem PreAbstractSimplicialComplex.closedStar_simplex {ι : Type u_1} [DecidableEq ι] {V σ : Finset ι} (hσ : σ ⊆ V) : (simplex V).closedStar σ = simplex V

The closed star of any subset σ ⊆ V in the simplex on V is the entire simplex.

@[simp]

theorem PreAbstractSimplicialComplex.link_simplex {ι : Type u_1} [DecidableEq ι] {V σ : Finset ι} (hσ : σ ⊆ V) : (simplex V).link σ = simplex (V \ σ)

The link of any subset σ ⊆ V in the simplex on V is the simplex on the vertices of V not in σ.

@[simp]

theorem PreAbstractSimplicialComplex.deletion_simplex_self {ι : Type u_1} {V : Finset ι} : (simplex V).deletion V = simplexBoundary V

Deleting the full vertex set from a simplex leaves exactly its boundary.

theorem PreAbstractSimplicialComplex.mem_closedStar_simplexBoundary {ι : Type u_1} [DecidableEq ι] {V σ ρ : Finset ι} : ρ ∈ (simplexBoundary V).closedStar σ ↔ ρ.Nonempty ∧ ρ ∪ σ ⊂ V

A set ρ lies in the closed star of σ in the boundary of the simplex on V exactly when ρ is nonempty and ρ ∪ σ is a proper subset of V.

@[simp]

theorem PreAbstractSimplicialComplex.link_simplexBoundary {ι : Type u_1} [DecidableEq ι] {V σ : Finset ι} (hσ : σ ⊆ V) : (simplexBoundary V).link σ = simplexBoundary (V \ σ)

The link of any subset σ ⊆ V in the boundary of the simplex on V is the boundary of the simplex on the complementary vertices.

theorem PreAbstractSimplicialComplex.link_simplex_self {ι : Type u_1} [DecidableEq ι] {V : Finset ι} : (simplex V).link V = ⊥

The link of the full vertex set in its simplex is empty. (simp also proves this via link_simplex; the named form is kept for convenience.)

theorem PreAbstractSimplicialComplex.link_simplexBoundary_self {ι : Type u_1} [DecidableEq ι] {V : Finset ι} : (simplexBoundary V).link V = ⊥

The link of the full vertex set V in the boundary of the simplex on V is empty (note V itself is not a face of that boundary). The statement also covers the empty spanning set. (simp also proves this via link_simplexBoundary; the named form is kept for convenience.)