## Stream: graph theory

### Topic: Bipartite graphs

#### Yaël Dillies (Nov 18 2022 at 12:16):

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 (Nov 18 2022 at 12:20):

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

#### Yaël Dillies (Nov 18 2022 at 12:25):

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 (Nov 18 2022 at 12:25):

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

#### Kyle Miller (Nov 18 2022 at 14:01):

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

#### Kyle Miller (Nov 18 2022 at 14:02):

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

#### Kyle Miller (Nov 18 2022 at 14:04):

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?

Interesting...

#### Yaël Dillies (Nov 18 2022 at 14:08):

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 (Nov 18 2022 at 14:11):

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 (Nov 18 2022 at 14:13):

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

#### Mauricio Collares (Nov 18 2022 at 14:21):

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 (Nov 18 2022 at 14:33):

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

#### Yaël Dillies (Nov 18 2022 at 14:36):

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 (Nov 18 2022 at 14:40):

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 (Nov 18 2022 at 14:44):

What's "it" that might break?

#### Yaël Dillies (Nov 18 2022 at 14:51):

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

#### Mauricio Collares (Nov 18 2022 at 15:31):

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.

Last updated: Aug 03 2023 at 10:10 UTC