## 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: Aug 03 2023 at 10:10 UTC