Documentation

TauCeti.AlgebraicTopology.SimplicialComplex.Zeeman

Contractible two-dimensional simplicial complexes #

This file supplies the predicate used in the statement of Zeeman's collapsibility conjecture. An abstract simplicial complex is a contractible 2-complex when it has finitely many faces, dimension at most two, and contractible geometric realization. The finiteness condition records the finite complexes considered by simplicial collapse, while the dimension bound is expressed using the intrinsic dimension from Dimension rather than a bound on the ambient vertex type.

The standard one-simplex is provided as a nontrivial witness. Its realization is contractible by the homeomorphism with Mathlib's convex standard simplex, so the predicate is exercised without assuming the desired Zeeman conclusion.

The universe-polymorphic proposition TauCeti.ZeemanConjecture asserts that the ordered simplicial cylinder is collapsible for every finite contractible complex of dimension at most two. The conjecture remains open; the full simplex on a finite linearly ordered type with a greatest element supplies a family where its conclusion follows from the cylinder's cone structure.

Main definitions #

Main results #

The proposition is stated, not proved.

source
def AbstractSimplicialComplex.Contractible2Complex {ι : Type u_1} (K : AbstractSimplicialComplex ι) :
Prop

A finite abstract simplicial complex of dimension at most two whose realization is contractible. This is the class of complexes occurring in Zeeman's conjecture, as stated in R. Kirby (ed.), Problems in Low-Dimensional Topology, Problem 5.2 (1997), following E. C. Zeeman, On the dunce hat, Topology 2 (1964), 341--358.

Equations
Instances For
    source
    theorem AbstractSimplicialComplex.contractible2Complex_iff {ι : Type u_1} {K : AbstractSimplicialComplex ι} :
    K.Contractible2Complex ↔ K.faces.Finite ∧ K.dimension ≤ 2 ∧ ContractibleSpace K.Realization

    The defining finiteness, dimension, and contractibility conditions for a contractible 2-complex.

    source
    theorem AbstractSimplicialComplex.Contractible2Complex.finite_faces {ι : Type u_1} {K : AbstractSimplicialComplex ι} (hK : K.Contractible2Complex) :
    K.faces.Finite

    A contractible 2-complex has finitely many faces.

    source
    theorem AbstractSimplicialComplex.Contractible2Complex.dimension_le_two {ι : Type u_1} {K : AbstractSimplicialComplex ι} (hK : K.Contractible2Complex) :
    K.dimension ≤ 2

    A contractible 2-complex has dimension at most two.

    source
    theorem AbstractSimplicialComplex.Contractible2Complex.contractibleSpace {ι : Type u_1} {K : AbstractSimplicialComplex ι} (hK : K.Contractible2Complex) :
    ContractibleSpace K.Realization

    The realization of a contractible 2-complex is contractible.

    source
    theorem AbstractSimplicialComplex.contractible2Complex_standardOneSimplex :
    ⊤.Contractible2Complex

    The standard one-simplex gives a concrete non-void witness for the ≤ 2 dimension bound.

    source
    def TauCeti.ZeemanConjecture :
    Prop

    Zeeman's conjecture: the ordered simplicial cylinder on every finite contractible complex of dimension at most two is collapsible.

    The cylinder uses the staircase triangulation fixed by AbstractSimplicialComplex.orderedCylinder. Its collapse is taken after forgetting to a pre-abstract simplicial complex, since collapse can remove vertices.

    Equations
    Instances For
      source
      theorem TauCeti.ZeemanConjecture.collapsible_orderedCylinder {ι : Type u} [LinearOrder ι] (h : ZeemanConjecture) (K : AbstractSimplicialComplex ι) (hK : K.Contractible2Complex) :
      K.orderedCylinder.Collapsible

      A proof of Zeeman's conjecture makes the ordered cylinder on any contractible two-complex collapsible.

      source
      theorem TauCeti.zeemanConjecture_iff :
      ZeemanConjecture ↔ ∀ (ι : Type u) [inst : LinearOrder ι] (K : AbstractSimplicialComplex ι), K.Contractible2Complex → K.orderedCylinder.Collapsible

      The defining characterization of Zeeman's conjecture.