2607.20376v1 / Tihany.lean
all files
import Mathlib
/-!
# The Erdős--Lovász Tihany conjecture for even-hole-free graphs
This file formalizes the new argument in arXiv:2607.20376v1. The only
external mathematical input is isolated in `ChudnovskySeymourStatement`:
every nonempty even-hole-free graph has a bisimplicial vertex.
-/
open scoped SimpleGraph
namespace Tihany
open Finset Set
open SimpleGraph
universe u
variable {V : Type u} [Fintype V] [DecidableEq V]
/-- A vertex is bisimplicial when its neighborhood is the union of two
cliques. This is verbatim the paper's definition (the cliques need not
initially be disjoint). -/
def Bisimplicial (G : SimpleGraph V) (v : V) : Prop :=
∃ A B : Set V,
G.IsClique A ∧ G.IsClique B ∧ G.neighborSet v = A ∪ B
/-- A finite, disjoint form of `Bisimplicial`, used in the proof. -/
def BisimplicialFinset (G : SimpleGraph V) (v : V) : Prop :=
∃ A B : Finset V,
Disjoint A B ∧ G.IsClique A ∧ G.IsClique B ∧
((A ∪ B : Finset V) : Set V) = G.neighborSet v
theorem bisimplicial_iff_finset (G : SimpleGraph V) (v : V) :
Bisimplicial G v ↔ BisimplicialFinset G v := by
classical
constructor
· rintro ⟨A, B, hA, hB, hn⟩
let Af : Finset V := A.toFinset
let Bf : Finset V := (B \ A).toFinset
refine ⟨Af, Bf, ?_, ?_, ?_, ?_⟩
· rw [Finset.disjoint_left]
intro a ha hb
have ha' : a ∈ A := by simpa [Af] using ha
have hb' : a ∈ B \ A := by simpa [Bf] using hb
exact hb'.2 ha'
· simpa [Af, Set.coe_toFinset] using hA
· apply hB.subset
intro x hx
exact (by simpa [Bf] using hx : x ∈ B \ A).1
· ext x
rw [hn]
simp [Af, Bf]
· rintro ⟨A, B, hAB, hA, hB, hn⟩
refine ⟨(A : Set V), (B : Set V), hA, hB, ?_⟩
simpa only [Finset.coe_union] using hn.symm
/-- The common neighborhood used in the paper. -/
def commonNeighbors (G : SimpleGraph V) (K : Finset V) : Set V :=
{x | x ∉ K ∧ ∀ a ∈ K, G.Adj x a}
theorem mem_commonNeighbors {G : SimpleGraph V} {K : Finset V} {x : V} :
x ∈ commonNeighbors G K ↔ x ∉ K ∧ ∀ a ∈ K, G.Adj x a :=
Iff.rfl
/-- `K` is Tihany at chromatic number `k`: deleting it is not
`(k - |K|)`-colorable. Under `χ(G)=k`, this is exactly
`χ(G-K) ≥ k-|K|+1`. -/
def IsTihanyAt (G : SimpleGraph V) (k : ℕ) (K : Finset V) : Prop :=
G.IsClique K ∧
¬(G.induce ((K : Set V)ᶜ)).Colorable (k - K.card)
/-- The paper's definition of `(s,t)`-splittability, expressed with
mathlib's chromatic number. -/
def Splittable (G : SimpleGraph V) (s t : ℕ) : Prop :=
∃ S : Set V,
(s : ℕ∞) ≤ (G.induce S).chromaticNumber ∧
(t : ℕ∞) ≤ (G.induce Sᶜ).chromaticNumber
/-- A deliberately naive two-set partition restatement of the paper's
definition, used to validate `Splittable`. -/
def SplittablePartition (G : SimpleGraph V) (s t : ℕ) : Prop :=
∃ S T : Set V,
S ∩ T = ∅ ∧ S ∪ T = Set.univ ∧
(s : ℕ∞) ≤ (G.induce S).chromaticNumber ∧
(t : ℕ∞) ≤ (G.induce T).chromaticNumber
theorem splittable_iff_partition {G : SimpleGraph V} {s t : ℕ} :
Splittable G s t ↔ SplittablePartition G s t := by
constructor
· rintro ⟨S, hS, hT⟩
exact ⟨S, Sᶜ, by ext; simp, by ext; simp, hS, hT⟩
· rintro ⟨S, T, hdisj, hunion, hS, hT⟩
have hTc : T = Sᶜ := by
ext x
constructor
· intro hxT hxS
have : x ∈ S ∩ T := ⟨hxS, hxT⟩
rw [hdisj] at this
exact this
· intro hxS
have hxU : x ∈ S ∪ T := by rw [hunion]; trivial
exact hxU.resolve_left hxS
subst T
exact ⟨S, hS, hT⟩
theorem Splittable.symm {G : SimpleGraph V} {s t : ℕ}
(h : Splittable G s t) : Splittable G t s := by
obtain ⟨S, hS, hSc⟩ := h
refine ⟨Sᶜ, hSc, ?_⟩
rw [compl_compl]
exact hS
theorem not_colorable_pred_iff_le_chromaticNumber {G : SimpleGraph V}
{n : ℕ} (hn : 1 ≤ n) :
(¬G.Colorable (n - 1)) ↔ (n : ℕ∞) ≤ G.chromaticNumber := by
rw [le_chromaticNumber_iff_colorable]
constructor
· intro h m hm
by_contra hmn
have hmle : m ≤ n - 1 := by omega
exact h (hm.mono hmle)
· intro h hc
exact (Nat.not_le_of_lt (by omega)) (h (n - 1) hc)
theorem Splittable.of_embedding {W : Type*} {H : SimpleGraph W}
{G : SimpleGraph V} {s t : ℕ} (f : H ↪g G)
(h : Splittable H s t) : Splittable G s t := by
obtain ⟨A, hA, hAc⟩ := h
let B : Set V := f '' A
let fA : H.induce A →g G.induce B :=
{ toFun := fun x ↦ ⟨f x, ⟨x, x.property, rfl⟩⟩
map_rel' := by
intro x y hxy
exact f.map_adj_iff.mpr hxy }
let fAc : H.induce Aᶜ →g G.induce Bᶜ :=
{ toFun := fun x ↦
⟨f x, by
intro hx
obtain ⟨a, ha, hfa⟩ := hx
have hax : a = x := f.injective hfa
exact x.property (hax ▸ ha)⟩
map_rel' := by
intro x y hxy
exact f.map_adj_iff.mpr hxy }
refine ⟨B, hA.trans (chromaticNumber_mono_of_hom fA),
hAc.trans ?_⟩
exact chromaticNumber_mono_of_hom fAc
theorem splittable_of_tihany_clique {G : SimpleGraph V}
{k s t : ℕ} (hs : 1 ≤ s) (ht : 1 ≤ t)
(hk : k = s + t - 1) {K : Finset V}
(hKcard : K.card = s) (hT : IsTihanyAt G k K) :
Splittable G s t := by
refine ⟨(K : Set V), ?_, ?_⟩
· rw [G.induce_eq_top.mpr hT.1, chromaticNumber_top]
simpa [hKcard]
· apply (not_colorable_pred_iff_le_chromaticNumber ht).mp
have hsub : k - K.card = t - 1 := by omega
simpa [hsub] using hT.2
/-- A hole is represented by an induced copy of a cycle graph. -/
def EvenHoleFree (G : SimpleGraph V) : Prop :=
∀ n : ℕ, Even n → 4 ≤ n → ¬(cycleGraph n ⊴ G)
/-- Naive formulation: no induced vertex set is isomorphic to an even
cycle of length at least four. -/
def EvenHoleFreeNaive (G : SimpleGraph V) : Prop :=
∀ n : ℕ, Even n → 4 ≤ n → ∀ S : Set V,
¬Nonempty (cycleGraph n ≃g G.induce S)
theorem evenHoleFree_iff_naive {G : SimpleGraph V} :
EvenHoleFree G ↔ EvenHoleFreeNaive G := by
simp only [EvenHoleFree, EvenHoleFreeNaive,
isIndContained_iff_exists_iso_induce, not_exists]
/-- The standard induced-`C₄`-free condition. -/
def C4Free (G : SimpleGraph V) : Prop :=
¬(cycleGraph 4 ⊴ G)
theorem C4Free.induce {G : SimpleGraph V} (hG : C4Free G)
(S : Set V) : C4Free (G.induce S) := by
intro h
exact hG (h.trans ⟨Embedding.induce S⟩)
theorem EvenHoleFree.c4Free {G : SimpleGraph V} (hG : EvenHoleFree G) :
C4Free G :=
hG 4 (by decide) (by omega)
theorem EvenHoleFree.induce {G : SimpleGraph V} (hG : EvenHoleFree G)
(S : Set V) : EvenHoleFree (G.induce S) := by
intro n hn hn4 hcycle
exact hG n hn hn4 (hcycle.trans ⟨Embedding.induce S⟩)
/-- The exact part of the Chudnovsky--Seymour structural theorem used by
the paper. Its chromatic bound is deliberately omitted because the proof
does not use it. -/
def ChudnovskySeymourStatement : Prop :=
∀ (W : Type u) [Fintype W] (H : SimpleGraph W),
EvenHoleFree H → Nonempty W → ∃ v : W, Bisimplicial H v
/-! ## The `C₄` nesting argument -/
/-- In a `C₄`-free graph, the neighborhoods in one clique of two
vertices in a disjoint clique are comparable by inclusion. This is the
four-vertex argument at the start of Lemma 2.2. -/
theorem crossNeighborhoods_comparable {G : SimpleGraph V}
(hC4 : C4Free G) {A B : Finset V}
(hAB : Disjoint A B) (hA : G.IsClique A) (hB : G.IsClique B)
{x y : V} (hx : x ∈ A) (hy : y ∈ A) :
(∀ ⦃z⦄, z ∈ B → G.Adj x z → G.Adj y z) ∨
(∀ ⦃z⦄, z ∈ B → G.Adj y z → G.Adj x z) := by
classical
by_contra hcomp
push Not at hcomp
obtain ⟨z, hzB, hxz, hnyz⟩ := hcomp.1
obtain ⟨w, hwB, hyw, hnxw⟩ := hcomp.2
have hxy : G.Adj x y := hA hx hy (by
intro h
subst y
exact hnyz hxz)
have hzw : G.Adj z w := hB hzB hwB (by
intro h
subst w
exact hnxw hxz)
have hx_ne_z : x ≠ z := by
intro h
subst z
exact (Finset.disjoint_left.mp hAB hx hzB)
have hx_ne_w : x ≠ w := by
intro h
subst w
exact (Finset.disjoint_left.mp hAB hx hwB)
have hy_ne_z : y ≠ z := by
intro h
subst z
exact (Finset.disjoint_left.mp hAB hy hzB)
have hy_ne_w : y ≠ w := by
intro h
subst w
exact (Finset.disjoint_left.mp hAB hy hwB)
have hx_ne_y : x ≠ y := G.ne_of_adj hxy
have hz_ne_w : z ≠ w := G.ne_of_adj hzw
have hyx : G.Adj y x := (G.adj_comm x y).mp hxy
have hzx : G.Adj z x := (G.adj_comm x z).mp hxz
have hwy : G.Adj w y := (G.adj_comm y w).mp hyw
have hwz : G.Adj w z := (G.adj_comm z w).mp hzw
have hnwx : ¬G.Adj w x := fun h ↦ hnxw ((G.adj_comm x w).mpr h)
have hnzy : ¬G.Adj z y := fun h ↦ hnyz ((G.adj_comm y z).mpr h)
apply hC4
let g : Fin 4 → V := fun i ↦ ![x, z, w, y] i
let f : cycleGraph 4 ↪g G :=
{ toFun := g
inj' := by
intro i j hij
fin_cases i <;> fin_cases j <;>
simp_all [g]
map_rel_iff' := by
intro i j
change G.Adj (g i) (g j) ↔ (cycleGraph 4).Adj i j
fin_cases i <;> fin_cases j <;>
norm_num [g, cycleGraph_adj, Fin.ext_iff] <;>
simp_all [G.adj_comm] <;> decide }
exact ⟨f⟩
/-- The structural content of Lemma 2.2: for every admissible `r` there
is an `(r+1)`-clique through `v` whose common neighborhood is a clique. -/
theorem exists_clique_with_clique_commonNeighbors {G : SimpleGraph V}
(hC4 : C4Free G) {v : V} {A B : Finset V}
(hAB : Disjoint A B) (hA : G.IsClique A) (hB : G.IsClique B)
(hn : ((A ∪ B : Finset V) : Set V) = G.neighborSet v)
{r : ℕ} (hr : 1 ≤ r) (hrA : r ≤ A.card) :
∃ K : Finset V,
K ⊆ insert v A ∧ K.card = r + 1 ∧ v ∈ K ∧
G.IsClique K ∧ G.IsClique (commonNeighbors G K) := by
classical
let NB : V → Finset V := fun a ↦ B.filter (G.Adj a)
have hAne : A.Nonempty := card_pos.mp (lt_of_lt_of_le (by omega) hrA)
obtain ⟨a₀, ha₀A, ha₀min⟩ :=
A.exists_min_image (fun a ↦ (NB a).card) hAne
have hNBmin : ∀ a ∈ A, NB a₀ ⊆ NB a := by
intro a haA
rcases crossNeighborhoods_comparable hC4 hAB hA hB ha₀A haA with h | h
· intro z hz
rw [mem_filter] at hz ⊢
exact ⟨hz.1, h hz.1 hz.2⟩
· have hsub : NB a ⊆ NB a₀ := by
intro z hz
rw [mem_filter] at hz ⊢
exact ⟨hz.1, h hz.1 hz.2⟩
have heq : NB a = NB a₀ :=
Finset.eq_of_subset_of_card_le hsub (ha₀min a haA)
exact heq.symm.subset
obtain ⟨R, ha₀R, hRA, hRcard⟩ :=
Finset.exists_subsuperset_card_eq
(show ({a₀} : Finset V) ⊆ A by simpa)
(by simpa using hr) hrA
have hvA : v ∉ A := by
intro hvA
exact G.loopless.irrefl v (by
rw [← mem_neighborSet, ← hn]
simp [hvA])
have hv_adj_A : ∀ a ∈ A, G.Adj v a := by
intro a ha
rw [← mem_neighborSet, ← hn]
simp [ha]
let K := insert v R
have hvR : v ∉ R := fun hv ↦ hvA (hRA hv)
have hKcard : K.card = r + 1 := by
simp [K, hvR, hRcard]
have hvK : v ∈ K := by simp [K]
have hKsub : K ⊆ insert v A := by
intro x hx
rcases Finset.mem_insert.mp hx with rfl | hx
· exact Finset.mem_insert_self ..
· exact Finset.mem_insert_of_mem (hRA hx)
have hKclique : G.IsClique K := by
dsimp only [K]
rw [Finset.coe_insert]
apply (hA.subset (by simpa only [Finset.coe_subset] using hRA)).insert
intro b hb _
exact hv_adj_A b (hRA (by simpa using hb))
refine ⟨K, hKsub, hKcard, hvK, hKclique, ?_⟩
intro x hx y hy hxy
have hxv : G.Adj x v := hx.2 v hvK
have hyv : G.Adj y v := hy.2 v hvK
have hxAB : x ∈ A ∨ x ∈ B := by
have : x ∈ G.neighborSet v := by
rw [mem_neighborSet]
exact (G.adj_comm v x).mpr hxv
rw [← hn] at this
simpa using this
have hyAB : y ∈ A ∨ y ∈ B := by
have : y ∈ G.neighborSet v := by
rw [mem_neighborSet]
exact (G.adj_comm v y).mpr hyv
rw [← hn] at this
simpa using this
rcases hxAB with hxA | hxB <;> rcases hyAB with hyA | hyB
· exact hA hxA hyA hxy
· have ha₀K : a₀ ∈ K := by
dsimp only [K]
exact mem_insert_of_mem (ha₀R (by simp))
have hy_a₀ : G.Adj y a₀ := hy.2 a₀ ha₀K
have hyNB : y ∈ NB a₀ := by
rw [mem_filter]
exact ⟨hyB, (G.adj_comm a₀ y).mpr hy_a₀⟩
exact (mem_filter.mp (hNBmin x hxA hyNB)).2
· have ha₀K : a₀ ∈ K := by
dsimp only [K]
exact mem_insert_of_mem (ha₀R (by simp))
have hx_a₀ : G.Adj x a₀ := hx.2 a₀ ha₀K
have hxNB : x ∈ NB a₀ := by
rw [mem_filter]
exact ⟨hxB, (G.adj_comm a₀ x).mpr hx_a₀⟩
exact (G.adj_comm x y).mpr
(mem_filter.mp (hNBmin y hyA hxNB)).2
· exact hB hxB hyB hxy
/-! ## Lemma 2.1 -/
/-- If one color class in a coloring of `G-K` has no vertex complete to
`K`, that coloring can be combined with the vertices of `K` while
saving one color. -/
theorem colorable_of_missing_commonNeighbor {G : SimpleGraph V}
{K : Finset V} {r : ℕ}
(C : (G.induce {x : V | x ∉ K}).Coloring (Fin r)) (i : Fin r)
(hmissing : ¬∃ w : {x : V // x ∉ K},
C w = i ∧ (w : V) ∈ commonNeighbors G K) :
G.Colorable (K.card + r - 1) := by
classical
have hex (w : {x : V // x ∉ K}) (hw : C w = i) :
∃ a ∈ K, ¬G.Adj (w : V) a := by
by_contra h
push Not at h
exact hmissing ⟨w, hw, w.property, h⟩
let pick : ∀ (w : {x : V // x ∉ K}), C w = i → K :=
fun w hw ↦ ⟨(hex w hw).choose, (hex w hw).choose_spec.1⟩
have pick_nonadj (w : {x : V // x ∉ K}) (hw : C w = i) :
¬G.Adj (w : V) (pick w hw : V) :=
(hex w hw).choose_spec.2
let out (x : V) (hx : x ∉ K) : {x : V // x ∉ K} := ⟨x, hx⟩
let color : V → (K ⊕ {j : Fin r // j ≠ i}) := fun x ↦
if hx : x ∈ K then
Sum.inl ⟨x, hx⟩
else
if hc : C (out x hx) = i then
Sum.inl (pick (out x hx) hc)
else
Sum.inr ⟨C (out x hx), hc⟩
let D : G.Coloring (K ⊕ {j : Fin r // j ≠ i}) :=
Coloring.mk color (by
intro x y hxy
intro heq
by_cases hx : x ∈ K
· by_cases hy : y ∈ K
· have hxy' : x = y := by
have heq' : (⟨x, hx⟩ : K) = (⟨y, hy⟩ : K) := by
simpa [color, hx, hy] using heq
exact congrArg Subtype.val heq'
exact G.ne_of_adj hxy hxy'
· by_cases hcy : C (out y hy) = i
· have heq' : (⟨x, hx⟩ : K) = pick (out y hy) hcy := by
simpa [color, hx, hy, hcy] using heq
apply pick_nonadj (out y hy) hcy
have hyx : G.Adj y x := G.adj_symm hxy
simpa [out, ← congrArg Subtype.val heq'] using hyx
· simp [color, hx, hy, hcy] at heq
· by_cases hy : y ∈ K
· by_cases hcx : C (out x hx) = i
· have heq' : pick (out x hx) hcx = (⟨y, hy⟩ : K) := by
simpa [color, hx, hy, hcx] using heq
apply pick_nonadj (out x hx) hcx
simpa [out, congrArg Subtype.val heq'] using hxy
· simp [color, hx, hy, hcx] at heq
· have hvalid : C (out x hx) ≠ C (out y hy) :=
C.valid hxy
by_cases hcx : C (out x hx) = i
· by_cases hcy : C (out y hy) = i
· exact hvalid (hcx.trans hcy.symm)
· simp [color, hx, hy, hcx, hcy] at heq
· by_cases hcy : C (out y hy) = i
· simp [color, hx, hy, hcx, hcy] at heq
· apply hvalid
have heq' :
(⟨C (out x hx), hcx⟩ : {j : Fin r // j ≠ i}) =
⟨C (out y hy), hcy⟩ := by
simpa [color, hx, hy, hcx, hcy] using heq
exact congrArg Subtype.val heq')
have hcard :
Fintype.card (K ⊕ {j : Fin r // j ≠ i}) = K.card + r - 1 := by
simp only [Fintype.card_sum, Fintype.card_coe,
Fintype.card_subtype_compl, Fintype.card_fin]
have : Fintype.card {j : Fin r // j = i} = 1 := Fintype.card_unique
rw [this]
have hi := i.isLt
exact (Nat.add_sub_assoc (by omega : 1 ≤ r) K.card).symm
rw [← hcard]
exact D.colorable
/-- Lemma 2.1 in finite-coloring form. -/
theorem clique_isTihanyAt {G : SimpleGraph V} {k : ℕ}
(hcol : G.Colorable k) (hncol : ¬G.Colorable (k - 1))
(hfree : G.CliqueFree k) {K : Finset V}
(hK : G.IsClique K)
(hcommon : G.IsClique (commonNeighbors G K)) :
IsTihanyAt G k K := by
classical
refine ⟨hK, ?_⟩
intro hcompColorable
have hKle : K.card ≤ k := hK.card_le_of_colorable hcol
have hKlt : K.card < k := by
apply lt_of_le_of_ne hKle
intro heq
exact hfree K ⟨hK, heq⟩
let r := k - K.card
have hr : 1 ≤ r := by omega
let C : (G.induce {x : V | x ∉ K}).Coloring (Fin r) := by
exact hcompColorable.some
have hfound (i : Fin r) :
∃ w : {x : V // x ∉ K},
C w = i ∧ (w : V) ∈ commonNeighbors G K := by
by_contra hmissing
apply hncol
have hc := colorable_of_missing_commonNeighbor C i hmissing
convert hc using 1
dsimp only [r] at *
omega
let w : Fin r → {x : V // x ∉ K} := fun i ↦ (hfound i).choose
have hwcolor (i : Fin r) : C (w i) = i := (hfound i).choose_spec.1
have hwcommon (i : Fin r) :
(w i : V) ∈ commonNeighbors G K := (hfound i).choose_spec.2
let f : Fin r → V := fun i ↦ w i
have hf_inj : Function.Injective f := by
intro i j hij
have hwij : w i = w j := Subtype.ext hij
calc
i = C (w i) := (hwcolor i).symm
_ = C (w j) := congrArg C hwij
_ = j := hwcolor j
let R : Finset V := Finset.univ.image f
have hRcard : R.card = r := by
rw [show R = Finset.univ.image f from rfl,
Finset.card_image_of_injective _ hf_inj, Finset.card_univ,
Fintype.card_fin]
have hRcommon : ∀ x ∈ R, x ∈ commonNeighbors G K := by
intro x hx
rw [show R = Finset.univ.image f from rfl, Finset.mem_image] at hx
obtain ⟨i, _, rfl⟩ := hx
exact hwcommon i
have hKR : Disjoint K R := by
rw [Finset.disjoint_left]
intro x hxK hxR
exact (hRcommon x hxR).1 hxK
let L := K ∪ R
have hLcard : L.card = k := by
rw [show L = K ∪ R from rfl, Finset.card_union_of_disjoint hKR, hRcard]
exact Nat.add_sub_of_le hKle
have hLclique : G.IsClique L := by
intro x hx y hy hxy
have hx' : x ∈ K ∨ x ∈ R := by simpa [L] using hx
have hy' : y ∈ K ∨ y ∈ R := by simpa [L] using hy
rcases hx' with hxK | hxR <;> rcases hy' with hyK | hyR
· exact hK hxK hyK hxy
· exact (G.adj_comm x y).mpr ((hRcommon y hyR).2 x hxK)
· exact (hRcommon x hxR).2 y hyK
· exact hcommon (hRcommon x hxR) (hRcommon y hyR) hxy
exact hfree L ⟨hLclique, hLcard⟩
/-- Lemma 2.2, with Lemma 2.1 applied to its output. -/
theorem exists_tihany_clique {G : SimpleGraph V} {k r : ℕ}
(hcol : G.Colorable k) (hncol : ¬G.Colorable (k - 1))
(hfree : G.CliqueFree k) (hC4 : C4Free G)
{v : V} {A B : Finset V}
(hAB : Disjoint A B) (hA : G.IsClique A) (hB : G.IsClique B)
(hn : ((A ∪ B : Finset V) : Set V) = G.neighborSet v)
(hr : 1 ≤ r) (hrA : r ≤ A.card) :
∃ K : Finset V,
K ⊆ insert v A ∧ K.card = r + 1 ∧ v ∈ K ∧
IsTihanyAt G k K := by
obtain ⟨K, hKsub, hKcard, hvK, hK, hcommon⟩ :=
exists_clique_with_clique_commonNeighbors hC4 hAB hA hB hn hr hrA
exact ⟨K, hKsub, hKcard, hvK,
clique_isTihanyAt hcol hncol hfree hK hcommon⟩
/-! ## Critical induced subgraphs -/
/-- The standard critical-graph degree argument: if deleting `v` is
`k`-colorable and `v` has fewer than `k` neighbors, the coloring extends
to all of `G`. -/
theorem colorable_of_delete_colorable_of_degree_lt {G : SimpleGraph V}
{v : V} {k : ℕ}
[Fintype (G.neighborSet v)]
(hdelete : (G.induce {x : V | x ≠ v}).Colorable k)
(hdegree : G.degree v < k) : G.Colorable k := by
classical
let C : (G.induce {x : V | x ≠ v}).Coloring (Fin k) := hdelete.some
let neighborColor : G.neighborFinset v → Fin k := fun x ↦
C ⟨x, (G.ne_of_adj (by simpa only [mem_neighborFinset] using x.property)).symm⟩
let used : Finset (Fin k) := Finset.univ.image neighborColor
have hused : used.card < k := by
calc
used.card ≤ (Finset.univ : Finset (G.neighborFinset v)).card :=
Finset.card_image_le
_ = G.degree v := by
simp only [Finset.card_univ, Fintype.card_coe, SimpleGraph.degree]
_ < k := hdegree
have hdiff : ((Finset.univ : Finset (Fin k)) \ used).Nonempty := by
apply Finset.sdiff_nonempty_of_card_lt_card
simpa using hused
let i : Fin k := hdiff.choose
have hi : i ∉ used := (Finset.mem_sdiff.mp hdiff.choose_spec).2
let color : V → Fin k := fun x ↦ if hx : x = v then i else C ⟨x, hx⟩
refine ⟨Coloring.mk color ?_⟩
intro x y hxy
by_cases hx : x = v
· subst x
have hy : y ≠ v := by
intro h
subst y
exact G.irrefl hxy
intro heq
have heq' : i = C ⟨y, hy⟩ := by
simpa [color, hy] using heq
apply hi
rw [show used = Finset.univ.image neighborColor from rfl, Finset.mem_image]
refine ⟨⟨y, by simpa using hxy⟩, Finset.mem_univ _, ?_⟩
change C ⟨y, _⟩ = i
simpa using heq'.symm
· by_cases hy : y = v
· subst y
intro heq
have heq' : C ⟨x, hx⟩ = i := by
simpa [color, hx] using heq
apply hi
rw [show used = Finset.univ.image neighborColor from rfl, Finset.mem_image]
refine ⟨⟨x, by simpa [G.adj_comm] using hxy⟩, Finset.mem_univ _, ?_⟩
change C ⟨x, _⟩ = i
simpa using heq'
· simpa [color, hx, hy] using
C.valid (v := ⟨x, hx⟩) (w := ⟨y, hy⟩) hxy
/-- Every finite non-`(k-1)`-colorable graph has a vertex-critical
induced subgraph. -/
theorem exists_vertexCritical_induced {G : SimpleGraph V} {k : ℕ}
(hncol : ¬G.Colorable (k - 1)) :
∃ S : Finset V,
S.Nonempty ∧
¬(G.induce (S : Set V)).Colorable (k - 1) ∧
∀ v : S,
((G.induce (S : Set V)).induce {x : S | x ≠ v}).Colorable (k - 1) := by
classical
let candidates : Finset (Finset V) :=
Finset.univ.powerset.filter
(fun S ↦ ¬(G.induce (S : Set V)).Colorable (k - 1))
have hcandidates : candidates.Nonempty := by
refine ⟨Finset.univ, ?_⟩
rw [show candidates =
(Finset.univ : Finset V).powerset.filter
(fun S : Finset V ↦ ¬(G.induce (S : Set V)).Colorable (k - 1)) from rfl,
Finset.mem_filter]
refine ⟨by simp, ?_⟩
intro hc
apply hncol
apply Colorable.of_hom (induceUnivIso G).symm.toHom
have heq : ((Finset.univ : Finset V) : Set V) = Set.univ := by
ext
simp
rw [heq] at hc
exact hc
obtain ⟨S, hScandidate, hSmin⟩ :=
candidates.exists_min_image Finset.card hcandidates
have hSsub : S ⊆ Finset.univ := by simp
have hnS : ¬(G.induce (S : Set V)).Colorable (k - 1) := by
simpa [candidates] using hScandidate
have hSne : S.Nonempty := by
by_contra h
rw [Finset.not_nonempty_iff_eq_empty] at h
subst S
apply hnS
letI : IsEmpty {x : V // x ∈ ((∅ : Finset V) : Set V)} :=
⟨fun x ↦ by simpa using x.property⟩
exact Colorable.of_isEmpty _
refine ⟨S, hSne, hnS, ?_⟩
intro v
have herase :
(G.induce ((S.erase v : Finset V) : Set V)).Colorable (k - 1) := by
by_contra hnot
have heraseCandidate : S.erase v ∈ candidates := by
simp [candidates, hnot]
have hle := hSmin (S.erase v) heraseCandidate
have hvS : (v : V) ∈ S := v.property
exact (Nat.not_le_of_lt (Finset.card_erase_lt_of_mem hvS)) hle
let f :
(G.induce (S : Set V)).induce {x : S | x ≠ v} →g
G.induce ((S.erase v : Finset V) : Set V) :=
{ toFun := fun x ↦
⟨(x : S),
Finset.mem_erase.mpr
⟨fun h ↦ x.property (Subtype.ext h), (x : S).property⟩⟩
map_rel' := by
intro x y hxy
exact hxy }
exact Colorable.of_hom f herase
/-! ## Theorem 1.4 -/
/-- Theorem 1.4 in the equivalent finite-coloring formulation of
`χ(G)=k` and `ω(G)<k`. -/
theorem theorem14_coloring {G : SimpleGraph V} {s t k : ℕ}
(hs : 2 ≤ s) (ht : 2 ≤ t) (hst : s ≤ t)
(hk : k = s + t - 1)
(hcol : G.Colorable k) (hncol : ¬G.Colorable (k - 1))
(hfree : G.CliqueFree k) (hC4 : C4Free G)
(hbis : ∀ S : Set V, Nonempty S →
∃ v : S, Bisimplicial (G.induce S) v) :
Splittable G s t := by
classical
obtain ⟨S, hSne, hnH, hcritical⟩ :=
exists_vertexCritical_induced hncol
let H : SimpleGraph S := G.induce (S : Set V)
have hHcol : H.Colorable k :=
Colorable.of_hom (Embedding.induce (S : Set V)).toHom hcol
have hHfree : H.CliqueFree k :=
hfree.comap ⟨(Embedding.induce (S : Set V)).toCopy⟩
have hHC4 : C4Free H := hC4.induce (S : Set V)
have hSnonempty : Nonempty S := ⟨⟨hSne.choose, hSne.choose_spec⟩⟩
obtain ⟨v, hvbis⟩ := hbis (S : Set V) hSnonempty
obtain ⟨A, B, hAB, hA, hB, hn⟩ :=
(bisimplicial_iff_finset H v).mp hvbis
have finish (A B : Finset S)
(hAB : Disjoint A B) (hA : H.IsClique A) (hB : H.IsClique B)
(hn : (((A ∪ B : Finset S) : Set S)) = H.neighborSet v)
(hBA : B.card ≤ A.card) : Splittable H s t := by
letI : Fintype (H.neighborSet v) := Fintype.ofFinite _
have hdegree : k - 1 ≤ H.degree v := by
by_contra h
have hlt : H.degree v < k - 1 := Nat.lt_of_not_ge h
exact hnH
(colorable_of_delete_colorable_of_degree_lt
(hcritical v) hlt)
have hdegree_eq : H.degree v = A.card + B.card := by
rw [SimpleGraph.degree]
have heq : H.neighborFinset v = A ∪ B := by
ext x
rw [mem_neighborFinset, ← mem_neighborSet, ← hn]
simp
rw [heq, Finset.card_union_of_disjoint hAB]
have hAlarge : s - 1 ≤ A.card := by
omega
obtain ⟨K, _, hKcard, _, hT⟩ :=
exists_tihany_clique hHcol hnH hHfree hHC4 hAB hA hB hn
(by omega : 1 ≤ s - 1) hAlarge
apply splittable_of_tihany_clique (by omega) (by omega) hk
· calc
K.card = s - 1 + 1 := hKcard
_ = s := Nat.sub_add_cancel (by omega)
· exact hT
have hsplitH : Splittable H s t := by
rcases le_total B.card A.card with hBA | hABcard
· exact finish A B hAB hA hB hn hBA
· apply finish B A hAB.symm hB hA
· simpa [Finset.union_comm] using hn
· exact hABcard
exact Splittable.of_embedding (Embedding.induce (S : Set V)) hsplitH
/-- Theorem 1.4, stated with mathlib's chromatic number and clique
number exactly as in the paper. -/
theorem theorem14 {G : SimpleGraph V} {s t : ℕ}
(hs : 2 ≤ s) (ht : 2 ≤ t)
(homega : (G.cliqueNum : ℕ∞) < G.chromaticNumber)
(hchi : G.chromaticNumber = (s + t - 1 : ℕ))
(hC4 : C4Free G)
(hbis : ∀ S : Set V, Nonempty S →
∃ v : S, Bisimplicial (G.induce S) v) :
Splittable G s t := by
classical
let k := s + t - 1
have hkpos : 0 < k := by omega
have hcol : G.Colorable k := by
rw [← chromaticNumber_le_iff_colorable]
simpa [k, hchi]
have hncol : ¬G.Colorable (k - 1) := by
intro hc
have hle := hc.chromaticNumber_le
rw [hchi] at hle
have hlt : ((k - 1 : ℕ) : ℕ∞) < (k : ℕ) := by
exact_mod_cast (Nat.sub_lt (by omega) (by omega : 0 < 1))
exact hlt.not_ge (by simpa [k] using hle)
have homegaNat : G.cliqueNum < k := by
rw [hchi] at homega
exact_mod_cast homega
have hfree : G.CliqueFree k := by
intro K hK
have hle := hK.isClique.card_le_cliqueNum
rw [hK.card_eq] at hle
omega
rcases le_total s t with hst | hts
· exact theorem14_coloring hs ht hst rfl hcol hncol hfree hC4 hbis
· apply Splittable.symm
have hkcomm : k = t + s - 1 := by
dsimp only [k]
omega
exact theorem14_coloring ht hs hts hkcomm hcol hncol hfree hC4 hbis
/-- Theorem 1.5. The sole hypothesis not proved in this file is the
explicitly named Chudnovsky--Seymour structural theorem. -/
theorem theorem15 (hCS : ChudnovskySeymourStatement.{u})
{G : SimpleGraph V} {s t : ℕ}
(hs : 2 ≤ s) (ht : 2 ≤ t)
(homega : (G.cliqueNum : ℕ∞) < G.chromaticNumber)
(hchi : G.chromaticNumber = (s + t - 1 : ℕ))
(hehf : EvenHoleFree G) :
Splittable G s t := by
apply theorem14 hs ht homega hchi hehf.c4Free
intro S hS
letI : Fintype S := Fintype.ofFinite _
exact hCS S (G.induce S) (hehf.induce S) hS
end Tihany