IsBipartiteWith doesn't cover all vertices

Stream: graph theory

[Jakub Nowak]

I've just realized that given G : SimpleGraph V and G.IsBipartiteWith s t it is not true, that s ∪ t = @Set.univ V. We only have G.support ⊆ s ∪ t. Should we change the definition so it also requires s ∪ t = Set.univ, or are we okay with the fact that biparition doesn't partition isolated vertices?
One consequence of this is that we doesn't have equivalence between 2-colorings and IsBipartiteWith. Although it's not an important property, I think it might be nice to have it?

[Snir Broshi]

G.IsBipartiteWith' s := G.IsBipartiteWith s sᶜ perhaps?

[Eric Wieser]

As an aside I think s ∪ t = Set.univ is better spelt Codisjoint s t

[Aaron Liu]

it would be if there were any lemmas on @Codisjoint (Set _) _

[Aaron Liu]

@loogle @Codisjoint (Set _)

[loogle]

:search: Codisjoint.preimage, Finsupp.codisjoint_supported_supported, and 11 more

[Aaron Liu]

@loogle @Disjoint (Set _)

[loogle]

:search: Set.disjoint_empty, Set.empty_disjoint, and 869 more

[Snir Broshi]

I think for this def it's more of a Setoid.IsPartition {s, t}. The fact that the graph is loopless guarantees Disjoint s t but it's strange to rely on it and only specify the Codisjoint half

[Vlad Tsyrklevich]

Your proposed change doesn't give an equivalence with 2 colorings since there's nothing forcing there to be an edge (or a vertex for that matter.)

[Vlad Tsyrklevich]

Adding the union property is logically equivalent to the current definition since any graph that is currently IsBipartiteWith s t would simply be IsBipartiteWith s s^c under the definition with the union property.

[Aaron Liu]

Snir Broshi said:

I think for this def it's more of a Setoid.IsPartition {s, t}. The fact that the graph is loopless guarantees Disjoint s t but it's strange to rely on it and only specify the Codisjoint half

Is that the same as IsCompl s t

[Aaron Liu]

oh no it's not because docs#Setoid.IsPartition also requires all the parts to be nonempty

[Jakub Nowak]

@Mitchell Horner you're listed as an Author of Bipartite file, so you might be interested in this discussion.

[Snir Broshi]

Aaron Liu said:

oh no it's not because docs#Setoid.IsPartition also requires all the parts to be nonempty

Cool, so IsCompl sounds better. It uses Codisjoint but seems to have more API, weird

[Mitchell Horner]

The definition of IsBipartiteWith is intended to be the proof that "every edge connects vertices in these two distinct sets". I prefer that Codisjoint s t is not required, as it makes combinations of the following statements possible with little to no coercion.

theorem between_isBipartiteWith (h : Disjoint s t) : (G.between s t).IsBipartiteWith s t
theorem isBipartiteWith_sum_degrees_eq (h : G.IsBipartiteWith s t) : ∑ v ∈ s, G.degree v = ∑ w ∈ t, G.degree w

[Mitchell Horner]

If it is the name that bothers you, feel free to rename it to something else. Id prefer it to be renamed rather than redefined.

Jakub Nowak said:

are we okay with the fact that biparition doesn't partition isolated vertices?

As one can recover a bipartition of vertices from IsBipartiteWith easily (and I mention this little nuance in the module docstring) I am okay with this.

[Mitchell Horner]

Snir Broshi said:

G.IsBipartiteWith' s := G.IsBipartiteWith s sᶜ perhaps?

IsBipartiteWithCompl?

[Jakub Nowak]

I think that isBipartiteWith_sum_degrees_eq is still true even if we require Codisjoint s t?

As for between_isBipartiteWith, maybe SimpleGraph.between should return SimpleGraph ↑(s ∪ t) instead of SimpleGraph V? With this change between_isBipartiteWith will still be true even with Codisjoint s t.

[Jakub Nowak]

