feat(Topology/CWComplex): 1-skeleton Graph of CWComplex (#37915)

This PR introduces `CWComplex.OneSkeletonGraph`, a graph with 0-dim cells as vertices and 1-dim cells as edges.

Author: Jun2M

Mathlib.lean

@@ -7433,6 +7433,7 @@ public import Mathlib.Topology.Bornology.Real
 public import Mathlib.Topology.CWComplex.Abstract.Basic
 public import Mathlib.Topology.CWComplex.Classical.Basic
 public import Mathlib.Topology.CWComplex.Classical.Finite
+public import Mathlib.Topology.CWComplex.Classical.Graph
 public import Mathlib.Topology.CWComplex.Classical.Subcomplex
 public import Mathlib.Topology.Category.Born
 public import Mathlib.Topology.Category.CompHaus.Basic

Mathlib/Topology/CWComplex/Classical/Basic.lean

@@ -74,7 +74,7 @@ together.
 
 noncomputable section
 
-open Metric Set
+open Metric Set Function
 
 namespace Topology
 
@@ -357,6 +357,60 @@ lemma RelCWComplex.cellFrontier_zero_eq_empty [RelCWComplex C D] {j : cell C 0}
     cellFrontier 0 j = ∅ := by
   simp [cellFrontier, sphere_eq_empty_of_subsingleton]
 
+lemma RelCWComplex.nonempty_cellFrontier [CWComplex C] {n : ℕ} (hn : n ≠ 0) (j : cell C n) :
+    (cellFrontier n j).Nonempty := by
+  letI : NeZero n := ⟨hn⟩
+  use map n j (Pi.single 0 1)
+  simp only [cellFrontier, mem_image, mem_sphere_iff_norm, sub_zero]
+  use Pi.single 0 1, by simp [Pi.norm_single]
+
+/-- If two 0-cells have the same characteristic image point, they are equal. -/
+lemma RelCWComplex.injective_map_zero (C : Set X) [RelCWComplex C D] :
+    Injective ((map 0 · ![]) : cell C 0 → X) := by
+  rintro x z h
+  by_contra hne
+  exact not_disjoint_iff.mpr ⟨map 0 x ![], by simp [openCell_zero_eq_singleton, h]⟩
+    <| disjoint_openCell_of_ne (by grind : (⟨0, x⟩ : Σ n, cell C n) ≠ ⟨0, z⟩)
+
+@[simp]
+lemma RelCWComplex.map_zero_eq_self_iff (C : Set X) [RelCWComplex C D] {x z : cell C 0} :
+    map 0 x ![] = map 0 z ![] ↔ x = z :=
+  ⟨fun h ↦ injective_map_zero C h, fun h ↦ h ▸ rfl⟩
+
+lemma RelCWComplex.closedCell_zero_injective (C : Set X) [RelCWComplex C D] :
+    Injective (closedCell 0 : cell C 0 → _) := by
+  intro x y h
+  rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
+  exact injective_map_zero C h
+
+lemma RelCWComplex.openCell_zero_injective (C : Set X) [RelCWComplex C D] :
+    Injective (openCell 0 : cell C 0 → _) := by
+  intro x y h
+  rw [openCell_zero_eq_singleton, openCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
+  exact injective_map_zero C h
+
+lemma RelCWComplex.cellFrontier_one_eq [RelCWComplex C D] (e : cell C 1) :
+    cellFrontier 1 e = map 1 e '' {-1, 1} := by
+  rw [cellFrontier]
+  congr 1
+  ext f
+  simp only [mem_sphere_iff_norm, sub_zero, Pi.norm_def, Finset.univ_unique, Fin.default_eq_zero,
+    Fin.isValue, Finset.sup_singleton, coe_nnnorm, Real.norm_eq_abs, abs_eq (zero_le_one' ℝ),
+    mem_insert_iff, mem_singleton_iff]
+  rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]
+  simp [const_apply, or_comm]
+
+lemma CWComplex.exists_cellFrontier_one_eq [CWComplex C] (e : cell C 1) :
+    ∃ x y : cell C 0, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y := by
+  obtain ⟨f, h⟩ := cellFrontier_subset_finite_closedCell 1 e
+  simp only [RelCWComplex.cellFrontier_one_eq, image_pair, Order.lt_one_iff, iUnion_iUnion_eq_left,
+    RelCWComplex.closedCell_zero_eq_singleton, pair_subset_iff, mem_iUnion, mem_singleton_iff,
+    exists_prop] at h
+  obtain ⟨⟨u, hu, hun1⟩, v, hv, hv1⟩ := h
+  use u, v
+  simp [RelCWComplex.cellFrontier_one_eq, image_pair, RelCWComplex.closedCell_zero_eq_singleton,
+    hun1, hv1, pair_comm]
+
 lemma RelCWComplex.base_subset_complex [RelCWComplex C D] : D ⊆ C := by
   simp_rw [← union]
   exact subset_union_left

Mathlib/Topology/CWComplex/Classical/Graph.lean

@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Jun Kwon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jun Kwon
+-/
+module
+
+public import Mathlib.Topology.CWComplex.Classical.Finite
+public import Mathlib.Combinatorics.Graph.Basic
+
+/-!
+# 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.
+
+-/
+
+public section
+
+open Metric Set Graph
+
+namespace Topology
+
+variable {X : Type*} [TopologicalSpace X]
+
+/-- The 1-skeleton of a CW complex as a graph. -/
+@[expose, simps]
+def CWComplex.OneSkeletonGraph (C : Set X) [CWComplex C] : Graph (cell C 0) (cell C 1) where
+  vertexSet := univ
+  edgeSet := univ
+  IsLink e x y := cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y
+  isLink_symm _ _ x y h := by grind
+  eq_or_eq_of_isLink_of_isLink e x y z w h1 h2 := by
+    simp_rw [closedCell_zero_eq_singleton] at h1 h2
+    rw [h1] at h2
+    simp only [(RelCWComplex.injective_map_zero C).eq_iff, union_singleton, pair_eq_pair_iff] at h2
+    tauto
+  left_mem_of_isLink _ _ _ _ := mem_univ _
+  edge_mem_iff_exists_isLink e := by
+    simp only [mem_univ, true_iff]
+    exact exists_cellFrontier_one_eq e
+
+namespace CWComplex.OneSkeletonGraph
+
+variable {C : Set X} [CWComplex C]
+
+lemma isLink_iff_pair (e : cell C 1) (x y : cell C 0) :
+    (OneSkeletonGraph C).IsLink e x y ↔ cellFrontier 1 e = {map 0 x ![], map 0 y ![]} := by
+  rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
+    singleton_union]
+
+lemma exists_isLoopAt_iff (e : cell C 1) : (∃ x : cell C 0, (OneSkeletonGraph C).IsLoopAt e x) ↔
+      ∃ x : cell C 0, cellFrontier 1 e = closedCell 0 x := by
+  refine exists_congr fun x ↦ ?_
+  change cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 x ↔ _
+  rw [union_self]
+
+lemma exists_isLoopAt_iff_subsingleton (e : cell C 1) :
+    (∃ x : cell C 0, (OneSkeletonGraph C).IsLoopAt e x) ↔ (cellFrontier 1 e).Subsingleton := by
+  rw [exists_isLoopAt_iff]
+  refine ⟨fun ⟨x, hx⟩ => by simp [closedCell_zero_eq_singleton, hx], fun h => ?_⟩
+  obtain ⟨x, y, hxy⟩ := exists_cellFrontier_one_eq e
+  simp only [closedCell_zero_eq_singleton, union_singleton] at hxy
+  obtain rfl : x = y := RelCWComplex.injective_map_zero C <| (hxy ▸ h) (by simp) (by simp)
+  exact ⟨x, by simp [hxy, closedCell_zero_eq_singleton]⟩
+
+lemma not_exists_isLoopAt_iff_nontrivial (e : cell C 1) :
+    ¬(∃ x : cell C 0, (OneSkeletonGraph C).IsLoopAt e x) ↔ (cellFrontier 1 e).Nontrivial :=
+  (exists_isLoopAt_iff_subsingleton e).not.trans not_subsingleton_iff
+
+@[simp]
+lemma adj_iff (x y : cell C 0) : (OneSkeletonGraph C).Adj x y ↔
+    ∃ e : cell C 1, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y := Iff.rfl
+
+end CWComplex.OneSkeletonGraph
+
+end Topology