# Zulip Chat Archive

## 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

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

Please feel free to adjust those last details :pray:

#### 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`

.

#### Kyle Miller (Nov 19 2021 at 04:53):

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?

Related: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

#### 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