The closed star, link, and deletion of a simplex

For an abstract simplicial complex K and a simplex σ, this file builds the three local subcomplexes that organise K around σ:

• the closed star closedStar K σ, the faces ρ whose union with σ is still a face of K (equivalently, the smallest subcomplex containing every face of K that contains σ);
• the link link K σ, the part of the closed star disjoint from σ;
• the deletion deletion K σ (the anti-star), the faces of K that do not contain σ.

These are the "basic API (faces, the star and link of a simplex)" that the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md, layer 11) asks for on top of Mathlib's AbstractSimplicialComplex. The link is the load-bearing one downstream: a combinatorial n-manifold is defined there by the condition that the link of every vertex is a combinatorial (n-1)-sphere or (n-1)-ball, so link is the primitive that condition is phrased against. The definitions follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3, and they work for PreAbstractSimplicialComplex (the singleton-free version), since the link of a simplex need not contain every vertex even when K does.

Main definitions

• PreAbstractSimplicialComplex.closedStar K σ: the closed star of σ in K.
• PreAbstractSimplicialComplex.link K σ: the link of σ in K.
• PreAbstractSimplicialComplex.deletion K σ: the deletion (anti-star) of σ in K.

Main results

• PreAbstractSimplicialComplex.closedStar_le / link_le / deletion_le: each is a subcomplex of K, and link_le_closedStar places the link inside the closed star.
• PreAbstractSimplicialComplex.mem_closedStar / mem_link: membership in the closed star or link, phrased as membership in K plus the local condition.
• PreAbstractSimplicialComplex.mem_closedStar_nonempty / mem_link_nonempty: the introduction-friendly membership forms using only nonemptiness and the defining local data.
• PreAbstractSimplicialComplex.closedStar_sup_deletion: the closed star and the deletion cover K, i.e. closedStar K σ ⊔ deletion K σ = K.
• PreAbstractSimplicialComplex.link_le_deletion_of_nonempty: for a nonempty σ, the link sits inside the deletion.
• PreAbstractSimplicialComplex.closedStar_empty / link_empty / deletion_empty: the values at the empty simplex (K, K, and ⊥), pinning the conventions.
• PreAbstractSimplicialComplex.isCone_closedStar / isCone_deletion: the closed star of a face is a cone with apex any vertex of that face, and deleting a face missing the apex of a cone leaves a cone with the same apex.
• monotonicity of all three constructions in K.

