Cones of simplicial complexes

The cone on a simplicial complex K is its join with a single vertex. Its vertex type is α ⊕ PUnit: the left summand contains the original vertices and Sum.inr PUnit.unit is the apex. A face is therefore either an original face, tagged into the left summand, or an original face together with the apex; the apex by itself is also a face.

Cones are elementary infrastructure for layer 11 of the geometric-topology roadmap. Recursive combinatorial balls are obtained by coning combinatorial spheres, and suspensions are formed by iterated coning/gluing. This file supplies the combinatorial operation and its face API, building entirely on the join construction already available in Tau Ceti.

The file also records that the construction satisfies the internal cone condition PreAbstractSimplicialComplex.IsCone at its apex (isCone_cone), which is what identifies the two accounts of a cone.

The construction follows Rourke--Sanderson, Introduction to Piecewise-Linear Topology, Chapter 2. No result from that source is used beyond the standard definition of a cone as a join with a point.

Main definitions

• PreAbstractSimplicialComplex.cone: the cone on a pre-abstract simplicial complex.
• AbstractSimplicialComplex.cone: the cone on an abstract simplicial complex.

Main results

• mem_cone_iff: a face of the cone is nonempty and has either an empty base projection or a face of the original complex as its base projection.
• map_inl_mem_cone: every original face is a face of the cone.
• apex_mem_cone: the apex is a face.
• disjSum_singleton_mem_cone: adjoining the apex to an original face gives a face.
• cone_mono: coning is monotone.
• finite_faces_cone: the cone on a finite complex is finite.
• isCone_cone: the cone construction is a cone with apex the adjoined vertex.

def PreAbstractSimplicialComplex.cone {α : Type u_1} (K : PreAbstractSimplicialComplex α) : PreAbstractSimplicialComplex (α ⊕ PUnit.{u_2 + 1})

The cone on a pre-abstract simplicial complex, defined as its join with the full complex on the one-point type PUnit.

Equations

• K.cone = K.join ⊤

@[simp]

theorem PreAbstractSimplicialComplex.mem_cone_iff {α : Type u_1} {K : PreAbstractSimplicialComplex α} {σ : Finset (α ⊕ PUnit.{u_2 + 1})} : σ ∈ K.cone ↔ σ.Nonempty ∧ (σ.toLeft = ∅ ∨ σ.toLeft ∈ K)

A finite set is a face of the cone exactly when it is nonempty and its left projection is either empty or a face of the base complex. There is no further condition on the right projection because the apex type has one element.

This is a low-priority simp lemma: it normalizes membership of an arbitrary finite set, while the specialized characterizations below still fire first on their own shapes.

@[simp]

theorem PreAbstractSimplicialComplex.map_inl_mem_cone_iff {α : Type u_1} {K : PreAbstractSimplicialComplex α} {s : Finset α} : Finset.map Function.Embedding.inl s ∈ K.cone ↔ s ∈ K

A finite set tagged into the left summand is a face of the cone exactly when it is a face of the base complex.

theorem PreAbstractSimplicialComplex.map_inl_mem_cone {α : Type u_1} {K : PreAbstractSimplicialComplex α} {s : Finset α} (hs : s ∈ K) : Finset.map Function.Embedding.inl s ∈ K.cone

Every face of the base complex, tagged into the left summand, is a face of its cone.

theorem PreAbstractSimplicialComplex.apex_mem_cone {α : Type u_1} {K : PreAbstractSimplicialComplex α} : {Sum.inr PUnit.unit} ∈ K.cone

The cone apex is a face.

@[simp]

theorem PreAbstractSimplicialComplex.disjSum_singleton_mem_cone_iff {α : Type u_1} {K : PreAbstractSimplicialComplex α} {s : Finset α} : s.disjSum {PUnit.unit} ∈ K.cone ↔ s = ∅ ∨ s ∈ K

Adjoining the apex gives a face of the cone exactly when the base is empty or a face of the base complex.

theorem PreAbstractSimplicialComplex.disjSum_singleton_mem_cone {α : Type u_1} {K : PreAbstractSimplicialComplex α} {s : Finset α} (hs : s ∈ K) : s.disjSum {PUnit.unit} ∈ K.cone

