Bipartite graphs

Stream: graph theory

[Yaël Dillies]

I am about to prove Erdös-Stone from SRL and for this I need the Embedding lemma, hence some API for containment.

[Yaël Dillies]

Now, the Zarankiewicz problem is about maximizing the number of edges of a $K_{t,t}$-free bipartite graph.

[Yaël Dillies]

Hence I wonder whether I should write API for both containment of simple graphs and containment of bipartite graphs.
Those notions are genuinely different. There are less containments of bipartite graphs than of the corresponding simple graphs, because each of the two parts of the contained graph must be mapped in the corresponding part of the containing graph. The thing is that those notions agree when the graph is complete bipartite (and that covers Zarankiewicz for example), as this forbids edges within a given part.

[Yaël Dillies]

TLDR: Do we care about containing non-complete bipartite graphs?

[Kyle Miller]

I'm not really familiar with SRL and how containment is used. What sorts of notions do you need to support?

[Kyle Miller]

Is this the generalization of "triangle-free" for other patterns?

[Kyle Miller]

One version of a bipartite graph is a graph that has a graph homomorphism to $K_2$. If keeping track of the partition is what you need, perhaps you want to model this as injective graph homomorphisms $G$ to $H$ such that their maps to $K_2$ commute?

[Yaël Dillies]

Interesting...

[Yaël Dillies]

Not much about containment is needed, really. What we need is

• containment can be pulled back along injective homs (which is immediate if we define containment as the presence of an injective hom)
• we can ensure no containment of H by removing one edge from each potential copy of H
• the number of potential copies of H is (|G| choose |H|)

[Kyle Miller]

Graph colorings are already defined to be graph homomorphisms to $K_t$, so maybe what you're doing justifies developing coloring-preserving graph homomorphisms. This is a slice category of the category of simple graphs, if you want to think of it that way.

[Yaël Dillies]

I think for now I will stick to simple graphs, and revisit this design decision when doing Zarankiewicz.

[Mauricio Collares]

Yaël Dillies said:

TLDR: Do we care about containing non-complete bipartite graphs?

Even cycles are an interesting example. See, e.g., https://www.its.caltech.edu/~dconlon/EGT10.pdf

[Yaël Dillies]

Seeing a bipartite graph as a simple graph still works in this case, right?

[Yaël Dillies]

Actually, the only way it breaks would be if we tried to contain a disconnected graph, as a connected graph is either 2-colored (in which case containing it as a bipartite graph and as a simple graph are the same thing, up to picking a color), or it is not (in which case it can't be contained according to either)

[Yaël Dillies]

So a better question would be "Do we ever want $G_1 = (X_1 \cup Y_1, E_1)$ containing $G_2 = (X_2 \cup Y_2, E_2)$ to mean that we have injections $X_2 \rightarrow X_1$, $Y_2 \rightarrow Y_1$?"

[Kyle Miller]

What's "it" that might break?

[Yaël Dillies]

Seeing a bipartite graph on α and β as a simple graph on α ⊕ β.

[Mauricio Collares]

I don't know any interesting theorems that vare about disconnected bipartite graphs in the extremal setting. Counting embeddings respecting the bipartition appears in places such as the KŁR conjecture (see, e.g., https://arxiv.org/abs/1305.2516), where they're called "canonical copies", but I think it's too early to think about that in mathlib.

[Alena Gusakov]

I know this thread is from a while ago but I had some thoughts recently that I wanted to try to reason through with other people.

@Kyle Miller made a comment in some other thread about whether we want graphs to be defined on different vertex types, which got me thinking - there are often cases where we use graph theory to reason about sets with different types. I'm thinking it might be interesting to experiment with a sort of graph hierarchy (that doesn't have edges as first class objects, sorry @Peter Nelson) that looks something like the following:

structure WeirdDef (V₁ V₂ : Type u) where
  Adj : V₁ → V₂ → Prop
  Rev : V₂ → V₁ → Prop

