refactor: make SimpleGraph.chromaticNumber be ENat-valued (#8883)

This removes an awkwardness of the API, where theorems had to include colorability hypotheses. This trades that awkwardness for a smaller one, which is that one writes `G.Colorable (ENat.toNat G.chromaticNumber)` rather than `G.Colorable G.chromaticNumber`.

It would be good to have a followup refactoring PR to more carefully evaluate the API after this change.

Mathlib/Combinatorics/SimpleGraph/Coloring.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino, Kyle Miller
 -/
 import Mathlib.Combinatorics.SimpleGraph.Clique
+import Mathlib.Data.ENat.Lattice
 import Mathlib.Data.Nat.Lattice
 import Mathlib.Data.Setoid.Partition
 import Mathlib.Order.Antichain
@@ -30,8 +31,10 @@ a complete graph, whose vertices represent the colors.
   is whether there exists a coloring with at most *n* colors.
 
 * `G.chromaticNumber` is the minimal `n` such that `G` is
-  `n`-colorable, or `0` if it cannot be colored with finitely many
+  `n`-colorable, or `⊤` if it cannot be colored with finitely many
   colors.
+  (Cardinal-valued chromatic numbers are more niche, so we stick to `ℕ∞`.)
+  We write `G.chromaticNumber ≠ ⊤` to mean a graph is colorable with finitely many colors.
 
 * `C.colorClass c` is the set of vertices colored by `c : α` in the
   coloring `C : G.Coloring α`.
@@ -157,11 +160,24 @@ def selfColoring : G.Coloring V := Coloring.mk id fun {_ _} => G.ne_of_adj
 #align simple_graph.self_coloring SimpleGraph.selfColoring
 
 /-- The chromatic number of a graph is the minimal number of colors needed to color it.
-If `G` isn't colorable with finitely many colors, this will be 0. -/
-noncomputable def chromaticNumber : ℕ :=
-  sInf { n : ℕ | G.Colorable n }
+This is `⊤` (infinity) iff `G` isn't colorable with finitely many colors.
+
+If `G` is colorable, then `ENat.toNat G.chromaticNumber` is the `ℕ`-valued chromatic number. -/
+noncomputable def chromaticNumber : ℕ∞ := ⨅ n ∈ setOf G.Colorable, (n : ℕ∞)
 #align simple_graph.chromatic_number SimpleGraph.chromaticNumber
 
+lemma chromaticNumber_eq_biInf {G : SimpleGraph V} :
+    G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, (n : ℕ∞) := rfl
+
+lemma chromaticNumber_eq_iInf {G : SimpleGraph V} :
+    G.chromaticNumber = ⨅ n : {m | G.Colorable m}, (n : ℕ∞) := by
+  rw [chromaticNumber, iInf_subtype]
+
+lemma Colorable.chromaticNumber_eq_sInf {G : SimpleGraph V} {n} (h : G.Colorable n) :
+    G.chromaticNumber = sInf {n' : ℕ | G.Colorable n'} := by
+  rw [ENat.coe_sInf, chromaticNumber]
+  exact ⟨_, h⟩
+
 /-- Given an embedding, there is an induced embedding of colorings. -/
 def recolorOfEmbedding {α β : Type*} (f : α ↪ β) : G.Coloring α ↪ G.Coloring β where
   toFun C := (Embedding.completeGraph f).toHom.comp C
@@ -200,12 +216,12 @@ theorem Colorable.mono {n m : ℕ} (h : n ≤ m) (hc : G.Colorable n) : G.Colora
   ⟨G.recolorOfCardLE (by simp [h]) hc.some⟩
 #align simple_graph.colorable.mono SimpleGraph.Colorable.mono
 
-theorem Coloring.to_colorable [Fintype α] (C : G.Coloring α) : G.Colorable (Fintype.card α) :=
+theorem Coloring.colorable [Fintype α] (C : G.Coloring α) : G.Colorable (Fintype.card α) :=
   ⟨G.recolorOfCardLE (by simp) C⟩
-#align simple_graph.coloring.to_colorable SimpleGraph.Coloring.to_colorable
+#align simple_graph.coloring.to_colorable SimpleGraph.Coloring.colorable
 
 theorem colorable_of_fintype (G : SimpleGraph V) [Fintype V] : G.Colorable (Fintype.card V) :=
-  G.selfColoring.to_colorable
+  G.selfColoring.colorable
 #align simple_graph.colorable_of_fintype SimpleGraph.colorable_of_fintype
 
 /-- Noncomputably get a coloring from colorability. -/
@@ -247,47 +263,63 @@ theorem chromaticNumber_bddBelow : BddBelow { n : ℕ | G.Colorable n } :=
   ⟨0, fun _ _ => zero_le _⟩
 #align simple_graph.chromatic_number_bdd_below SimpleGraph.chromaticNumber_bddBelow
 
-theorem chromaticNumber_le_of_colorable {n : ℕ} (hc : G.Colorable n) : G.chromaticNumber ≤ n := by
-  rw [chromaticNumber]
+theorem Colorable.chromaticNumber_le {n : ℕ} (hc : G.Colorable n) : G.chromaticNumber ≤ n := by
+  rw [hc.chromaticNumber_eq_sInf]
+  norm_cast
   apply csInf_le chromaticNumber_bddBelow
-  constructor
-  exact Classical.choice hc
-#align simple_graph.chromatic_number_le_of_colorable SimpleGraph.chromaticNumber_le_of_colorable
+  exact hc
+#align simple_graph.chromatic_number_le_of_colorable SimpleGraph.Colorable.chromaticNumber_le
+
+theorem chromaticNumber_ne_top_iff_exists : G.chromaticNumber ≠ ⊤ ↔ ∃ n, G.Colorable n := by
+  rw [chromaticNumber]
+  convert_to ⨅ n : {m | G.Colorable m}, (n : ℕ∞) ≠ ⊤ ↔ _
+  · rw [iInf_subtype]
+  rw [← lt_top_iff_ne_top, ENat.iInf_coe_lt_top]
+  simp
+
+theorem chromaticNumber_le_iff_colorable {n : ℕ} : G.chromaticNumber ≤ n ↔ G.Colorable n := by
+  refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩
+  have : G.chromaticNumber ≠ ⊤ := (trans h (WithTop.coe_lt_top n)).ne
+  rw [chromaticNumber_ne_top_iff_exists] at this
+  obtain ⟨m, hm⟩ := this
+  rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h
+  have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)
+  rw [Set.mem_setOf_eq] at this
+  exact this.mono h
 
 theorem chromaticNumber_le_card [Fintype α] (C : G.Coloring α) :
