Complete multipartite graphs

Stream: mathlib4

[Jeremy Tan]

A complete bipartite graph is currently defined in mathlib as

def completeBipartiteGraph (V W : Type*) : SimpleGraph (Sum V W)
    where
  Adj v w := v.isLeft ∧ w.isRight ∨ v.isRight ∧ w.isLeft
  symm := by
    intro v w
    cases v <;> cases w <;> simp
  loopless := by
    intro v
    cases v <;> simp

A note above this reads

TODO also introduce complete multi-partite graphs, where the vertex type is a sigma type of an
indexed family of vertex types

What is a "sigma type of an indexed family of vertex types"? And how would this extend to a definition of complete multipartite graphs?

[Notification Bot]

A message was moved here from #mathlib4 > lake exe cache get broken? by Jeremy Tan.

[Alex J. Best]

Sum V W is the type whose elements are either an element of V or an element of W (non-overlapping). A sigma type is a natural way to generalize this, given an indexed family of types V : ι → Type _ (one type for each element of iota) we can form the sigma type Σ i, V i, this is a type whose elements are the union of those in all the V is (non overlapping). So the sum type is like a sigma type indexed by Fin 2. You can think of elements of the sigma type as dependent pairs (i, v) where i : ι and v : V i.

[Kyle Miller]

Yeah, that's exactly what I had in mind when I wrote that TODO.

def completeMultipartiteGraph (V : ι → Type*) : SimpleGraph (Σ i, V i) where ...

[Kyle Miller]

