Collapsing ordered simplicial cylinders

If a complex is a cone whose apex is the greatest vertex, then its ordered cylinder is again a cone: its apex is the pair of the original apex with the terminal interval vertex. Consequently a finite such cylinder collapses to that apex. In particular this applies to the full simplex, supplying a first nontrivial family for which the conclusion of Zeeman's conjecture holds and checking that the ordered-product convention and the collapse API fit together.

The ordered cylinder is the staircase triangulation from TauCeti.AlgebraicTopology.SimplicialComplex.Product; collapse and the theorem that finite cones collapse are from TauCeti.AlgebraicTopology.SimplicialComplex.Collapse.Cone. The argument is the standard observation that every vertex of a full ordered simplex lies below its greatest vertex.

Main results

• AbstractSimplicialComplex.collapsesTo_point_orderedCylinder_of_isCone: a finite cone's ordered cylinder collapses to its terminal apex.
• AbstractSimplicialComplex.collapsible_orderedCylinder_of_isCone: a finite cone's ordered cylinder is collapsible.
• AbstractSimplicialComplex.collapsesTo_point_orderedCylinder_top: a finite such cylinder collapses to its greatest terminal vertex.
• AbstractSimplicialComplex.collapsible_orderedCylinder_top: a finite such cylinder is collapsible.

theorem AbstractSimplicialComplex.collapsesTo_point_orderedCylinder_of_isCone {ι : Type u_1} [LinearOrder ι] {v : ι} {K : AbstractSimplicialComplex ι} (hfin : K.faces.Finite) (hK : K.IsCone v) (hv : ∀ (w : ι), {w} ∈ K → w ≤ v) : K.orderedCylinder.CollapsesTo (PreAbstractSimplicialComplex.point (v, 1))

The ordered cylinder of a finite cone whose apex bounds every vertex collapses to the corresponding terminal apex.

theorem AbstractSimplicialComplex.collapsible_orderedCylinder_of_isCone {ι : Type u_1} [LinearOrder ι] {v : ι} {K : AbstractSimplicialComplex ι} (hfin : K.faces.Finite) (hK : K.IsCone v) (hv : ∀ (w : ι), {w} ∈ K → w ≤ v) : K.orderedCylinder.Collapsible

The ordered cylinder of a finite cone whose apex bounds every vertex is collapsible.

theorem AbstractSimplicialComplex.collapsesTo_point_orderedCylinder_top {ι : Type u_1} [LinearOrder ι] [OrderTop ι] [Finite ι] : ⊤.orderedCylinder.CollapsesTo (PreAbstractSimplicialComplex.point (⊤, 1))

The ordered cylinder of a full simplex on a finite vertex type collapses to its greatest vertex at the terminal endpoint.

theorem AbstractSimplicialComplex.collapsible_orderedCylinder_top {ι : Type u_1} [LinearOrder ι] [OrderTop ι] [Finite ι] : ⊤.orderedCylinder.Collapsible

The ordered cylinder of a full simplex on a finite vertex type is collapsible.