-    G.chromaticNumber ≤ Fintype.card α :=
-  csInf_le chromaticNumber_bddBelow C.to_colorable
+    G.chromaticNumber ≤ Fintype.card α := by
+  rw [C.colorable.chromaticNumber_eq_sInf]
+  norm_cast
+  exact csInf_le chromaticNumber_bddBelow C.colorable
 #align simple_graph.chromatic_number_le_card SimpleGraph.chromaticNumber_le_card
 
-theorem colorable_chromaticNumber {m : ℕ} (hc : G.Colorable m) : G.Colorable G.chromaticNumber := by
+theorem colorable_chromaticNumber {m : ℕ} (hc : G.Colorable m) :
+    G.Colorable (ENat.toNat G.chromaticNumber) := by
   classical
-  dsimp only [chromaticNumber]
-  rw [Nat.sInf_def]
+  rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
   apply Nat.find_spec
   exact colorable_set_nonempty_of_colorable hc
 #align simple_graph.colorable_chromatic_number SimpleGraph.colorable_chromaticNumber
 
 theorem colorable_chromaticNumber_of_fintype (G : SimpleGraph V) [Finite V] :
-    G.Colorable G.chromaticNumber := by
+    G.Colorable (ENat.toNat G.chromaticNumber) := by
   cases nonempty_fintype V
   exact colorable_chromaticNumber G.colorable_of_fintype
 #align simple_graph.colorable_chromatic_number_of_fintype SimpleGraph.colorable_chromaticNumber_of_fintype
 
 theorem chromaticNumber_le_one_of_subsingleton (G : SimpleGraph V) [Subsingleton V] :
     G.chromaticNumber ≤ 1 := by
-  rw [chromaticNumber]
-  apply csInf_le chromaticNumber_bddBelow
-  constructor
-  refine' Coloring.mk (fun _ => 0) _
-  intro v w
-  rw [Subsingleton.elim v w]
+  rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]
+  refine ⟨Coloring.mk (fun _ => 0) ?_⟩
+  intros v w
+  cases Subsingleton.elim v w
   simp
 #align simple_graph.chromatic_number_le_one_of_subsingleton SimpleGraph.chromaticNumber_le_one_of_subsingleton
 
 theorem chromaticNumber_eq_zero_of_isempty (G : SimpleGraph V) [IsEmpty V] :
     G.chromaticNumber = 0 := by
