Stream: graph theory

Topic: coloring/partitions

Arthur Paulino (Nov 18 2021 at 22:16):

I've created this definition of partitionable:

/-- Whether a graph can be partitioned in at most n parts. -/
def partitionable (n : ℕ) : Prop :=
∃ (P : G.partition), nonempty (P.parts ↪ fin n)


To prove this:

lemma partitionable_iff_colorable {n : ℕ} :
G.partitionable n ↔ G.colorable n :=
begin
split,
{ intro h,
cases h with P h,
obtain ⟨f⟩ := h,
have C := partition.to_coloring' P,
use G.recolor_of_embedding f C, },
{ rintro ⟨C⟩,
have P := partition.from_coloring C,
use [P, P.from_coloring_to_embedding C], },
end


Now I need to define this function:

/-- An embedding from the parts of a partition to the colors of a coloring -/
def from_coloring_to_embedding {α : Type v} (C : G.coloring α) : P.parts ↪ α := sorry


Is it possible to do so?

Kyle Miller (Nov 18 2021 at 22:38):

That definition of partitionable seems like a reasonable way to encode the idea. I wonder though if it'd be easier to work with down the line if it used the docs#set.finite interface:

def partitionable (n : ℕ) : Prop :=
∃ (P : G.partition) (h : P.parts.finite), h.to_finset.card ≤ n


I'm not really sure, though, what's the most common way in mathlib of saying "this is a set with at most n elements."

Kyle Miller (Nov 18 2021 at 22:38):

For from_coloring_to_embedding, I think you need additional hypotheses on what P is.

Kyle Miller (Nov 18 2021 at 22:40):

P might have more independent sets than the number of color classes for C, and they might not me mergeable.

Arthur Paulino (Nov 18 2021 at 22:45):

Right, I had the impression that I lost important information with the abstraction

/-- Creates a partition from a coloring. -/
def from_coloring {α : Type v} (C : G.coloring α) : G.partition :=
begin
let parts : set (set V) := C.color_classes,
have is_partition : setoid.is_partition parts,
{ by apply coloring.color_classes_is_partition, },
have independent : ∀ (s ∈ parts), is_antichain G.adj s,
{ by apply coloring.color_classes_is_independent, },
exact partition.mk parts is_partition independent,
end


Arthur Paulino (Nov 18 2021 at 22:46):

I want P.parts to be exactly the color classes themselves

Kyle Miller (Nov 18 2021 at 22:48):

Are you wanting this?

def from_coloring_to_embedding {α : Type v} (C : G.coloring α) :
(from_coloring C).parts ↪ α := sorry


Arthur Paulino (Nov 18 2021 at 22:49):

Hm, I think so. Lemme try to plug that in

Arthur Paulino (Nov 18 2021 at 22:55):

use [P, P.from_coloring_to_embedding C] is no longer accepted tho

Kyle Miller (Nov 18 2021 at 22:55):

Also, here's something that still needs design: how to express "this is a partition with at most n parts." There's not really a way to say "let P be a bipartition" directly.

I'd thought about making P.parts be a finset, so it could be (P : G.partition) (h : P.parts.card <= 2), but that seems unnecessarily restrictive.

Leaving it as a set, another option is a predicate (not sure what to call it) like P.parts_card_le 2

Arthur Paulino (Nov 18 2021 at 23:00):

I like the predicate idea more because it's more symmetrical with the idea of a coloring (no restrictions on the number of colors)

Arthur Paulino (Nov 19 2021 at 03:03):

@Kyle Miller Alright I think I've iterated on all of your comments, but there are some unfortunate sorrys in the way (I'm a bit exhaust)

Arthur Paulino (Nov 19 2021 at 03:03):

here

lemma coloring.mem_color_classes {v : V} : C.color_class (C v) ∈ C.color_classes :=
begin
use v,
let aa := C.mem_color_class v,
sorry,
end

lemma coloring.color_classes_is_independent :
∀ (s ∈ C.color_classes), is_antichain G.adj s :=
begin
intros s hs v hv w hw hnvw,
sorry,
end


Arthur Paulino (Nov 19 2021 at 03:03):

And I couldn't make the conversation from earlier come true:

def from_coloring_to_embedding {α : Type v} (C : G.coloring α) : P.parts ↪ α := sorry


Arthur Paulino (Nov 19 2021 at 03:06):

This version is useful because it's exactly what's expected in a proof in the context of partitions:

lemma coloring.color_classes_is_independent :
∀ (s ∈ C.color_classes), is_antichain G.adj s


