Edge partitions / Graham-Pollak

Stream: graph theory

[Julian Berman]

At NYC Lean after a few weeks fighting with rearranging finset.sums we proved the Graham-Pollak theorem. In order to do so we needed edge partitions, which Mathlib doesn't have (Partition is vertex partitions) and I couldn't find any prior discussion of.

Is there a reason not to PR them, and to do so as below along with some API:

/-- An edge partition of a simple graph `G`. -/
@[ext]
structure EdgePartition (G : SimpleGraph V) where
  /-- `parts`: sets of subsets of the edges of `G`. -/
  parts : Set (Set G.edgeSet)
  /-- `isPartition`: a proof that `parts` is a proper partition of the edges. -/
  isPartition : Setoid.IsPartition parts

And then secondarily, is Graham-Pollak itself suitable for Mathlib, or is there a generalization of it which we would want instead? I don't know much graph theory but my quick googling seemed to suggest that generalizing too far away from it leads quickly to open problems... The statement we proved is:

/--
The Graham-Pollak theorem:

In a complete graph on `|V|` vertices, any edge partition into complete bipartite subgraphs has
at least `|V| - 1` parts.
-/
theorem card_le_card_parts_add_one_of_CompleteBipartite
  {E : (⊤ : SimpleGraph V).EdgePartition}
  [Fintype E.parts]
  (completeBipartiteOf : ∀ p, CompleteBipartite <| E.graph p) :
    card V ≤ card E.parts + 1 := sorry

[Snir Broshi]

I think docs#SimpleGraph.EdgeLabeling is equivalent to EdgePartition, though I'm not sure how to convert a function α → β to Set (Set α) + a proof of Setoid.IsPartition. Perhaps docs#Setoid.ker, or docs#Set.preimage of singletons ({ f ⁻¹' {b} | b : β }).
(EdgeLabeling was upstreamed for Ramsey's theorem)
The Wikipedia page links to Graph labeling, and it does seem vaguely similar to Ramsey stuff.
I prefer having just one definition (i.e. EdgeLabeling), and it also feels more constructive in some sense. Unless the Set (Set _)) version is easier to work with in some places?

[Julian Berman]

Aha, I indeed missed that definition, let's see if I can slot it in easily, thanks for the pointer.

[Snir Broshi]

I didn't know about docs#SimpleGraph.Partition, and in contrast to your EdgePartition they have a condition requiring every part is an independent set. So now I'm wondering:

