Cells of an abstract simplicial complex

An n-cell of an abstract simplicial complex is a face with n + 1 vertices. For a linearly ordered vertex type, every cell has a canonical increasing enumeration. This file also defines the codimension-one cell obtained by deleting an enumerated vertex and proves the semisimplicial face identity. The codimension-one cells are classified by the vertex deleted from the original face. Finally, a cell whose vertices all precede a vertex v, and to which v can be adjoined, has a cone with v as its last vertex; its faces are the original cell and the cones on the faces of the original cell.

Main definitions

• AbstractSimplicialComplex.RealizationCell: the faces with a prescribed dimension.
• AbstractSimplicialComplex.RealizationCell.vertexEmbedding: the increasing vertex enumeration.
• AbstractSimplicialComplex.RealizationCell.face: deletion of one enumerated vertex.
• AbstractSimplicialComplex.RealizationCell.vertex: the 0-cell of a vertex.
• AbstractSimplicialComplex.RealizationCell.cone: the cone on a cell with a later vertex.

@[reducible, inline]

abbrev AbstractSimplicialComplex.RealizationCell {ι : Type u_1} (K : AbstractSimplicialComplex ι) (n : ℕ) : Type u_1

The n-dimensional cells of K: its faces with n + 1 vertices.

def AbstractSimplicialComplex.RealizationCell.vertex {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : K.RealizationCell 0

The 0-cell of K whose only vertex is v.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.vertex_val {ι : Type u_1} (K : AbstractSimplicialComplex ι) (v : ι) : ↑↑(vertex K v) = {v}

The vertex set of the 0-cell of a vertex is that vertex.

def AbstractSimplicialComplex.RealizationCell.vertexEmbedding {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : Fin (n + 1) ↪ ι

The increasing enumeration of the vertices of a simplicial cell.

theorem AbstractSimplicialComplex.RealizationCell.strictMono_vertexEmbedding {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : StrictMono ⇑c.vertexEmbedding

The chosen vertex enumeration is strictly increasing.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.vertexEmbedding_mem {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) (i : Fin (n + 1)) : c.vertexEmbedding i ∈ ↑↑c

Every enumerated vertex belongs to the cell's face.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.image_vertexEmbedding {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) : Finset.image (⇑c.vertexEmbedding) Finset.univ = ↑↑c

The increasing enumeration has the cell's face as its image.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.vertexEmbedding_vertex {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (v : ι) (i : Fin 1) : (vertex K v).vertexEmbedding i = v

The only enumerated vertex of the 0-cell of a vertex is that vertex.

theorem AbstractSimplicialComplex.RealizationCell.eq_vertex {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (c : K.RealizationCell 0) : c = vertex K (c.vertexEmbedding 0)

Every 0-cell is the 0-cell of its only vertex.

def AbstractSimplicialComplex.RealizationCell.face {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) : K.RealizationCell n

The codimension-one face obtained by deleting the j-th vertex in the increasing enumeration of a simplicial cell.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.face_val {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) : ↑↑(c.face j) = (↑↑c).erase (c.vertexEmbedding j)

The finite set underlying a deleted-vertex face is obtained by erasing that vertex.

theorem AbstractSimplicialComplex.RealizationCell.face_injective {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) : Function.Injective c.face

The codimension-one faces obtained by deleting vertices are pairwise distinct.

theorem AbstractSimplicialComplex.RealizationCell.exists_subset_face_iff_ssubset {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (s : Finset ι) : (∃ (j : Fin (n + 2)), s ⊆ ↑↑(c.face j)) ↔ s ⊂ ↑↑c

A finite set lies in a codimension-one face exactly when it is a proper subset of the original face.

theorem AbstractSimplicialComplex.RealizationCell.exists_face_eq_iff_subset {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (d : K.RealizationCell n) : (∃ (j : Fin (n + 2)), c.face j = d) ↔ ↑↑d ⊆ ↑↑c

The codimension-one cells of a cell are exactly its subfaces of the appropriate dimension.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.vertexEmbedding_face {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) : ⇑(c.face j).vertexEmbedding = ⇑c.vertexEmbedding ∘ j.succAbove

The increasing enumeration of a deleted-vertex face skips exactly the deleted position.

theorem AbstractSimplicialComplex.RealizationCell.face_face {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 2)) (i : Fin (n + 3)) (j : Fin (n + 2)) : (c.face i).face j = (c.face (i.succAbove j)).face (j.predAbove i)

Deleting two vertices is independent of their order, with the indices transported through the first deletion. This is the semisimplicial face identity.

def AbstractSimplicialComplex.RealizationCell.cone {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) : K.RealizationCell (n + 1)

The cone on a cell c with a vertex v larger than all vertices of c, when adjoining v to c gives a face: the cell with vertex set c ∪ {v}.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.cone_val {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) : ↑↑(c.cone v hlt hK) = insert v ↑↑c

The vertex set of a cone is obtained by adjoining the cone vertex.

theorem AbstractSimplicialComplex.RealizationCell.vertexEmbedding_cone {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) : ⇑(c.cone v hlt hK).vertexEmbedding = fun (i : Fin (n + 1 + 1)) => Fin.lastCases v (⇑c.vertexEmbedding) i

The increasing enumeration of a cone enumerates the original cell and then the cone vertex.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.face_cone_last {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell n) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) : (c.cone v hlt hK).face (Fin.last (n + 1)) = c

Deleting the cone vertex from a cone recovers the original cell.

theorem AbstractSimplicialComplex.RealizationCell.face_val_subset {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) : ↑↑(c.face j) ⊆ ↑↑c

The vertex set of a deleted-vertex face of a cell lies in the original cell.

theorem AbstractSimplicialComplex.RealizationCell.insert_face_mem {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (j : Fin (n + 2)) {v : ι} (hK : insert v ↑↑c ∈ K) : insert v ↑↑(c.face j) ∈ K

Adjoining v to a deleted-vertex face of a cell gives a face of K when adjoining it to the cell does.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.face_cone_castSucc {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} {n : ℕ} (c : K.RealizationCell (n + 1)) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) (j : Fin (n + 2)) : (c.cone v hlt hK).face j.castSucc = (c.face j).cone v ⋯ ⋯

Deleting a vertex of the original cell from a cone gives the cone on the corresponding face.

@[simp]

theorem AbstractSimplicialComplex.RealizationCell.face_cone_zero {ι : Type u_1} [LinearOrder ι] {K : AbstractSimplicialComplex ι} (c : K.RealizationCell 0) (v : ι) (hlt : ∀ w ∈ ↑↑c, w < v) (hK : insert v ↑↑c ∈ K) : (c.cone v hlt hK).face 0 = vertex K v

Deleting the first vertex of the cone on a 0-cell leaves the cone vertex.