A finite cone collapses to its apex #

A simplicial complex is a cone with apex v when v is one of its vertices and adjoining v to any face gives a face again. The basic collapsing theorem of piecewise-linear topology (Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3) says that a finite cone collapses to its apex; in particular every finite cone is collapsible.

This file proves that theorem for the collapse relation of PreAbstractSimplicialComplex.CollapsesTo, and reads it off for the standard cones: an abstract simplex, the closed star of a face, and the cone construction PreAbstractSimplicialComplex.cone. Before this, Collapsible was known only for the one-vertex complexes of Collapsible.point; these theorems supply collapsible complexes of arbitrarily many faces, and the simplex case is the base of the recursion on combinatorial balls in layer 11 of the geometric-topology roadmap (TauCetiRoadmap/GeometricTopology/README.md).

The cone predicate IsCone lives in TauCeti.AlgebraicTopology.SimplicialComplex.IsCone, and each standard cone is recognised in the file of its own construction (isCone_simplex, isCone_closedStar, isCone_cone, isCone_stellarSubdivision_of_closedStar_eq_self); this file adds only what depends on collapse theory.

The proof is the usual one: pick a face σ maximal among the faces missing the apex. Maximality makes σ a free face with unique proper coface insert v σ, deleting it leaves a smaller cone with the same apex, and the face count of Collapse.FaceCount provides the termination measure.

Main results #

PreAbstractSimplicialComplex.IsCone.collapsesTo_point: a finite cone collapses to its apex.
PreAbstractSimplicialComplex.IsCone.collapsible: a finite cone is collapsible.
PreAbstractSimplicialComplex.collapsesTo_point_simplex: an abstract simplex collapses to any of its vertices.
PreAbstractSimplicialComplex.collapsesTo_point_closedStar: a finite closed star of a face collapses to any vertex of that face.
PreAbstractSimplicialComplex.collapsesTo_point_cone: the cone on a finite complex collapses to its apex.
PreAbstractSimplicialComplex.collapsible_stellarSubdivision_of_closedStar_eq_self: a finite stellar subdivision that is a cone is collapsible.

source

theorem PreAbstractSimplicialComplex.IsCone.exists_notMem_of_ne_point {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) (hne : K ≠ point v) :

∃ σ ∈ K, v ∉ σ

A cone with apex v that is not the one-vertex complex at v has a face missing v.

source

theorem PreAbstractSimplicialComplex.IsCone.collapsesTo_point {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) (hfin : K.faces.Finite) :

K.CollapsesTo (point v)

A finite cone collapses to its apex (Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 3).

source

theorem PreAbstractSimplicialComplex.IsCone.collapsible {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {v : ι} (h : K.IsCone v) (hfin : K.faces.Finite) :

K.Collapsible

A finite cone is collapsible.

source

theorem PreAbstractSimplicialComplex.collapsible_stellarSubdivision_of_closedStar_eq_self {ι : Type u_1} [DecidableEq ι] {K : PreAbstractSimplicialComplex ι} {v : ι} {σ : Finset ι} (hfin : K.faces.Finite) (hσ : σ ∈ K) (hstar : K.closedStar σ = K) :

(K.stellarSubdivision σ v).Collapsible

A finite stellar subdivision is collapsible when the original complex is its own closed star at the starred face.

source

theorem PreAbstractSimplicialComplex.collapsible_stellarSubdivision_simplex_self {ι : Type u_1} [DecidableEq ι] {v : ι} {V : Finset ι} (hV : V.Nonempty) :

((simplex V).stellarSubdivision V v).Collapsible

A simplex starred at its whole vertex set is collapsible.

source

theorem PreAbstractSimplicialComplex.collapsesTo_point_simplex {ι : Type u_1} {v : ι} {V : Finset ι} (hv : v ∈ V) :

(simplex V).CollapsesTo (point v)

An abstract simplex collapses to any of its vertices.

source

theorem PreAbstractSimplicialComplex.collapsible_simplex {ι : Type u_1} {V : Finset ι} (hV : V.Nonempty) :

(simplex V).Collapsible

An abstract simplex on a nonempty spanning set is collapsible. Its face count grows with the spanning set, so this exhibits collapsible complexes with arbitrarily many faces, beyond the one-vertex complexes of Collapsible.point.

source