Ah, sorry, you concern about isBipartiteWith_sum_degrees_eq is that it requires s and t to be finsets?

[Jakub Nowak]

We could use docs#finsum instead of docs#Finset.sum to state that result even with infinite sets I think?

[Mitchell Horner]

Jakub Nowak said:

maybe SimpleGraph.between should return SimpleGraph ↑(s ∪ t) instead of SimpleGraph V

G.between s t is intended to have the same type as G as I found it is easier to interpret and use as a true subgraph of G without having to map its vertices. It is primarily used with s sᶜ anyway but is left generalized (like IsBipartiteWith) for edge cases.

[Jakub Nowak]

It could also return G.Subgraph. SimpleGraph.Subgraph has useful lemmas that make working with subgraphs easier.

[Jakub Nowak]

I'm aware that it can be painful to work with subgraphs. That's why I think at least some people would want to leave SimpleGraph behind and move to docs#Graph.

[Mitchell Horner]

Lots of the definitions in this file are a convenience wrapper around DoubleCounting.lean to help double-counting arguments that often come in the form of bipartite graphs.

I see G.between s t as a convenience for double-counting the edges between s and t, I don't think it needs to be G.Subgraph either :sweat_smile: - the fact that it is itself SimpleGraph V is just a further convenience when working with graph-related terms (degrees, etc.).

[Mitchell Horner]

I don't want to seem obstinate. :sweat_smile: I understand the philosophy behind the suggestions - to constrain the definitions to capture extra structure - but for what I need, I prefer that they are unconstrained and easy to reach for.

[Jakub Nowak]

Hm. I can understand your position. There are many use cases when isolated vertices don't matter. Especially if you're thinking about Graph as just relation. I feel like we have two potentially conflicting views on graphs.

Maybe we should really have two different graphs definitions? We could have SimpleGraph be this kinds of view on graphs, where you mainly care about relation and not much about vertex set. This would suggest changing the definition of SimpleGraph.Subgraph and removing verts and edge_vert from it.

And we can have docs#Graph be the kind of approach on graphs, where you think about graph as a structure of vertices and edges, and in which case you do care about distinguishing isolated vertices.

[Shreyas Srinivas]

Could we please not abandon simplegraphs to have no vertex set?

[Shreyas Srinivas]

There is a hideous amount of definitions that need to be duplicated across SimpleGraph and subgraph because of this

[Shreyas Srinivas]

And there is too much existing stuff in SimpleGraph to abandon it

[Jakub Nowak]

I'm not saying to abandon it entirely, but to move it to docs#Graph.

[Shreyas Srinivas]

Further in many cases Simplegraphs are all we need

[Shreyas Srinivas]

The current state is that Graph has basically too little API

[Shreyas Srinivas]

And it would take too long to reinvent it

[Shreyas Srinivas]

And in many cases even if we did, SimpleGraph is better

[Shreyas Srinivas]

If someone wants to work with Relations let them work with docs#Rel

[Jakub Nowak]

Shreyas Srinivas said:

If someone wants to work with Relations let them work with docs#Rel

That's a good point.

[Shreyas Srinivas]

I’d really really like SimpleGraph to actually represent simple graphs and that means giving them a vertex set and replacing Subgraph uses with IsSubgraph

[Shreyas Srinivas]

Because the other point is, Subgraphs are Simplegraphs too and it is tedious to repeat basi definitions for it

[Shreyas Srinivas]

If someone wishes to improve docs#Graph so that it can eventually subsume SimpleGraphs and make the change completely transparent to downstream users, that is great, but until then SimpleGraphs are the only meaningful API we have for downstream use and any improvement to make it more graph-like (in the set theoretic sense) is a good idea imho.

[Jakub Nowak]

So, I think we want SimpleGraph.between to return docs#SimpleGraph.Subgraph. And the version that doesn't restrict domain, as @Mitchell Horner wants it, should be defined on docs#Rel or docs#SetRel.