-  rw [← nonpos_iff_eq_zero]
-  apply csInf_le chromaticNumber_bddBelow
+  rw [← nonpos_iff_eq_zero, ← Nat.cast_zero, chromaticNumber_le_iff_colorable]
   apply colorable_of_isEmpty
 #align simple_graph.chromatic_number_eq_zero_of_isempty SimpleGraph.chromaticNumber_eq_zero_of_isempty
 
@@ -299,6 +331,7 @@ theorem isEmpty_of_chromaticNumber_eq_zero (G : SimpleGraph V) [Finite V]
 #align simple_graph.is_empty_of_chromatic_number_eq_zero SimpleGraph.isEmpty_of_chromaticNumber_eq_zero
 
 theorem chromaticNumber_pos [Nonempty V] {n : ℕ} (hc : G.Colorable n) : 0 < G.chromaticNumber := by
+  rw [hc.chromaticNumber_eq_sInf, Nat.cast_pos]
   apply le_csInf (colorable_set_nonempty_of_colorable hc)
   intro m hm
   by_contra h'
@@ -308,43 +341,48 @@ theorem chromaticNumber_pos [Nonempty V] {n : ℕ} (hc : G.Colorable n) : 0 < G.
   exact Nat.not_lt_zero _ h₁
 #align simple_graph.chromatic_number_pos SimpleGraph.chromaticNumber_pos
 
-theorem colorable_of_chromaticNumber_pos (h : 0 < G.chromaticNumber) :
-    G.Colorable G.chromaticNumber := by
-  obtain ⟨h, hn⟩ := Nat.nonempty_of_pos_sInf h
+theorem colorable_of_chromaticNumber_ne_top (h : G.chromaticNumber ≠ ⊤) :
+    G.Colorable (ENat.toNat G.chromaticNumber) := by
+  rw [chromaticNumber_ne_top_iff_exists] at h
+  obtain ⟨n, hn⟩ := h
   exact colorable_chromaticNumber hn