Arthur Paulino (Nov 19 2021 at 03:07):

but I couldn't prove it after changing the definition of color_classes to (setoid.ker C).classes

Arthur Paulino (Nov 19 2021 at 03:09):

The branch is updated with my latest commit

Yakov Pechersky (Nov 19 2021 at 04:50):

Arthur, you can't computably eliminate from Prop into data. You only have the Prop that such an embedding exists (nonempty _), but you can't unwrap that nonempty hypothesis directly into data on its own. Of course, inside a proof, you can use tactic like rcases or obtain to retrieve a possible such embedding, so you might not need an explicit definition of from_coloring_to_embedding.

Sorries are gone

Kyle Miller (Nov 19 2021 at 04:55):

I'm not sure how from_coloring_to_embedding was supposed to work, so I deleted it. (It still lives on in a git commit and in this conversation.)

Kyle Miller (Nov 19 2021 at 04:58):

If anyone wants to figure out where they should go, what they should be called, or how to write them better, there are some lemmas about cardinalities about setoid.ker and set.range: https://github.com/leanprover-community/mathlib/blob/70b66747bd72293939b22546215808d1f72c508f/src/combinatorics/simple_graph/coloring.lean#L103-L147 (pr: #10287)

Yakov Pechersky (Nov 19 2021 at 04:59):

Some syntax clean-up:

  { rintro ⟨C⟩,
refine ⟨C.to_partition, C.color_classes_finite_of_fintype, le_trans _ (fintype.card_fin n).le⟩,
generalize_proofs h,
haveI : fintype C.color_classes := C.color_classes_finite_of_fintype.fintype,
rw h.card_to_finset,
exact C.card_color_classes_le },


Yakov Pechersky (Nov 19 2021 at 05:09):

Is something like this more general?

