coloring/partitions

Stream: graph theory

[Arthur Paulino]

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]

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]

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

[Kyle Miller]

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

[Arthur Paulino]

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]

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

[Kyle Miller]

Are you wanting this?

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

[Arthur Paulino]

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

[Arthur Paulino]

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

[Kyle Miller]

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]

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]

@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]

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]

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]

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]

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

[Arthur Paulino]

The branch is updated with my latest commit

[Arthur Paulino]

Please feel free to adjust those last details :pray:

[Yakov Pechersky]

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]

Sorries are gone

[Kyle Miller]

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]

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]

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]

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]

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

[Arthur Paulino]

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]

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]

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

[Arthur Paulino]

@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]

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

[Kyle Miller]

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

[Arthur Paulino]

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]

Like an infinite clique, for instance

[Kyle Miller]

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

[Arthur Paulino]

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]

@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]

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

[Arthur Paulino]

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

[Eric Rodriguez]

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

[Arthur Paulino]

Kyle Miller said:

(want to PR them? :smile:)

Sure, np

[Eric Rodriguez]

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]

(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]

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]

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

[Arthur Paulino]

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]

Will do in a few minutes :+1:

[Mauricio Collares]

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]

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