-#align simple_graph.colorable_of_chromatic_number_pos SimpleGraph.colorable_of_chromaticNumber_pos
+#align simple_graph.colorable_of_chromatic_number_pos SimpleGraph.colorable_of_chromaticNumber_ne_top
 
 theorem Colorable.mono_left {G' : SimpleGraph V} (h : G ≤ G') {n : ℕ} (hc : G'.Colorable n) :
     G.Colorable n :=
   ⟨hc.some.comp (Hom.mapSpanningSubgraphs h)⟩
 #align simple_graph.colorable.mono_left SimpleGraph.Colorable.mono_left
 
-theorem Colorable.chromaticNumber_le_of_forall_imp {V' : Type*} {G' : SimpleGraph V'} {m : ℕ}
-    (hc : G'.Colorable m) (h : ∀ n, G'.Colorable n → G.Colorable n) :
+theorem chromaticNumber_le_of_forall_imp {V' : Type*} {G' : SimpleGraph V'}
+    (h : ∀ n, G'.Colorable n → G.Colorable n) :
     G.chromaticNumber ≤ G'.chromaticNumber := by
-  apply csInf_le chromaticNumber_bddBelow
-  apply h
-  apply colorable_chromaticNumber hc
-#align simple_graph.colorable.chromatic_number_le_of_forall_imp SimpleGraph.Colorable.chromaticNumber_le_of_forall_imp
-
-theorem Colorable.chromaticNumber_mono (G' : SimpleGraph V) {m : ℕ} (hc : G'.Colorable m)
+  rw [chromaticNumber, chromaticNumber]
+  simp only [Set.mem_setOf_eq, le_iInf_iff]
+  intro m hc
+  have := h _ hc
+  rw [← chromaticNumber_le_iff_colorable] at this
+  exact this
+#align simple_graph.colorable.chromatic_number_le_of_forall_imp SimpleGraph.chromaticNumber_le_of_forall_imp
+
+theorem chromaticNumber_mono (G' : SimpleGraph V)
     (h : G ≤ G') : G.chromaticNumber ≤ G'.chromaticNumber :=
-  hc.chromaticNumber_le_of_forall_imp fun _ => Colorable.mono_left h
-#align simple_graph.colorable.chromatic_number_mono SimpleGraph.Colorable.chromaticNumber_mono
+  chromaticNumber_le_of_forall_imp fun _ => Colorable.mono_left h
+#align simple_graph.colorable.chromatic_number_mono SimpleGraph.chromaticNumber_mono
 
-theorem Colorable.chromaticNumber_mono_of_embedding {V' : Type*} {G' : SimpleGraph V'} {n : ℕ}
-    (h : G'.Colorable n) (f : G ↪g G') : G.chromaticNumber ≤ G'.chromaticNumber :=
-  h.chromaticNumber_le_of_forall_imp fun _ => Colorable.of_embedding f
-#align simple_graph.colorable.chromatic_number_mono_of_embedding SimpleGraph.Colorable.chromaticNumber_mono_of_embedding
+theorem chromaticNumber_mono_of_embedding {V' : Type*} {G' : SimpleGraph V'}
+    (f : G ↪g G') : G.chromaticNumber ≤ G'.chromaticNumber :=
+  chromaticNumber_le_of_forall_imp fun _ => Colorable.of_embedding f
+#align simple_graph.colorable.chromatic_number_mono_of_embedding SimpleGraph.chromaticNumber_mono_of_embedding
 
 theorem chromaticNumber_eq_card_of_forall_surj [Fintype α] (C : G.Coloring α)
     (h : ∀ C' : G.Coloring α, Function.Surjective C') : G.chromaticNumber = Fintype.card α := by
   apply le_antisymm
   · apply chromaticNumber_le_card C
-  · by_contra hc
+  · rw [C.colorable.chromaticNumber_eq_sInf, Nat.cast_le]
+    by_contra hc
     rw [not_le] at hc
     obtain ⟨n, cn, hc⟩ :=
-      exists_lt_of_csInf_lt (colorable_set_nonempty_of_colorable C.to_colorable) hc
+      exists_lt_of_csInf_lt (colorable_set_nonempty_of_colorable C.colorable) hc
     rw [← Fintype.card_fin n] at hc
     have f := (Function.Embedding.nonempty_of_card_le (le_of_lt hc)).some
     have C' := cn.some
@@ -359,7 +397,8 @@ theorem chromaticNumber_bot [Nonempty V] : (⊥ : SimpleGraph V).chromaticNumber
       Coloring.mk (fun _ => 0) fun {v w} h => False.elim h
   apply le_antisymm
   · exact chromaticNumber_le_card C
-  · exact chromaticNumber_pos C.to_colorable
+  · rw [ENat.one_le_iff_pos]
+    exact chromaticNumber_pos C.colorable
 #align simple_graph.chromatic_number_bot SimpleGraph.chromaticNumber_bot
 
 @[simp]
@@ -373,19 +412,13 @@ theorem chromaticNumber_top [Fintype V] : (⊤ : SimpleGraph V).chromaticNumber
   exact C.valid h
 #align simple_graph.chromatic_number_top SimpleGraph.chromaticNumber_top
 
-theorem chromaticNumber_top_eq_zero_of_infinite (V : Type*) [Infinite V] :
-    (⊤ : SimpleGraph V).chromaticNumber = 0 := by
-  let n := (⊤ : SimpleGraph V).chromaticNumber
+theorem chromaticNumber_top_eq_top_of_infinite (V : Type*) [Infinite V] :
+    (⊤ : SimpleGraph V).chromaticNumber = ⊤ := by
   by_contra hc
-  replace hc := pos_iff_ne_zero.mpr hc
-  apply Nat.not_succ_le_self n
-  convert_to (⊤ : SimpleGraph { m | m < n + 1 }).chromaticNumber ≤ _
-  · rw [SimpleGraph.chromaticNumber_top, Fintype.card_ofFinset,
-        Finset.card_range, Nat.succ_eq_add_one]
-  refine' (colorable_of_chromaticNumber_pos hc).chromaticNumber_mono_of_embedding _
-  apply Embedding.completeGraph
-  exact (Function.Embedding.subtype _).trans (Infinite.natEmbedding V)
-#align simple_graph.chromatic_number_top_eq_zero_of_infinite SimpleGraph.chromaticNumber_top_eq_zero_of_infinite
+  rw [← Ne.def, chromaticNumber_ne_top_iff_exists] at hc
+  obtain ⟨n, ⟨hn⟩⟩ := hc
+  exact not_injective_infinite_finite _ hn.injective_of_top_hom
+#align simple_graph.chromatic_number_top_eq_zero_of_infinite SimpleGraph.chromaticNumber_top_eq_top_of_infinite
 
 /-- The bicoloring of a complete bipartite graph using whether a vertex
 is on the left or on the right. -/
@@ -433,12 +466,17 @@ theorem IsClique.card_le_of_colorable {s : Finset V} (h : G.IsClique s) {n : ℕ
   simp
 #align simple_graph.is_clique.card_le_of_colorable SimpleGraph.IsClique.card_le_of_colorable
 
--- TODO eliminate `Finite V` constraint once chromatic numbers are refactored.
--- This is just to ensure the chromatic number exists.
-theorem IsClique.card_le_chromaticNumber [Finite V] {s : Finset V} (h : G.IsClique s) :
+theorem IsClique.card_le_chromaticNumber {s : Finset V} (h : G.IsClique s) :
     s.card ≤ G.chromaticNumber := by
-  cases nonempty_fintype V
-  exact h.card_le_of_colorable G.colorable_chromaticNumber_of_fintype
+  obtain (hc | hc) := eq_or_ne G.chromaticNumber ⊤
+  · rw [hc]
+    exact le_top
+  · have hc' := hc
+    rw [chromaticNumber_ne_top_iff_exists] at hc'
+    obtain ⟨n, c⟩ := hc'
+    rw [← ENat.coe_toNat_eq_self] at hc
+    rw [← hc, Nat.cast_le]
+    exact h.card_le_of_colorable (colorable_chromaticNumber c)
 #align simple_graph.is_clique.card_le_chromatic_number SimpleGraph.IsClique.card_le_chromaticNumber
 
 protected theorem Colorable.cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n < m) :
@@ -449,11 +487,15 @@ protected theorem Colorable.cliqueFree {n m : ℕ} (hc : G.Colorable n) (hm : n
   exact Nat.lt_le_asymm hm (h.card_le_of_colorable hc)
 #align simple_graph.colorable.clique_free SimpleGraph.Colorable.cliqueFree
 
--- TODO eliminate `Finite V` constraint once chromatic numbers are refactored.
--- This is just to ensure the chromatic number exists.
-theorem cliqueFree_of_chromaticNumber_lt [Finite V] {n : ℕ} (hc : G.chromaticNumber < n) :
-    G.CliqueFree n :=
-  G.colorable_chromaticNumber_of_fintype.cliqueFree hc
+theorem cliqueFree_of_chromaticNumber_lt {n : ℕ} (hc : G.chromaticNumber < n) :
+    G.CliqueFree n := by
+  have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top
+  obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne
+  have := colorable_chromaticNumber hc'
+  refine this.cliqueFree ?_
+  rw [← ENat.coe_toNat_eq_self] at hne
+  rw [← hne] at hc
+  simpa using hc
 #align simple_graph.clique_free_of_chromatic_number_lt SimpleGraph.cliqueFree_of_chromaticNumber_lt
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean

@@ -42,10 +42,10 @@ def pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : pathGraph 2 ↪g pathGraph
 
 theorem chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) :
     (pathGraph n).chromaticNumber = 2 := by
-  have hc := (pathGraph.bicoloring n).to_colorable
+  have hc := (pathGraph.bicoloring n).colorable
   apply le_antisymm
-  · exact chromaticNumber_le_of_colorable hc
+  · exact hc.chromaticNumber_le
   · simpa only [pathGraph_two_eq_top, chromaticNumber_top] using
-      hc.chromaticNumber_mono_of_embedding (pathGraph_two_embedding n h)
+      chromaticNumber_mono_of_embedding (pathGraph_two_embedding n h)
 
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Partition.lean

@@ -115,9 +115,9 @@ def toColoring' : G.Coloring (Set V) :=
   Coloring.mk P.partOfVertex fun hvw ↦ P.partOfVertex_ne_of_adj hvw
 #align simple_graph.partition.to_coloring' SimpleGraph.Partition.toColoring'
 
-theorem to_colorable [Fintype P.parts] : G.Colorable (Fintype.card P.parts) :=
-  P.toColoring.to_colorable
-#align simple_graph.partition.to_colorable SimpleGraph.Partition.to_colorable
+theorem colorable [Fintype P.parts] : G.Colorable (Fintype.card P.parts) :=
+  P.toColoring.colorable
+#align simple_graph.partition.to_colorable SimpleGraph.Partition.colorable
 
 end Partition
 
@@ -143,7 +143,7 @@ theorem partitionable_iff_colorable {n : ℕ} : G.Partitionable n ↔ G.Colorabl
   · rintro ⟨P, hf, hc⟩
     have : Fintype P.parts := hf.fintype
     rw [Set.Finite.card_toFinset hf] at hc
-    apply P.to_colorable.mono hc
+    apply P.colorable.mono hc
   · rintro ⟨C⟩
     refine' ⟨C.toPartition, C.colorClasses_finite, le_trans _ (Fintype.card_fin n).le⟩
     generalize_proofs h