lemma fintype.card_le_of_surjective {α β : Type*} [fintype α] [fintype β] (f : α → β)
(h : function.surjective f): fintype.card β ≤ fintype.card α :=
begin
let g : set.range f → α := λ y, y.2.some,
have : function.injective g,
{ rintros ⟨x, hx⟩ ⟨x', hx'⟩,
simp only [g],
have h := hx.some_spec,
have h' := hx'.some_spec,
intro he,
rw [he, h'] at h,
simp [h], },
classical,
haveI : fintype (set.range f) := subtype.fintype _,
refine le_trans (le_of_eq _) (fintype.card_le_of_injective _ this),
refine fintype.card_congr _,
exact (equiv.subtype_univ_equiv h).symm
end

-- TODO move to correct place
lemma fintype.card_range_le {α β : Type*} (f : α → β) [fintype α] [fintype (set.range f)] :
fintype.card (set.range f) ≤ fintype.card α :=
fintype.card_le_of_surjective (λ a, ⟨f a, by simp⟩) (λ ⟨_, a, ha⟩, ⟨a, ha⟩)


Kyle Miller (Nov 19 2021 at 05:16):

Oh, I should have looked for docs#fintype.card_le_of_surjective

Arthur Paulino (Nov 19 2021 at 13:34):

Amazing! I'm going to backtrack your guys' ideas and try to wrap my head around them. My learning is skyrocketing. Thanks a lot

Arthur Paulino (Nov 19 2021 at 13:35):

Amazing! I'm going to backtrack your guys' ideas and try to wrap my head around them. My learning is skyrocketing. Thanks a lot

Arthur Paulino (Nov 19 2021 at 17:31):

@Kyle Miller I've pushed this commit to the branch

Arthur Paulino (Jan 18 2022 at 22:40):

@Kyle Miller doesn't this definition bother you a bit though? It bugs me because the chromatic number is something we want to minimize

Arthur Paulino (Jan 18 2022 at 22:41):

It seems to me that it should be applied to finite graphs, only

Kyle Miller (Jan 18 2022 at 22:42):

There's theory about colorability of infinite graphs with finitely many colors

Arthur Paulino (Jan 18 2022 at 22:43):

So is it consistent with the literature that infinite graphs that can't be colored with a finite number of colors have chromatic number equal to zero?

Arthur Paulino (Jan 18 2022 at 22:43):

Like an infinite clique, for instance

Kyle Miller (Jan 18 2022 at 22:45):

Oh, no, 0 is junk data I'm pretty sure.

Arthur Paulino (Jan 18 2022 at 22:46):

But then are we currently able to prove that the chromatic number of an infinite clique is 0? (I think I've finally formulated my question properly)

Kyle Miller (Jan 18 2022 at 23:33):

@Arthur Paulino Excellent question. It's possible, but it takes some missing lemmas (want to PR them? :smile:)

import combinatorics.simple_graph.coloring
import tactic

namespace simple_graph

lemma colorable_of_zero_le_chromatic_number {V : Type*} {G : simple_graph V}
(h : 0 < G.chromatic_number) :
G.colorable G.chromatic_number :=
begin
obtain ⟨h, hn⟩ := nat.nonempty_of_pos_Inf h,
exact colorable_chromatic_number hn,
end

lemma colorable_of_embedding {V V' : Type*} {G : simple_graph V} {G' : simple_graph V'}
(f : G ↪g G') {n : ℕ} (h : G'.colorable n) : G.colorable n :=
begin
have c : G'.coloring (fin n) := h.to_coloring (by simp),
exact ⟨c.comp f⟩,
end

/- replace chromatic_number_le_of_forall_imp with this -/
lemma chromatic_number_le_of_forall_imp' {V V' : Type*} {G : simple_graph V} {G' : simple_graph V'}
{m : ℕ} (hc : G'.colorable m)
(h : ∀ n, G'.colorable n → G.colorable n) :
G.chromatic_number ≤ G'.chromatic_number :=
begin
apply cInf_le chromatic_number_bdd_below,
apply h,
apply colorable_chromatic_number hc,
end

lemma chromatic_number_le_of_embedding {V V' : Type*} {G : simple_graph V} {G' : simple_graph V'}
(f : G ↪g G') {n : ℕ} (h : G'.colorable n) :
G.chromatic_number ≤ G'.chromatic_number :=
chromatic_number_le_of_forall_imp' h (λ _, colorable_of_embedding f)

lemma chromatic_number_top_eq_zero_of_infinite (V : Type*) [infinite V] :
(⊤ : simple_graph V).chromatic_number = 0 :=
begin
set n := (⊤ : simple_graph V).chromatic_number,
by_contra hc,
replace hc := pos_iff_ne_zero.mpr hc,
have : n + 1 ≤ (⊤ : simple_graph V).chromatic_number,
{ convert_to (⊤ : simple_graph {m | m < n + 1}).chromatic_number ≤ _,
{ simp [chromatic_number_complete_graph], },
refine chromatic_number_le_of_embedding _ (colorable_of_zero_le_chromatic_number hc),
apply embedding.complete_graph.of_embedding,
exact (function.embedding.subtype _).trans (infinite.nat_embedding V), },
exact nat.not_succ_le_self _ this,
end

end simple_graph


Kyle Miller (Jan 18 2022 at 23:33):

I didn't simplify the last lemma's proof.

Arthur Paulino (Jan 18 2022 at 23:34):

Wait, isn't this a hole? Shouldn't we tweak the definition of chromatic number to forbid this strangeness?

Eric Rodriguez (Jan 18 2022 at 23:35):

this is pretty common in mathlib. order_of (2 : ℤ) = 0. nat.card ℕ = 0. it's a nice throw-away value

Arthur Paulino (Jan 18 2022 at 23:42):

Kyle Miller said:

(want to PR them? :smile:)

Sure, np

Eric Rodriguez (Jan 18 2022 at 23:43):

and because this is so widespread, it works well together, too; the monoid.exponent of a cyclic group is equal to its nat.card, same with the chromatic_number of a complete graph

Eric Rodriguez (Jan 18 2022 at 23:45):

(although usually we end up stating the results in terms of fintype/infinite anways because the proof ends up being fairly different, as you can see above & also in docs#is_cyclic.exponent_eq_card)

Arthur Paulino (Jan 18 2022 at 23:47):

Now I'm curious to see how this concept (hack?) first got into mathlib :joy:
Or is it a common practice in formalized mathematics?

Kyle Miller (Jan 18 2022 at 23:52):

(@Arthur Paulino I replaced the proof for chromatic_number_top_eq_zero_of_infinite with something a bit shorter.)

Arthur Paulino (Jan 18 2022 at 23:57):

I feel a bit awkward PR'ing something you authored 100%, but babysitting PRs is something I don't mind if you don't enjoy it very much

Arthur Paulino (Jan 18 2022 at 23:59):

Will do in a few minutes :+1:

Mauricio Collares (Jan 19 2022 at 00:20):

Arthur Paulino said:

Now I'm curious to see how this concept (hack?) first got into mathlib :joy:
Or is it a common practice in formalized mathematics?

Kyle Miller (Jan 19 2022 at 00:20):

(Oops, sorry about that Arthur. I'll PR it :+1:)

Last updated: Dec 20 2023 at 11:08 UTC