structure SimpleGraph (V : Type u) extends WeirdDef V V where
  symm : ∀ (u v : V), Adj u v ↔ Rev v u  -- this part is a bit silly/awkward
  irrefl : ∀ (v : V), ¬ Adj v v

Some advantages that I can think of with this definition is we're "bundling" the opposite direction for edges, but a disadvantage is we'd have to consider two cases for every edge: Adj u v or Rev u v, which will lead to a ton of code duplication. Another option is to use an idea Peter mentioned a while back for defining undirected graphs as a quotient over the edge orientations in directed graphs. Zooming out to having distinct types, maybe we could develop something resembling sym2 that works for different types for this?

@Eric Wieser's graded rings paper also makes me wonder whether we should have graphs over more vertex types that are indexed, which would introduce some awkward dependent type theory, but allow for distinct adjacency definitions between different pairs of types where we don't have to use if then else that splits over different sets. One drawback I can see is it would introduce a lot of dependent type problems and/or code duplication in the case of e.g. objects that are defined in a single type where we do actually need to use if then else over sets.

Another huge drawback is code duplication and/or awkwardness between bipartite defined over types vs bipartite as a property of simple graphs.

Something else I keep wondering is whether the properties of adjacency relations should be unbundled/instances.

I don't know, does anyone have any thoughts on this? I feel like these might be some problematic definitions but I'm wondering if there's something there. I'm fairly convinced that we need to allow for different vertex types in a single graph. Allowing for distinct types is the sort of approach we had in one of the formulations of Hall's Marriage Theorem.

[Shreyas Srinivas]

Why not just use a disjoint sum of types when we need different types of vertices

[Shreyas Srinivas]

Or define a more complex network of relations and conversion functions to SimpleGraph or Digraph as needed

[Alena Gusakov]

Shreyas Srinivas said:

Why not just use a disjoint sum of types when we need different types of vertices

You'd still need to be able to define the adjacency relation as between the distinct types though, no? I guess you could coerce back and forth between the sum type and the individual types, but I think the type coercion will also get messy/awkward

[Shreyas Srinivas]

I am just a bit wary about types as a solution to anything because so far I have found that working with Sets and partitions is much simpler than type theoretic things

[Shreyas Srinivas]

Even the absence of vertex sets in the current SimpleGraph definitions leads to a lot of inconvenience

[Alena Gusakov]

Shreyas Srinivas said:

Even the absence of vertex sets in the current SimpleGraph definitions leads to a lot of inconvenience

I do agree with that

[Alena Gusakov]

I was thinking you could somehow use this same approach but combine it with the set requirement, i.e. everything related by adjacency has to belong to carrier sets

[Alena Gusakov]

I think you could write that requirement in an abstract way, like if the types are indexed and we had a sym sort of object defined on distinct types

[Kyle Miller]

Here's a way to avoid Rev:

structure WeirderDef {ι : Type u} (V : ι → Type v) where
  Adj {i j : ι} : V i → V j → Prop
  symm : ∀ (i j : ι) (v : V i) (w : V j), Adj v w → Adj w v
  partite : ∀ (i : ι) (v w : V i), ¬ Adj v w

[Alena Gusakov]

Kyle Miller said:

Here's a way to avoid Rev:

structure WeirderDef {ι : Type u} (V : ι → Type v) where
  Adj {i j : ι} : V i → V j → Prop
  symm : ∀ (i j : ι) (v : V i) (w : V j), Adj v w → Adj w v
  partite : ∀ (i : ι) (v w : V i), ¬ Adj v w

Oh yes, this is what I was thinking but I was having trouble figuring out how to express it - the indexed types allow for a good amount of generality

[Alena Gusakov]

We could have one definition that doesn't include symm or partite but that does have the carrier set requirement, so that it can be generalized to types that do overlap

[Alena Gusakov]

structure WeirderDef {ι : Type u} (V : ι → Type v) where
  Adj {i j : ι} : V i → V j → Prop
  Carrier (i : ι) : i → Set V i
  adjSet {i j : ι} : Adj (v : V i) (w : V j) → v \in V i → w \in V j -- or something

