Definition 19: Edge Boundary and Vertex Incidence for Cell Complexes

For a cell complex X (Def_7), we define:

• edgeBoundaryCell X S — the edge boundary δS = {e ∈ X₁ | ∃ u ∈ ∂₁e, u ∈ S, ∃ w ∈ ∂₁e, w ∉ S}
• incidentVerticesCell X E — vertices incident to edges E: Γ(E) = {v ∈ X₀ | ∃ e ∈ E, v ∈ ∂₁ e}
• incidentEdges X v — edges incident to vertex v: δv = {e ∈ X₁ | v ∈ ∂₁ e}
• edgeBoundaryVertex X S v — edges in the edge boundary incident to v: (δS)_v = δS ∩ δv

Main Results

• mem_edgeBoundaryCell — membership characterization for δS
• mem_incidentVerticesCell — membership characterization for Γ(E)
• mem_incidentEdges — membership characterization for δv
• mem_edgeBoundaryVertex — membership characterization for (δS)_v
• edgeBoundaryVertex_subset — (δS)_v ⊆ δS
• edgeBoundaryVertex_subset_incidentEdges — (δS)_v ⊆ δv
• mem_edgeBoundaryVertex_iff — alternate characterization

Edge Boundary

def CellComplex.edgeBoundaryCell (X : CellComplex) (S : Finset (X.cells 0)) : Finset (X.cells 1)

The edge boundary δS = {e ∈ X₁ | ∃ u ∈ ∂₁e, u ∈ S, ∃ w ∈ ∂₁e, w ∉ S} of a vertex subset S ⊆ X₀. An edge e is in δS iff its boundary contains a vertex in S and a vertex outside S.

Equations

• X.edgeBoundaryCell S = {e : X.cells 1 | (∃ u ∈ X.bdry e, u ∈ S) ∧ ∃ w ∈ X.bdry e, w ∉ S}

theorem CellComplex.mem_edgeBoundaryCell (X : CellComplex) (S : Finset (X.cells 0)) (e : X.cells 1) : e ∈ X.edgeBoundaryCell S ↔ (∃ u ∈ X.bdry e, u ∈ S) ∧ ∃ w ∈ X.bdry e, w ∉ S

Membership in the edge boundary: e ∈ δS iff ∂₁ e meets both S and Sᶜ.

theorem CellComplex.edgeBoundaryCell_nonempty (X : CellComplex) (S : Finset (X.cells 0)) (h : ∃ (e : X.cells 1), (∃ u ∈ X.bdry e, u ∈ S) ∧ ∃ w ∈ X.bdry e, w ∉ S) : (X.edgeBoundaryCell S).Nonempty

Witness: the edge boundary is nonempty when there exists an edge with one endpoint in S and one outside S.

Incident Vertices

def CellComplex.incidentVerticesCell (X : CellComplex) (E : Finset (X.cells 1)) : Finset (X.cells 0)

The set of vertices incident to a set of edges E ⊆ X₁: Γ(E) = {v ∈ X₀ | ∃ e ∈ E, v ∈ ∂₁ e}.

Equations

• X.incidentVerticesCell E = {v : X.cells 0 | ∃ e ∈ E, v ∈ X.bdry e}

theorem CellComplex.mem_incidentVerticesCell (X : CellComplex) (E : Finset (X.cells 1)) (v : X.cells 0) : v ∈ X.incidentVerticesCell E ↔ ∃ e ∈ E, v ∈ X.bdry e

Membership in incident vertices: v ∈ Γ(E) iff there exists an edge e ∈ E with v ∈ ∂₁ e.

theorem CellComplex.incidentVerticesCell_nonempty (X : CellComplex) (E : Finset (X.cells 1)) (h : ∃ e ∈ E, ∃ (v : X.cells 0), v ∈ X.bdry e) : (X.incidentVerticesCell E).Nonempty

Witness: incidentVerticesCell is nonempty when E contains an edge with a nonempty boundary.

Incident Edges (Star of a vertex)

def CellComplex.incidentEdges (X : CellComplex) (v : X.cells 0) : Finset (X.cells 1)

The set of edges incident to a vertex v: δv = {e ∈ X₁ | v ∈ ∂₁ e}, i.e., the star of v.

Equations

• X.incidentEdges v = {e : X.cells 1 | v ∈ X.bdry e}

theorem CellComplex.mem_incidentEdges (X : CellComplex) (v : X.cells 0) (e : X.cells 1) : e ∈ X.incidentEdges v ↔ v ∈ X.bdry e

Membership in incident edges: e ∈ δv iff v ∈ ∂₁ e.

theorem CellComplex.incidentEdges_nonempty (X : CellComplex) (v : X.cells 0) (h : ∃ (e : X.cells 1), v ∈ X.bdry e) : (X.incidentEdges v).Nonempty

Witness: incidentEdges is nonempty when there exists an edge whose boundary contains v.

Edge Boundary Vertex

def CellComplex.edgeBoundaryVertex (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) : Finset (X.cells 1)

The edges in the edge boundary δS that are incident to vertex v: (δS)_v = δS ∩ δv = {e ∈ X₁ | e ∈ δS ∧ v ∈ ∂₁ e}.

Equations

• X.edgeBoundaryVertex S v = {e ∈ X.edgeBoundaryCell S | v ∈ X.bdry e}

theorem CellComplex.mem_edgeBoundaryVertex (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) (e : X.cells 1) : e ∈ X.edgeBoundaryVertex S v ↔ e ∈ X.edgeBoundaryCell S ∧ v ∈ X.bdry e

Membership in the edge boundary at vertex v: e ∈ (δS)_v iff e ∈ δS and v ∈ ∂₁ e.

theorem CellComplex.edgeBoundaryVertex_subset (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) : X.edgeBoundaryVertex S v ⊆ X.edgeBoundaryCell S

edgeBoundaryVertex is a subset of the edge boundary.

theorem CellComplex.edgeBoundaryVertex_subset_incidentEdges (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) : X.edgeBoundaryVertex S v ⊆ X.incidentEdges v

edgeBoundaryVertex is a subset of the incident edges.

theorem CellComplex.edgeBoundaryVertex_nonempty (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) (h : ∃ e ∈ X.edgeBoundaryCell S, v ∈ X.bdry e) : (X.edgeBoundaryVertex S v).Nonempty

Witness: edgeBoundaryVertex is nonempty when there exists an edge in δS incident to v.

theorem CellComplex.mem_edgeBoundaryVertex_iff (X : CellComplex) (S : Finset (X.cells 0)) (v : X.cells 0) (e : X.cells 1) : e ∈ X.edgeBoundaryVertex S v ↔ v ∈ X.bdry e ∧ (∃ u ∈ X.bdry e, u ∈ S) ∧ ∃ w ∈ X.bdry e, w ∉ S

Alternate characterization: e ∈ (δS)_v iff v ∈ ∂₁ e, ∂₁ e meets S, and ∂₁ e meets Sᶜ.