1-skeletons of CW complexes as graphs

In this file we define the 1-skeleton of a CW complex as a graph.

Main definitions

• CWComplex.OneSkeletonGraph: the 1-skeleton of a CW complex as a graph.

def Topology.CWComplex.OneSkeletonGraph {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] : Graph (cell C 0) (cell C 1)

The 1-skeleton of a CW complex as a graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Topology.CWComplex.OneSkeletonGraph_isLink {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] (e : cell C 1) (x y : cell C 0) : (OneSkeletonGraph C).IsLink e x y = (cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y)

@[simp]

theorem Topology.CWComplex.vertexSet_OneSkeletonGraph {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] : (OneSkeletonGraph C).vertexSet = Set.univ

@[simp]

theorem Topology.CWComplex.edgeSet_OneSkeletonGraph {X : Type u_1} [TopologicalSpace X] (C : Set X) [CWComplex C] : (OneSkeletonGraph C).edgeSet = Set.univ

theorem Topology.CWComplex.OneSkeletonGraph.isLink_iff_pair {X : Type u_1} [TopologicalSpace X] {C : Set X} [CWComplex C] (e : cell C 1) (x y : cell C 0) : (OneSkeletonGraph C).IsLink e x y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

theorem Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff {X : Type u_1} [TopologicalSpace X] {C : Set X} [CWComplex C] (e : cell C 1) : (∃ (x : cell C 0), (OneSkeletonGraph C).IsLoopAt e x) ↔ ∃ (x : cell C 0), cellFrontier 1 e = closedCell 0 x

theorem Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff_subsingleton {X : Type u_1} [TopologicalSpace X] {C : Set X} [CWComplex C] (e : cell C 1) : (∃ (x : cell C 0), (OneSkeletonGraph C).IsLoopAt e x) ↔ (cellFrontier 1 e).Subsingleton

theorem Topology.CWComplex.OneSkeletonGraph.not_exists_isLoopAt_iff_nontrivial {X : Type u_1} [TopologicalSpace X] {C : Set X} [CWComplex C] (e : cell C 1) : (¬∃ (x : cell C 0), (OneSkeletonGraph C).IsLoopAt e x) ↔ (cellFrontier 1 e).Nontrivial

@[simp]

theorem Topology.CWComplex.OneSkeletonGraph.adj_iff {X : Type u_1} [TopologicalSpace X] {C : Set X} [CWComplex C] (x y : cell C 0) : (OneSkeletonGraph C).Adj x y ↔ ∃ (e : cell C 1), cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y