def PreAbstractSimplicialComplex.closedStar {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (σ : Finset ι) : PreAbstractSimplicialComplex ι

The closed star of a simplex σ in K: the faces ρ whose union with σ is a face of K. Equivalently, this is the subcomplex of K generated by faces whose union with σ remains in K.

Equations

• K.closedStar σ = { faces := {ρ : Finset ι | ρ.Nonempty ∧ ρ ∪ σ ∈ K}, isRelLowerSet_faces := ⋯ }

def PreAbstractSimplicialComplex.link {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (σ : Finset ι) : PreAbstractSimplicialComplex ι

The link of a simplex σ in K: the part of the closed star disjoint from σ, i.e. the faces ρ disjoint from σ with ρ ∪ σ a face of K. This is the primitive the combinatorial n-manifold condition is phrased against: the link of every vertex should be a combinatorial sphere or ball.

Equations

• K.link σ = { faces := {ρ : Finset ι | ρ.Nonempty ∧ Disjoint ρ σ ∧ ρ ∪ σ ∈ K}, isRelLowerSet_faces := ⋯ }

def PreAbstractSimplicialComplex.deletion {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (σ : Finset ι) : PreAbstractSimplicialComplex ι

The deletion (or anti-star) of a simplex σ in K: the faces of K that do not contain σ as a subset. Together with the closed star it covers K (closedStar_sup_deletion).

Equations

• K.deletion σ = { faces := {ρ : Finset ι | ρ ∈ K ∧ ¬σ ⊆ ρ}, isRelLowerSet_faces := ⋯ }

theorem PreAbstractSimplicialComplex.mem_closedStar_nonempty {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} : ρ ∈ K.closedStar σ ↔ ρ.Nonempty ∧ ρ ∪ σ ∈ K

A nonempty finset belongs to the closed star exactly when adjoining σ gives a face of K. This is the introduction-friendly form of closed-star membership.

theorem PreAbstractSimplicialComplex.mem_link_nonempty {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} : ρ ∈ K.link σ ↔ ρ.Nonempty ∧ Disjoint ρ σ ∧ ρ ∪ σ ∈ K

A nonempty finset belongs to the link exactly when it is disjoint from σ and adjoining σ gives a face of K. This is the introduction-friendly form of link membership.

theorem PreAbstractSimplicialComplex.notMem_link_of_notMem {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {v : ι} (hv : {v} ∉ K) {w : ι} : {v} ∉ K.link {w}

A fresh vertex of a complex is absent from every vertex link.

@[simp]

theorem PreAbstractSimplicialComplex.mem_deletion {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} : ρ ∈ K.deletion σ ↔ ρ ∈ K ∧ ¬σ ⊆ ρ

@[simp]

theorem PreAbstractSimplicialComplex.mem_closedStar {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} : ρ ∈ K.closedStar σ ↔ ρ ∈ K ∧ ρ ∪ σ ∈ K

A finset ρ belongs to the closed star exactly when ρ is a face of K and adjoining σ still gives a face of K.

@[simp]

theorem PreAbstractSimplicialComplex.mem_link {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} : ρ ∈ K.link σ ↔ ρ ∈ K ∧ Disjoint ρ σ ∧ ρ ∪ σ ∈ K

A finset ρ belongs to the link exactly when ρ is a face of K, is disjoint from σ, and adjoining σ still gives a face of K.

@[simp]

theorem PreAbstractSimplicialComplex.link_link {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} (hστ : Disjoint σ τ) : (K.link σ).link τ = K.link (σ ∪ τ)

Taking the link of τ inside the link of a disjoint face σ is the link of their union.

theorem PreAbstractSimplicialComplex.closedStar_le {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : K.closedStar σ ≤ K

The closed star of σ is a subcomplex of K.

theorem PreAbstractSimplicialComplex.link_le_closedStar {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : K.link σ ≤ K.closedStar σ

The link of σ is a subcomplex of its closed star.

theorem PreAbstractSimplicialComplex.link_le {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : K.link σ ≤ K

The link of σ is a subcomplex of K.

theorem PreAbstractSimplicialComplex.deletion_le {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : K.deletion σ ≤ K

The deletion of σ is a subcomplex of K.

theorem PreAbstractSimplicialComplex.closedStar_sup_deletion {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : K.closedStar σ ⊔ K.deletion σ = K

The closed star and the deletion of σ cover K: every face either survives in the deletion (it does not contain σ) or lies in the closed star (it, hence its union with σ, is a face).

theorem PreAbstractSimplicialComplex.link_le_deletion_of_nonempty {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} (hσ : σ.Nonempty) : K.link σ ≤ K.deletion σ

For a nonempty simplex σ, the link lies inside the deletion: a face disjoint from a nonempty σ cannot contain it.

@[simp]

theorem PreAbstractSimplicialComplex.closedStar_empty {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} : K.closedStar ∅ = K

The closed star at the empty simplex is the whole complex.

@[simp]

theorem PreAbstractSimplicialComplex.link_empty {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} : K.link ∅ = K

The link at the empty simplex is the whole complex.

@[simp]

theorem PreAbstractSimplicialComplex.deletion_empty {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.deletion ∅ = ⊥

The deletion at the empty simplex is empty: every face contains ∅.

theorem PreAbstractSimplicialComplex.closedStar_mono {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {σ : Finset ι} (h : K ≤ L) : K.closedStar σ ≤ L.closedStar σ

The closed star is monotone in the complex.

theorem PreAbstractSimplicialComplex.link_mono {ι : Type u_1} [DecidableEq ι] {K L : PreAbstractSimplicialComplex ι} {σ : Finset ι} (h : K ≤ L) : K.link σ ≤ L.link σ

The link is monotone in the complex.

theorem PreAbstractSimplicialComplex.deletion_mono {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {σ : Finset ι} (h : K ≤ L) : K.deletion σ ≤ L.deletion σ

The deletion is monotone in the complex.

theorem PreAbstractSimplicialComplex.mem_closedStar_iff_sdiff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} (hσ : σ ∈ K) : ρ ∈ K.closedStar σ ↔ ρ.Nonempty ∧ (ρ \ σ = ∅ ∨ ρ \ σ ∈ K.link σ)

A closed-star face is characterized by its nonempty part outside the starred face being a link face. An empty outside part is allowed.

theorem PreAbstractSimplicialComplex.mem_closedStar_inf_deletion_iff_sdiff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ ρ : Finset ι} (hσ : σ ∈ K) : ρ ∈ K.closedStar σ ⊓ K.deletion σ ↔ ρ.Nonempty ∧ ρ ∩ σ ⊂ σ ∧ (ρ \ σ = ∅ ∨ ρ \ σ ∈ K.link σ)

The intersection of the closed star with the deletion consists of faces whose part in σ is proper and whose nonempty part outside σ is in the link.

theorem PreAbstractSimplicialComplex.finite_faces_closedStar_iff {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} : (K.closedStar σ).faces.Finite ↔ (K.link σ).faces.Finite

A closed star has finitely many faces exactly when its link does, for any finset σ.

theorem PreAbstractSimplicialComplex.isCone_closedStar {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (hσ : σ ∈ K) (hv : v ∈ σ) : (K.closedStar σ).IsCone v

The closed star of a face is a cone with apex any vertex of that face: adjoining v ∈ σ to a face ρ of the closed star leaves the defining union ρ ∪ σ unchanged.

theorem PreAbstractSimplicialComplex.isCone_deletion {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {σ : Finset ι} {v : ι} (h : K.IsCone v) (hσ : σ.Nonempty) (hv : v ∉ σ) : (K.deletion σ).IsCone v

Deleting a nonempty face that misses the apex of a cone leaves a cone with the same apex. Note that the deletion of a face containing the apex need not be a cone: deleting {v} itself destroys the apex.