[Alena Gusakov]

and then that could be generalized to the undirected or partite requirements, etc

[Alena Gusakov]

and for a single vertex type we just specify a singleton index set and make an alias for it, or for a graph that we want to be bipartite in the same vertex type we'd have the partite requirement be on the carrier sets (belonging to the same type) instead of the types (code duplication for sets vs types - problem?). Would we want the partite condition to be a typeclass? I guess edge contractions would become really really messy then, but I don't think they're too nice in the single vertex type case either because you still have to quotient over two vertices and get a new type

[Alena Gusakov]

This might be too expressive though, what if the vertex types are all singletons

[Shreyas Srinivas]

Kyle Miller said:

Here's a way to avoid Rev:

structure WeirderDef {ι : Type u} (V : ι → Type v) where
  Adj {i j : ι} : V i → V j → Prop
  symm : ∀ (i j : ι) (v : V i) (w : V j), Adj v w → Adj w v
  partite : ∀ (i : ι) (v w : V i), ¬ Adj v w

Interesting. I did something similar in my definition of the port numbering model of distributed graph algorithms.

[Shreyas Srinivas]

There each vertex labels its adjacent edges differently and the type of the labelling depends on the degree of the vertex.

[Shreyas Srinivas]

I also use an indexing notation to construct a uniform type of vertex and edge labellings which describe inputs and outputs to algorithms.

[Shreyas Srinivas]

@Alena : perhaps we could use labels to classify vertices into different “types”?

[Shreyas Srinivas]

Here: https://github.com/Shreyas4991/DGAlgorithms/blob/main/DGAlgorithms/Models/PortNumbering.lean#L11

[Shreyas Srinivas]

The good thing with labellings is that one can simply extend SimpleGraph with a structure that adds labels. Additionally one can continue working on the underlying SimpleGraph when convenient.

[Kyle Miller]

Shreyas Srinivas said:

@Alena : perhaps we could use labels to classify vertices into different “types”?

The vertex labeling version of n-partite is already done using docs#SimpleGraph.Coloring

The IsBipartite predicate is defined using it: https://github.com/leanprover-community/mathlib4/blob/1a83ec9d7a74f9063014411a530bdbdbb3b86a38/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean#L252

There's always going to be a tension between using indexed families of types and a projection function from a "total type". They're dual to each other.

[Alena Gusakov]

Kyle Miller said:

Shreyas Srinivas said:

@Alena : perhaps we could use labels to classify vertices into different “types”?

The vertex labeling version of n-partite is already done using docs#SimpleGraph.Coloring

The IsBipartite predicate is defined using it: https://github.com/leanprover-community/mathlib4/blob/1a83ec9d7a74f9063014411a530bdbdbb3b86a38/Mathlib/Combinatorics/SimpleGraph/Bipartite.lean#L252

There's always going to be a tension between using indexed families of types and a projection function from a "total type". They're dual to each other.

Yeah that's kind of why I was wondering whether indexed families of types is something we want for our graphs. I'm still inclined to think we might want it, @Bhavik Mehta pointed out to me that it could be useful for cographs or if we ever want to work with graded graphs (which I didn't know was a thing, whoops) but one big issue is having graphs with singleton vertex types, or graphs with empty types floating around, etc and the awkward lack of defeqs between them graphs that should be the same

[Alena Gusakov]

You could maybe impose a nontrivial instance on the types but another problem is the indexing function imposes an ordering on the types, and otherwise identical graphs with different indexing will not be defeq

[Alena Gusakov]

Which brings me back to the weird sym2 idea, if we have something like that where order doesn't matter we could sort of avoid that problem, if it's built into the definition somehow. But then that might be awkward to work with, and you probably still want an indexing function to be able to put arbitrarily many types

[Alena Gusakov]

I'll look at the category theory library later today to see what I can learn from it for this stuff, I'm sure someone's already done that before/done work inspired by it but it'll be more for my own understanding of what we can do. Thanks for indulging my train of thought lol