Abstract simplices and their boundaries

This file defines the abstract simplex spanned by a finite set of vertices and its boundary. Both are PreAbstractSimplicialComplexes on the original ambient vertex type: this lets the construction remember exactly which vertices occur, unlike AbstractSimplicialComplex, which must contain every singleton of its ambient type.

The boundary consists of the nonempty proper subsets of the spanning vertex set. These constructions provide the standard models needed for the recursive definitions of combinatorial spheres and balls in layer 11 of the geometric-topology roadmap.

The definitions follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2.

Main definitions

• PreAbstractSimplicialComplex.simplex: the complex of nonempty subsets of a finite vertex set.
• PreAbstractSimplicialComplex.simplexBoundary: its proper faces.

def TauCeti.PreAbstractSimplicialComplex.simplex {ι : Type u_1} (V : Finset ι) : PreAbstractSimplicialComplex ι

The abstract simplex spanned by V: its faces are the nonempty subsets of V.

Equations

• TauCeti.PreAbstractSimplicialComplex.simplex V = { faces := {σ : Finset ι | σ.Nonempty ∧ σ ⊆ V}, isRelLowerSet_faces := ⋯ }

def TauCeti.PreAbstractSimplicialComplex.simplexBoundary {ι : Type u_1} (V : Finset ι) : PreAbstractSimplicialComplex ι

The boundary of the abstract simplex spanned by V: its faces are the nonempty proper subsets of V.

Equations

• TauCeti.PreAbstractSimplicialComplex.simplexBoundary V = { faces := {σ : Finset ι | σ.Nonempty ∧ σ ⊂ V}, isRelLowerSet_faces := ⋯ }

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.mem_simplex {ι : Type u_1} {V σ : Finset ι} : σ ∈ simplex V ↔ σ.Nonempty ∧ σ ⊆ V

A finite set is a face of a simplex exactly when it is nonempty and contained in the spanning vertex set.

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.mem_simplexBoundary {ι : Type u_1} {V σ : Finset ι} : σ ∈ simplexBoundary V ↔ σ.Nonempty ∧ σ ⊂ V

A finite set is a face of a simplex boundary exactly when it is a nonempty proper subset of the spanning vertex set.

theorem TauCeti.PreAbstractSimplicialComplex.self_mem_simplex {ι : Type u_1} {V : Finset ι} : V ∈ simplex V ↔ V.Nonempty

The spanning vertex set is a face of its simplex exactly when it is nonempty.

theorem TauCeti.PreAbstractSimplicialComplex.self_notMem_simplexBoundary {ι : Type u_1} {V : Finset ι} : V ∉ simplexBoundary V

The spanning vertex set is not a face of its own boundary.

theorem TauCeti.PreAbstractSimplicialComplex.singleton_mem_simplex {ι : Type u_1} {V : Finset ι} {v : ι} : {v} ∈ simplex V ↔ v ∈ V

A vertex belongs to the spanning set exactly when its singleton is a face of the simplex.

theorem TauCeti.PreAbstractSimplicialComplex.singleton_mem_simplexBoundary {ι : Type u_1} {V : Finset ι} {v : ι} : {v} ∈ simplexBoundary V ↔ v ∈ V ∧ V ≠ {v}

A singleton is a boundary face exactly when its vertex belongs to a spanning set containing at least one other vertex.

theorem TauCeti.PreAbstractSimplicialComplex.simplexBoundary_le_simplex {ι : Type u_1} {V : Finset ι} : simplexBoundary V ≤ simplex V

The boundary is a subcomplex of the simplex.

theorem TauCeti.PreAbstractSimplicialComplex.simplexBoundary_lt_simplex {ι : Type u_1} {V : Finset ι} (hV : V.Nonempty) : simplexBoundary V < simplex V

The boundary of a simplex with nonempty spanning set is a strict subcomplex of the simplex.

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.simplex_empty {ι : Type u_1} : simplex ∅ = ⊥

The simplex on the empty spanning set has no faces.

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.simplexBoundary_empty {ι : Type u_1} : simplexBoundary ∅ = ⊥

The boundary of the empty simplex has no faces.

@[simp]

theorem TauCeti.PreAbstractSimplicialComplex.simplexBoundary_singleton {ι : Type u_1} (v : ι) : simplexBoundary {v} = ⊥

The boundary of a one-vertex simplex is empty.

theorem TauCeti.PreAbstractSimplicialComplex.simplex_le_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {V : Finset ι} : simplex V ≤ K ↔ V.Nonempty → V ∈ K

The simplex on V is contained in a complex exactly when V is a face of the complex whenever V is nonempty. For V = ∅ the simplex is ⊥, so it is contained in every complex.

theorem TauCeti.PreAbstractSimplicialComplex.simplex_le_simplex_iff {ι : Type u_1} {V W : Finset ι} : simplex V ≤ simplex W ↔ V ⊆ W

Simplices are ordered exactly when their spanning vertex sets are ordered.

theorem TauCeti.PreAbstractSimplicialComplex.simplex_mono {ι : Type u_1} {V W : Finset ι} (h : V ⊆ W) : simplex V ≤ simplex W

Enlarging the spanning vertex set enlarges the simplex.

theorem TauCeti.PreAbstractSimplicialComplex.simplexBoundary_mono {ι : Type u_1} {V W : Finset ι} (h : V ⊆ W) : simplexBoundary V ≤ simplexBoundary W

Enlarging the spanning vertex set enlarges the boundary.

theorem TauCeti.PreAbstractSimplicialComplex.mem_simplexBoundary_iff_mem_simplex_ne {ι : Type u_1} {V σ : Finset ι} : σ ∈ simplexBoundary V ↔ σ ∈ simplex V ∧ σ ≠ V

A face of a simplex lies in its boundary exactly when it is not the whole spanning set.

theorem TauCeti.PreAbstractSimplicialComplex.mem_simplex_iff_mem_simplexBoundary_or_eq {ι : Type u_1} {V σ : Finset ι} : σ ∈ simplex V ↔ σ ∈ simplexBoundary V ∨ V.Nonempty ∧ σ = V

The faces of a simplex are its boundary faces together with the spanning set itself, the latter only when the spanning set is nonempty.