Elementary collapses of simplicial complexes

An elementary simplicial collapse deletes a free face together with its unique proper coface. This file supplies that local move for PreAbstractSimplicialComplex, Mathlib's type of downward-closed collections of nonempty finite faces. This is the elementary substrate for the collapse track in layer 11 of the geometric-topology roadmap.

Following Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3, the pair (σ, τ) is free when σ is a proper face of τ and every face containing σ is either σ or τ. The usual codimension-one condition is expressed by Mathlib's finset cover relation; uniqueness already suffices to prove that deleting the pair leaves a simplicial complex.

PreAbstractSimplicialComplex is intentional here. Mathlib's AbstractSimplicialComplex ι contains every singleton of the fixed ambient vertex type ι, so deleting a free vertex would leave that type. A collapse changes the used vertex set and therefore naturally lives in the pre-complex type.

Main definitions

• PreAbstractSimplicialComplex.IsFreePair: a face and its unique proper coface.
• PreAbstractSimplicialComplex.ElementaryCollapsesTo: the relation of one elementary collapse.

structure TauCeti.PreAbstractSimplicialComplex.IsFreePair {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) (σ τ : Finset ι) : Prop

A pair (σ, τ) of faces is free when σ is a proper face of τ and τ is the only face other than σ that contains σ.

This formulation includes maximality of τ: applying the last field to a face containing τ forces that face to equal τ.

• lower_mem : σ ∈ K

  The lower face belongs to the complex.

• upper_mem : τ ∈ K

  The upper face belongs to the complex.

• lower_ssubset_upper : σ ⊂ τ

  The lower face is properly contained in the upper face.

• eq_lower_or_eq_upper ⦃ω : Finset ι⦄ : ω ∈ K → σ ⊆ ω → ω = σ ∨ ω = τ

  These are the only faces of the complex containing the lower face.

theorem TauCeti.PreAbstractSimplicialComplex.IsFreePair.upper_maximal {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} (h : IsFreePair K σ τ) {ω : Finset ι} (hω : ω ∈ K) (hτω : τ ⊆ ω) : ω = τ

The upper face of a free pair is maximal in the complex.

theorem TauCeti.PreAbstractSimplicialComplex.IsFreePair.covBy {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} (h : IsFreePair K σ τ) : σ ⋖ τ

The lower face of a free pair has codimension one in the upper face.

theorem TauCeti.PreAbstractSimplicialComplex.mem_deletion_of_isFreePair {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) {σ τ ω : Finset ι} (h : IsFreePair K σ τ) : ω ∈ K ∧ ¬σ ⊆ ω ↔ ω ∈ K ∧ ω ≠ σ ∧ ω ≠ τ

Deleting the lower face of a free pair retains exactly the original faces other than the lower and upper faces.

def TauCeti.PreAbstractSimplicialComplex.ElementaryCollapsesTo {ι : Type u_1} (K L : PreAbstractSimplicialComplex ι) : Prop

One complex elementarily collapses to another when the latter is obtained by deleting a free pair.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.PreAbstractSimplicialComplex.ElementaryCollapsesTo.of_isFreePair {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {σ τ : Finset ι} (hfree : IsFreePair K σ τ) (hL : L = deletion K σ) : ElementaryCollapsesTo K L

A free pair determines an elementary collapse to its deletion.

theorem TauCeti.PreAbstractSimplicialComplex.ElementaryCollapsesTo.le {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : ElementaryCollapsesTo K L) : L ≤ K

An elementary collapse produces a subcomplex.

theorem TauCeti.PreAbstractSimplicialComplex.ElementaryCollapsesTo.lt {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : ElementaryCollapsesTo K L) : L < K

An elementary collapse is strict: its lower free face is lost.

theorem TauCeti.PreAbstractSimplicialComplex.ElementaryCollapsesTo.exists_pair {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : ElementaryCollapsesTo K L) : ∃ (σ : Finset ι) (τ : Finset ι) (_ : IsFreePair K σ τ), σ ⋖ τ ∧ ∀ (ω : Finset ι), ω ∈ L ↔ ω ∈ K ∧ ω ≠ σ ∧ ω ≠ τ

Membership in the result of an elementary collapse is membership in the original complex away from the selected free pair.