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.
• AbstractSimplicialComplex.standardSuccSimplexBoundary: the boundary complex of the standard (n + 1)-simplex.

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

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

Equations

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

def 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

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

@[simp]

theorem 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 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 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 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 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 PreAbstractSimplicialComplex.finite_faces_simplex {ι : Type u_1} (V : Finset ι) : (simplex V).faces.Finite

An abstract simplex has finitely many faces: they are subsets of the spanning set.

theorem PreAbstractSimplicialComplex.isCone_simplex {ι : Type u_1} {V : Finset ι} [DecidableEq ι] {v : ι} (hv : v ∈ V) : (simplex V).IsCone v

An abstract simplex is a cone with apex any of its vertices.

theorem 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 PreAbstractSimplicialComplex.simplexBoundary_le_simplex {ι : Type u_1} {V : Finset ι} : simplexBoundary V ≤ simplex V

The boundary is a subcomplex of the simplex.

theorem PreAbstractSimplicialComplex.finite_faces_simplexBoundary {ι : Type u_1} (V : Finset ι) : (simplexBoundary V).faces.Finite

The boundary of an abstract simplex has finitely many faces.

theorem 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 PreAbstractSimplicialComplex.simplex_empty {ι : Type u_1} : simplex ∅ = ⊥

The simplex on the empty spanning set has no faces.

@[simp]

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

The boundary of the empty simplex has no faces.

@[simp]

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

The boundary of a one-vertex simplex is empty.

@[simp]

theorem PreAbstractSimplicialComplex.simplex_univ {ι : Type u_1} [Fintype ι] : simplex Finset.univ = ⊤

The simplex on all vertices is the top pre-abstract simplicial complex.

@[simp]

theorem PreAbstractSimplicialComplex.simplexBoundary_univ_fin_two : simplexBoundary Finset.univ = ⊥.toPreAbstractSimplicialComplex

The boundary of the standard one-simplex consists of its two vertices. Equivalently, it is the underlying precomplex of the bottom abstract simplicial complex on Fin 2.

theorem 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 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 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 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 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 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.

def AbstractSimplicialComplex.standardSuccSimplexBoundary (n : ℕ) : AbstractSimplicialComplex (Fin (n + 2))

The boundary complex of the standard (n + 1)-simplex. Its vertices are Fin (n + 2) and its faces are the nonempty proper subsets of all vertices.

Equations

• AbstractSimplicialComplex.standardSuccSimplexBoundary n = PreAbstractSimplicialComplex.toAbstractSimplicialComplex (Fin (n + 2)) (PreAbstractSimplicialComplex.simplexBoundary Finset.univ) ⋯

@[simp]

theorem AbstractSimplicialComplex.standardSuccSimplexBoundary_toPreAbstractSimplicialComplex (n : ℕ) : (standardSuccSimplexBoundary n).toPreAbstractSimplicialComplex = PreAbstractSimplicialComplex.simplexBoundary Finset.univ

The underlying precomplex of standardSuccSimplexBoundary n is the boundary of the simplex on all n + 2 vertices.

@[simp]

theorem AbstractSimplicialComplex.mem_standardSuccSimplexBoundary_iff {n : ℕ} {σ : Finset (Fin (n + 2))} : σ ∈ standardSuccSimplexBoundary n ↔ σ.Nonempty ∧ σ ⊂ Finset.univ

The faces of the boundary of the standard (n + 1)-simplex are exactly the nonempty proper subsets of its vertex set.