• Why do we have an equivalent formulation of coloring? They were even added together (mathlib3#10287), and there are conversion functions between them (both ways).
• There seem to be 3 binary choices here which can make 8 possible definitions: vertex/edge, function/set-of-sets, whether to restrict it with a coloring-like condition.
  We have Coloring (001), Partition (011), EdgeLabeling (100), EdgeColoring (101) in PR, and you're suggesting EdgePartition (110).
  Should we have all 8? I'm not sure what to make of this

[Snir Broshi]

(my opinion is to deprecate Partition since it's old and doesn't seem used, whereas colorings are known to be useful concepts, and maybe a definition for EdgeLabeling is a bit weird but Ramsey theory is a great justification IMO)

[Julian Berman]

It seems like no matter what happens it'd be nice to sprinkle words like "decomposition" and "partition" into a few more docstrings to help whichever definitions remain be a bit easier to find.

[Julian Berman]

FWIW it turned out to be completely trivial to drop in EdgeLabeling, and the API / lemmas I'd written for our thing basically lined up more or less exactly with lemmas that existed for it.

What seems a bit less obvious to me still is how to handle the next bit, which is expressing complete bipartiteness. We have docs#SimpleGraph.IsCompleteMultipartite, but in our case we defined

def IsCompleteWith {ι : Type} (G : SimpleGraph V) (parts : ι → Set V) : Prop :=
  ∀ i, ∀ v ∈ parts i, ∀ j, i ≠ j → ∀ u ∈ parts j, G.Adj v u

structure CompleteBipartite (G : SimpleGraph V) where
  left : Set V
  right : Set V
  bipartite : G.IsBipartiteWith left right
  complete : G.IsCompleteWith ![left, right]

and worked with that -- I don't yet see an easy way to make use of IsCompleteMultipartite. I know Mathlib also currently has separate implementations of bipartite and multipartiteness for reasons I haven't fully digested yet.

[Julian Berman]

Possibly though we're close enough to a PR that I'll just file one and see what a reviewer recommends.

[Jakub Nowak]

You could try getting partition from SimpleGraph.IsCompleteMultipartite.setoid and Setoid.classes.

[Jakub Nowak]

Julian Berman said:

I know Mathlib also currently has separate implementations of bipartite and multipartiteness for reasons I haven't fully digested yet.

SimpleGraph.IsBipartite is just defined as 2-colorable in terms of SimpleGraph.Coloring. I think bipartite case is common enough in graph theory to justify having it, but maybe most of the theory about bipartite graphs generalizes to multipartite?

[Vlad Tsyrklevich]

IsCompleteMultipartite is not the right tool here because e.g. an edgeless graph is complete multipartite so you'd need IsBipartite + an additional hypothesis saying that every vertex has an edge to get complete bipartiteness. In this setting I think you want to define a IsCompleteMultipartiteWith s predicate where s is a partition of the vertices similarly to IsBipartite/IsBipartiteWith. Then you get an easy proof of IsBipartiteWith when #s = 2

[Vlad Tsyrklevich]

And I just realized that that is exactly what Julian's IsCompleteWith does, modulo the fact that it allows overlapping partitions. Overlapping partitions are impossible to realize anyways because simple graphs don't allow self-loops so perhaps the definition should be changed to force specifying a single partition for every element?

[Snir Broshi]

It also seems to allow edges inside each partition

[Snir Broshi]

We can do

def IsCompleteMultipartiteWith {V ι : Type*} (G : SimpleGraph V) (f : V → ι) : Prop :=
  ∀ u v, G.Adj u v ↔ f u ≠ f v

or equivalently

def IsCompleteMultipartiteWith {V ι : Type*} (G : SimpleGraph V) (f : V → ι) : Prop :=
  G.Adj = Ne.onFun f

[Jakub Nowak]

Snir Broshi said:

It also seems to allow edges inside each partition

You mean IsCompleteMultipartite? I think it doesn't? Partitions are equivalence classes where relation is contained in non-adjacency relation.

[Snir Broshi]

Jakub Nowak said:

Snir Broshi said:

It also seems to allow edges inside each partition

You mean IsCompleteMultipartite?

IsCompleteWith

[Julian Berman]

So would we add 3 (possibly 4 including CompleteMultipartite?) definitions:

def IsCompleteMultipartiteWith (f : V → ι) : Prop :=
  G.Adj = Ne.onFun f

def IsCompleteBipartiteWith (left : Set V) : Prop :=
  G.IsCompleteMultipartiteWith (· ∈ left)

def CompleteBipartite :=
  ∃ left, G.IsCompleteBipartiteWith left

I haven't fully fixed my proof yet but this seems to reasonably easily drop into it now if I restate a bunch of helper lemmas into API for these.

[Vlad Tsyrklevich]

I don't think I have a good enough sense for the mathlib-preferred design patterns to say. (I would prefer Snir's first definition to the second one though, I think it's harder to read and apply)

[Julian Berman]

I put up #34050 with the entirety of the fixed proof, even though it's not ready for merge yet clearly -- but the definitions above worked fairly well in the lemmas I needed -- more API is presumably needed before they're usable in general, so I'll split them off into a new PR most likely, but if anyone has immediate feedback who's helped me already here (or sees a mistake) feel free to let me know!

I would prefer Snir's first definition to the second one though, I think it's harder to read and apply

Not that I disagree strongly, what do I know, but the definition of IsCompleteMultipartite is already pretty obtuse, no? It's Transitive (¬ G.Adj · ·). I think as long as there's some sane lemma you can rewrite with to get to a G.Adj version quickly that it doesn't matter what the "real definition" is? (but tell me if you feel more sure than I am!)

[Julian Berman]

Also allow me to jump on the "oh god I love grind" bandwagon.

[Vlad Tsyrklevich]

Julian Berman said:

I think as long as there's some sane lemma you can rewrite with to get to a G.Adj version quickly that it doesn't matter what the "real definition" is? (but tell me if you feel more sure than I am!)

For users of the API sure, but I think it's easier to understand and has better defeqs for setting-up the theory so why not.

Also I agree that the definition IsCompleteMultipartite is unintuitive, but I'm not sure how one would make it clearer. I think the difficulty is that it's easiest to define a multipartite graph in terms of its complement being a sum of cliques and that's really what the definition means though it takes a bit to unravel it.

[Julian Berman]

Ah good I certainly had no intuition for which definition had better defeqs, I still don't know how to intuit that, but I'm certainly willing to trust you and try it.

[Vlad Tsyrklevich]

I think you can imagine being in the middle of a proof and saying "I have a hypothesis that u and v are in different partitions and I want to show they are adjacent" and now you just get that by (hmultipartite u v).mpr hpartitionne or the other way around without being forced to specifically use a chain of rewrites.

[Vlad Tsyrklevich]

or really the def should probably be ∀ ⦃u v : V⦄, ... so that you get hmultipartite.mpr hpartitionne