Adjoining the apex to a face of the base produces a face of the cone.

theorem PreAbstractSimplicialComplex.cone_mono {α : Type u_1} {K L : PreAbstractSimplicialComplex α} (h : K ≤ L) : K.cone ≤ L.cone

Coning is monotone in the base complex.

theorem PreAbstractSimplicialComplex.finite_faces_cone {α : Type u_1} {K : PreAbstractSimplicialComplex α} (hfin : K.faces.Finite) : K.cone.faces.Finite

The cone on a finite complex is finite: a face of the cone is determined by its two projections (Finset.sumEquiv), the left one is empty or a face of the base, and the apex type is finite.

theorem PreAbstractSimplicialComplex.isCone_cone {α : Type u_1} [DecidableEq α] (K : PreAbstractSimplicialComplex α) : K.cone.IsCone (Sum.inr PUnit.unit)

The cone construction produces a cone in the internal sense, with apex the adjoined vertex. This is what identifies the two accounts of a cone.

def AbstractSimplicialComplex.cone {α : Type u_1} (K : AbstractSimplicialComplex α) : AbstractSimplicialComplex (α ⊕ PUnit.{u_2 + 1})

The cone on an abstract simplicial complex, defined as its join with the full complex on the one-point type PUnit.

Equations

• K.cone = K.join ⊤

@[simp]

theorem AbstractSimplicialComplex.cone_toPreAbstractSimplicialComplex {α : Type u_1} {K : AbstractSimplicialComplex α} : K.cone.toPreAbstractSimplicialComplex = K.cone

Forgetting the singleton-face witness from an abstract cone recovers the cone of the underlying pre-abstract simplicial complex.

@[simp]

theorem AbstractSimplicialComplex.mem_cone_iff {α : Type u_1} {K : AbstractSimplicialComplex α} {σ : Finset (α ⊕ PUnit.{u_2 + 1})} : σ ∈ K.cone ↔ σ.Nonempty ∧ (σ.toLeft = ∅ ∨ σ.toLeft ∈ K)

A finite set is a face of the cone exactly when it is nonempty and its left projection is either empty or a face of the base complex.

This is a low-priority simp lemma: it normalizes membership of an arbitrary finite set, while the specialized characterizations below still fire first on their own shapes.

@[simp]

theorem AbstractSimplicialComplex.map_inl_mem_cone_iff {α : Type u_1} {K : AbstractSimplicialComplex α} {s : Finset α} : Finset.map Function.Embedding.inl s ∈ K.cone ↔ s ∈ K

A finite set tagged into the left summand is a face of the cone exactly when it is a face of the base complex.

theorem AbstractSimplicialComplex.map_inl_mem_cone {α : Type u_1} {K : AbstractSimplicialComplex α} {s : Finset α} (hs : s ∈ K) : Finset.map Function.Embedding.inl s ∈ K.cone

Every face of the base complex, tagged into the left summand, is a face of its cone.

theorem AbstractSimplicialComplex.apex_mem_cone {α : Type u_1} {K : AbstractSimplicialComplex α} : {Sum.inr PUnit.unit} ∈ K.cone

The cone apex is a face.

@[simp]

theorem AbstractSimplicialComplex.disjSum_singleton_mem_cone_iff {α : Type u_1} {K : AbstractSimplicialComplex α} {s : Finset α} : s.disjSum {PUnit.unit} ∈ K.cone ↔ s = ∅ ∨ s ∈ K

Adjoining the apex gives a face of the cone exactly when the base is empty or a face of the base complex.

theorem AbstractSimplicialComplex.disjSum_singleton_mem_cone {α : Type u_1} {K : AbstractSimplicialComplex α} {s : Finset α} (hs : s ∈ K) : s.disjSum {PUnit.unit} ∈ K.cone

Adjoining the apex to a face of the base produces a face of the cone.

theorem AbstractSimplicialComplex.cone_mono {α : Type u_1} {K L : AbstractSimplicialComplex α} (h : K ≤ L) : K.cone ≤ L.cone

Coning is monotone in the base complex.