The definition of Adj should be Adj v w := v.1 ≠ w.1 (compare this to completeBipartiteGraph, where it's just checking that the sides each vertex is from are not equal)

[Eric Wieser]

Can this be written as a preimage of Sigma.fst on the complete graph?

[Eric Wieser]

docs#SimpleGraph.comap ?

[Eric Wieser]

Yeah, that looks like it would work

[Eric Wieser]

I guess we could have defined the bipartite case as the pullback of Sum.map (fun _ => ()) (fun _ => ()) or similar

[Kyle Miller]

Eric Wieser said:

Can this be written as a preimage of Sigma.fst on the complete graph?

Yes. One reason is that graph colorings are the same thing as graph homomorphisms to a complete graph, and completeMultipartiteGraph is the maximal graph with the given vertex colors. Sigma.fst gets the vertex color so to speak.

I've been going back and forth on this. On one hand it's nice having concrete graphs to show how you can define a concrete SimpleGraph, but maybe

abbrev completeMultipartiteGraph (V : ι → Type*) : SimpleGraph (Σ i, V i) := comap Sigma.fst \top

really is a better definition (note: I haven't tested this in Lean). simp is probably able to see that (completeMultipartiteGraph V).Adj v w = v.1 ≠ w.1 without any help.

[Eric Wieser]

That should be trivially true by definition, so you could always add the lemma

[Eric Wieser]

I assume you're less keen on my suggested re-definition of bipartite?

[Kyle Miller]

Eric Wieser said:

I guess we could have defined the bipartite case as the pullback of Sum.map (fun _ => ()) (fun _ => ()) or similar

I'm not sure where you're going with that, but comap Sum.isLeft \top with \top : SimpleGraph Bool should work.

[Eric Wieser]

The idea was to use Sum Unit Unit in place of Bool because it avoids breaking symmetry

[Eric Wieser]

It wasn't a very serious idea though, unlike the multipartite suggestion which I genuinely believe is the right definition

[Jeremy Tan]

#6762

[Jeremy Tan]

How could we define complete bipartite graphs as a special case of complete multipartite graphs, using the comap definition above?

[Jeremy Tan]

I note that in the present complete bipartite graph definition the types of the two sides can reside in different universes, whereas the indexed family requires all vertex types to be in the same universe

[Damiano Testa]

There was a similar discussion in #6723. The conclusion there was it was probably not worth the effort.

This conclusion may be very case-dependent though.

[Damiano Testa]

[or maybe not: @Junyan Xu just posted something new!]

[Yaël Dillies]

Btw, there's a very cute definition of the Turan graph as a SimpleGraph (Fin n)

[Yaël Dillies]

And I believe it is superior to the description as a complete multipartite graph

[Mauricio Collares]

You mean connecting two elements of Fin n iff they have different remainders mod k?

[Jeremy Tan]

@Yaël Dillies OK, I want to state Turán's theorem, but the statement here doesn't typecheck because failed to synthesize instance Fintype ↑(edgeSet H)...

import Mathlib.Combinatorics.SimpleGraph.Clique
import Mathlib.Order.Filter.Extr

namespace SimpleGraph

open SimpleGraph

def turanGraph (n r : ℕ) : SimpleGraph (Fin n) where Adj v w := v % r ≠ w % r

variable {V : Type*} [Fintype V] [DecidableEq V]
variable (G : SimpleGraph V) [DecidableRel G.Adj]

theorem turan {n r : ℕ} {hr : 0 < r} (hn : Fintype.card V = n)
    (hs : IsMaxOn (fun H => H.edgeFinset.card) {H | H.CliqueFree (r + 1)} G) :
    G ≃g turanGraph n r := by
  sorry

end SimpleGraph

[Jeremy Tan]

Can Fintype ↑(edgeSet H) where H : SimpleGraph V actually be proven from Fintype V & DecidableEq V alone? I believe it is so but no idea how to proceed

[Jeremy Tan]

If I had [DecidableRel H.Adj] this would be easy but what if I don't have it?

[Eric Wieser]

You definitely need that assumption, just add it

[Eric Wieser]

If you don't have it then there's no way to ask "is there an edge between these vertices"

[Jeremy Tan]

@Eric Wieser Yes, but where do I put that assumption wrt (fun H => H.edgeFinset.card)?

[Jeremy Tan]

H in the inline fun is a totally local variable!

[Eric Wieser]

I guess you could use fun H : Σ H, DecidableRel H.Adj => letI := H.2; H.1.edgeFinset.card

[Eric Wieser]

I'm not familiar with docs#IsMaxOn, maybe there's a nicer way

[Eric Wieser]

This problem would go away if we had separate SimpleGraph and FiniteSimpleGraph types to mirror Set and Finset; but that obviously entails lots of duplication

[Jeremy Tan]

Eric Wieser said:

I guess you could use fun H : {H // DecidableRel H.Adj } => letI := H.2; H.1.edgeFinset.card

Doesn't work.

theorem turan (n r : ℕ) {hr : 0 < r} {G : SimpleGraph V} [DecidableRel G.Adj]
    {hn : Fintype.card V = n}
    (hs : IsMaxOn (fun H : {K : SimpleGraph V // DecidableRel K.Adj} =>
      letI := H.2
      H.1.edgeFinset.card) {H | H.CliqueFree (r + 1)} G) :
    G ≃g turanGraph n r := by
  sorry

DecidableRel K.Adj is a Type, not a Prop

[Jeremy Tan]

There's also no such thing as IsDecidable

[Eric Wieser]

Oh good point, then it should be a sigma type (edited above)

[Jeremy Tan]

Jeremy Tan said:

Can Fintype ↑(edgeSet H) where H : SimpleGraph V actually be proven from Fintype V & DecidableEq V alone? I believe it is so but no idea how to proceed

My reasoning is this: even if H.Adj is not decidable it is still a subgraph of ⊤ : SimpleGraph V. Since Fintype V, ⊤ : SimpleGraph V has finitely many edges, so H must also have finitely many edges

[Eric Wieser]

That's not enough, Fintype requires you to know precisely what's in Finset.univ

[Scott Morrison]

Isn't there a prop-valued version of finiteness by now??

[Eric Wieser]

Yes, but you need to replace Finset.card as well

[Jeremy Tan]

This works, but…

theorem turan (n r : ℕ) {hr : 0 < r} {G : SimpleGraph V} [DecidableRel G.Adj]
    {hn : Fintype.card V = n} (hs : IsMaxOn (fun H : (Σ H : SimpleGraph V, DecidableRel H.Adj) =>
      letI := H.2; H.1.edgeFinset.card) {H | H.1.CliqueFree (r + 1)} (Sigma.mk G ‹_›)) :
    G ≃g turanGraph n r := by
  sorry

[Eric Wieser]

Isn't ≃g data? So that should be a def.

[Eric Wieser]

#lint will tell you

[Eric Wieser]

As Scott alludes to, you might have a better time with docs#Set.ncard

[Eric Wieser]

.... Which has a very weird type in the docs

[Jeremy Tan]

Somewhat better

def isoTuranGraph (n r : ℕ) {hr : 0 < r} {G : SimpleGraph V} [DecidableRel G.Adj]
    {hn : Fintype.card V = n} {hs : IsMaxOn (Set.ncard ∘ edgeSet) {H | H.CliqueFree (r + 1)} G} :
    G ≃g turanGraph n r := by
  sorry

[Eric Wieser]

This has to be non-computable, right? If G has any symmetry (which it must since it's isomorphic to turans graph) then there's no way to pick the isomorphism

[Jeremy Tan]

It probably will be noncomputable – I haven't written out the proof yet

[Kyle Miller]

Jeremy Tan said:

How could we define complete bipartite graphs as a special case of complete multipartite graphs, using the comap definition above?

I wouldn't make them be a special case. If we wanted, we could redefine bipartite graph to be comap Sum.isLeft (\top : SimpleGraph Bool), or use Eric's comap (Sum.map (fun _ => ()) (fun _ => ()) (\top : SimpleGraph (Sum Unit Unit)) and bask in the symmetry.

[Yaël Dillies]

@Jeremy Tan, just so you know, I'm porting @John Talbot's proof of Turan's theorem over at https://github.com/YaelDillies/LeanTuran

[Mauricio Collares]

Füredi's proof, which is what Talbot formalized IIRC, is really nice to have because it gives stability (and even supersaturated stability) for free.

[Yaël Dillies]

That's my reasoning as well.