Simplicial collapse

This file passes from the local elementary-collapse move to finite simplicial collapses. A complex K collapses to L when there is a finite, possibly empty, sequence of elementary collapses from K to L; it is collapsible when the endpoint can be a one-vertex complex. These are the collapse notions used in layer 11 of the geometric-topology roadmap and in the statement of Zeeman's conjecture.

As in ElementaryCollapse, the definitions use PreAbstractSimplicialComplex: collapsing a free vertex changes the set of vertices actually used by a complex. The definitions follow Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3.

Main definitions

• PreAbstractSimplicialComplex.point: the complex whose only face is a given vertex.
• PreAbstractSimplicialComplex.CollapsesTo: the reflexive transitive closure of elementary collapse.
• PreAbstractSimplicialComplex.Collapsible: collapse to a one-vertex complex.

def PreAbstractSimplicialComplex.point {ι : Type u_1} (v : ι) : PreAbstractSimplicialComplex ι

The one-vertex complex at v. Its unique face is {v}.

Equations

• PreAbstractSimplicialComplex.point v = { faces := {{v}}, isRelLowerSet_faces := ⋯ }

@[simp]

theorem PreAbstractSimplicialComplex.mem_point {ι : Type u_1} {v : ι} {σ : Finset ι} : σ ∈ point v ↔ σ = {v}

theorem PreAbstractSimplicialComplex.singleton_mem_point {ι : Type u_1} {v w : ι} : {w} ∈ point v ↔ w = v

A singleton is a face of point v exactly when it is the singleton at v.

theorem PreAbstractSimplicialComplex.point_le_iff {ι : Type u_1} {v : ι} {K : PreAbstractSimplicialComplex ι} : point v ≤ K ↔ {v} ∈ K

The one-vertex complex at v is a subcomplex of K exactly when {v} is a face of K.

theorem PreAbstractSimplicialComplex.point_ne_bot {ι : Type u_1} (v : ι) : point v ≠ ⊥

The one-vertex complex at v is nonempty.

@[simp]

theorem PreAbstractSimplicialComplex.point_inj {ι : Type u_1} {v w : ι} : point v = point w ↔ v = w

Two one-vertex complexes are equal exactly when their vertices are equal.

@[simp]

theorem PreAbstractSimplicialComplex.simplex_singleton {ι : Type u_1} (v : ι) : simplex {v} = point v

The abstract simplex spanned by a single vertex is the one-vertex complex at that vertex.

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

K collapses to L when a finite, possibly empty, sequence of elementary collapses takes K to L.

Equations

• K.CollapsesTo L = Relation.ReflTransGen PreAbstractSimplicialComplex.ElementaryCollapsesTo K L

theorem PreAbstractSimplicialComplex.CollapsesTo.refl {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) : K.CollapsesTo K

Every complex collapses to itself by the empty sequence.

theorem PreAbstractSimplicialComplex.CollapsesTo.single {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.ElementaryCollapsesTo L) : K.CollapsesTo L

An elementary collapse is a collapse of length one.

theorem PreAbstractSimplicialComplex.CollapsesTo.trans {ι : Type u_1} {K L P : PreAbstractSimplicialComplex ι} (hKL : K.CollapsesTo L) (hLP : L.CollapsesTo P) : K.CollapsesTo P

Collapse is transitive by concatenating finite collapse sequences.

theorem PreAbstractSimplicialComplex.CollapsesTo.head {ι : Type u_1} {K L P : PreAbstractSimplicialComplex ι} (hKL : K.ElementaryCollapsesTo L) (hLP : L.CollapsesTo P) : K.CollapsesTo P

Prepending an elementary collapse to a collapse sequence gives a collapse.

theorem PreAbstractSimplicialComplex.CollapsesTo.tail {ι : Type u_1} {K L P : PreAbstractSimplicialComplex ι} (hKL : K.CollapsesTo L) (hLP : L.ElementaryCollapsesTo P) : K.CollapsesTo P

Appending an elementary collapse to a collapse sequence gives a collapse.

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

The endpoint of a collapse is a subcomplex of its starting complex.

theorem PreAbstractSimplicialComplex.CollapsesTo.eq_of_le {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) (hKL : K ≤ L) : K = L

If K collapses to a complex L that contains K, then K and L are equal.

theorem PreAbstractSimplicialComplex.CollapsesTo.antisymm {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (hKL : K.CollapsesTo L) (hLK : L.CollapsesTo K) : K = L

A collapse between comparable complexes is equality when the order points both ways.

theorem PreAbstractSimplicialComplex.CollapsesTo.eq_or_exists_head {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) : K = L ∨ ∃ (P : PreAbstractSimplicialComplex ι), K.ElementaryCollapsesTo P ∧ P.CollapsesTo L

A nontrivial collapse sequence contains a first elementary collapse.

theorem PreAbstractSimplicialComplex.CollapsesTo.lt {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (h : K.CollapsesTo L) (hne : K ≠ L) : L < K

A nontrivial collapse strictly decreases the complex.

theorem PreAbstractSimplicialComplex.CollapsesTo.property_of_antitone {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {p : PreAbstractSimplicialComplex ι → Prop} (hp : ∀ ⦃A B : PreAbstractSimplicialComplex ι⦄, A ≤ B → p B → p A) (h : K.CollapsesTo L) (hK : p K) : p L

A collapse preserves any property that is inherited by subcomplexes.

theorem PreAbstractSimplicialComplex.CollapsesTo.property_of_elementaryCollapsesTo {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} {p : PreAbstractSimplicialComplex ι → Prop} (hp : ∀ ⦃A B : PreAbstractSimplicialComplex ι⦄, A.ElementaryCollapsesTo B → p A → p B) (h : K.CollapsesTo L) (hK : p K) : p L

A property preserved by each elementary collapse is preserved by a collapse sequence.

def PreAbstractSimplicialComplex.Collapsible {ι : Type u_1} (K : PreAbstractSimplicialComplex ι) : Prop

A simplicial complex is collapsible when it collapses to a one-vertex complex.

Equations

• K.Collapsible = ∃ (v : ι), K.CollapsesTo (PreAbstractSimplicialComplex.point v)

theorem PreAbstractSimplicialComplex.collapsible_iff {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} : K.Collapsible ↔ ∃ (v : ι), K.CollapsesTo (point v)

A complex is collapsible exactly when it admits a collapse sequence to some one-vertex complex.

theorem PreAbstractSimplicialComplex.Collapsible.point {ι : Type u_1} (v : ι) : (PreAbstractSimplicialComplex.point v).Collapsible

A one-vertex complex is collapsible, using the empty collapse sequence.

theorem PreAbstractSimplicialComplex.Collapsible.of_collapsesTo {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (hKL : K.CollapsesTo L) (hL : L.Collapsible) : K.Collapsible

If K collapses to a collapsible complex, then K is collapsible.

theorem PreAbstractSimplicialComplex.Collapsible.of_elementaryCollapsesTo {ι : Type u_1} {K L : PreAbstractSimplicialComplex ι} (hKL : K.ElementaryCollapsesTo L) (hL : L.Collapsible) : K.Collapsible

If K elementarily collapses to a collapsible complex, then K is collapsible.

theorem PreAbstractSimplicialComplex.Collapsible.ne_bot {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} (h : K.Collapsible) : K ≠ ⊥

A collapsible complex is nonempty.

theorem PreAbstractSimplicialComplex.Collapsible.exists_vertex {ι : Type u_1} {K : PreAbstractSimplicialComplex ι} (h : K.Collapsible) : ∃ (v : ι), {v} ∈ K

A collapsible complex contains its terminal vertex as a face.