Complexes that are cones

A simplicial complex is a cone with apex v when v is one of its vertices and adjoining v to a face gives a face again. This file carries that condition as the predicate IsCone K v, stated for an apex v of the vertex type of K itself, so that a complex can be recognised as a cone without changing its vertex type.

The predicate sits upstream of every construction that satisfies it, so that each construction records its own recognition lemma in its own file: isCone_simplex for an abstract simplex (TauCeti.AlgebraicTopology.SimplicialComplex.Simplex.Basic), isCone_closedStar for the closed star of a face and isCone_deletion for the deletion of a face missing the apex (TauCeti.AlgebraicTopology.SimplicialComplex.LinkStar), and isCone_cone for the cone construction (TauCeti.AlgebraicTopology.SimplicialComplex.Cone), which is what identifies the two accounts of a cone. The point of the predicate is the basic collapsing theorem of piecewise-linear topology, that a finite cone collapses to its apex (TauCeti.AlgebraicTopology.SimplicialComplex.Collapse.Cone).

Main definitions

• PreAbstractSimplicialComplex.IsCone: a complex is a cone with a given apex.

structure PreAbstractSimplicialComplex.IsCone {ι : Type u_1} [DecidableEq ι] (K : PreAbstractSimplicialComplex ι) (v : ι) : Prop

K is a cone with apex v when v is a vertex of K and adjoining v to a face of K again gives a face of K.

This is the internal form of the cone condition: the apex is a vertex of the ambient type of K itself, so a complex can be recognised as a cone without changing its vertex type. The cone construction satisfies it at its apex (isCone_cone).

• apex_mem : {v} ∈ K

  The apex is a vertex of the complex.

• insert_mem ⦃σ : Finset ι⦄ : σ ∈ K → insert v σ ∈ K

  Adjoining the apex to a face gives a face.

theorem PreAbstractSimplicialComplex.IsCone.ne_bot {ι : Type u_1} [DecidableEq ι] {v : ι} {K : PreAbstractSimplicialComplex ι} (h : K.IsCone v) : K ≠ ⊥

A cone with apex v is nonempty.