k-factors

Stream: graph theory

[Yaël Dillies]

@Kyle Miller, how hard do you think it is to prove that the number of k-factors of a graph is the product over its connected components of their number of k-factors?

[Yaël Dillies]

And is there a higher generality I'm missing?

[Yaël Dillies]

In particular, should we define k-factors of a graph or of a subgraph? And how do you plan on modelling connected components? For this latter question, I think defining them as a set of subgraphs is the way to go.

[Kyle Miller]

Connected components are not very developed in the walks_and_trees branch yet. So far it's just the quotient of V by G.reachable, so it's more like $\pi_0(G)$.

The set of connected components as subgraphs I think is

def connected_components : set (subgraph G) :=
{G' | G'.coe.connected ∧ ∀ G'', G' ≤ G'' → ¬ G'.coe.connected}

and it would be good having a theorem that says these correspond to quot G.reachable, with each connected component being the induced subgraph from an equivalence class of vertices. (And that the union of these graphs is G and that they're disjoint.)

There also ought to be facts like every G.walk u v can be written as a walk in an element of connected_components. The code for reinterpreting walks as walks in subgraphs is very underdeveloped at the moment, though there's not nothing.

[Kyle Miller]

Another aspect of formalization is writing G specifically as a disjoint union of connected subgraphs. In a way, the stuff about quot G.reachable and induced subgraphs is just a way to show it's possible.

[Kyle Miller]

I don't know very much about k-factors. My ignorant answer is that it seems ok defining them for graphs, then for subgraphs you have k-factors of G'.coe.

[Yaël Dillies]

So you mean I should rather prove that the number of k-factors of a sum of graphs is their product? Then the connected component version will be a special case.

[Yaël Dillies]

Do we have the sum of simple_graphs?

[Kyle Miller]

I mean write a graph as a disjoint union of connected subgraphs, then relate k-factors of subgraphs (as k-factors of subgraphs coerced to simple graphs) to the original graph.

[Kyle Miller]

Then again, it's probably fine defining k-factors with respect to a subgraph, since k-factors of the top subgraph is a special case.

[Yaël Dillies]

Ah okay, so what about (warning, doesn't compile as is) simple_graph.pi (s : set ι) (G : Π i, simple_graph (α i)) : simple_graph (Π i, α i) := s.pi G? And then you can show number_k_factors (imple_graph.pi s G) = ∏ i, number_k_factors (G i)?

[Yaël Dillies]

Then you can transfer this result to connected components using the equivalence between a graph and the sum of its connected compoents.

[Kyle Miller]

We'll want that equivalence eventually anyway.

[Kyle Miller]

I'm not sure it'll make the proof easier though. I think it might be less awkward staying in the realm of subgraphs of a given graph, though it'd take setting things up right.

[Kyle Miller]

(I'm imagining wrangling all the vertex types, versus having just one vertex type.)

[Yaël Dillies]

Yeah, I totally get that. Which way sounds the more mathlib-like to you?

[Kyle Miller]

I think the statements in the end will be the same (and will involve creating similar theory), so whichever way to get there that's simpler :smile:

Here's some start for some pseudocode. The idea is that mk_k_factor is actually defining an equivalence between the product of the sets of k-factors of the connected components and the k-factors of G, which would be explicitly constructed next from it, and then you apply the lemmas for fintype.card of an equivalence and extract the result you want.

def connected_components : set (subgraph G) :=
{G' | G'.coe.connected ∧ ∀ G'', G' ≤ G'' → ¬ G'.coe.connected}

def subgraph.k_factors [locally_finite G] (G' : subgraph G) (k : ℕ) : set (subgraph G) :=
{G'' | G'.verts = G''.verts ∧ G''.coe.is_regular_of_degree k}

def mk_k_factor [locally_finite G] (k : ℕ)
  (f : Π G' (hG' : G' ∈ G.connected_components), subgraph G)
  (hf : ∀ G' hG', f G' hG' ∈ G'.k_factors k) :
  {G' : subgraph G | G' ∈ (⊤ : simple_graph V).k_factors k} := sorry

[Kyle Miller]

(The inverse of mk_k_factor would be from intersecting the k-factor G' with each connected component.)

[Yaël Dillies]

I like the idea! But I'm not convinced we should rely on connected_components to even define mk_k_factor

[Kyle Miller]

You could develop a theory of disjoint unions of "locally complete" subgraphs (maybe subgraphs that contain their incidence sets) and define mk_k_factor in terms of choosing a k-factor for each subgraph in the disjoint union.

Then as a special case, the connected components (as defined above) form such a system.

[Yaël Dillies]

Yeah that's what I was describing above.

[Kyle Miller]

Where?

[Yaël Dillies]

Here
Yaël Dillies said:

So you mean I should rather prove that the number of k-factors of a sum of graphs is their product? Then the connected component version will be a special case.

and there
Yaël Dillies said:

Ah okay, so what about (warning, doesn't compile as is) simple_graph.pi (s : set ι) (G : Π i, simple_graph (α i)) : simple_graph (Π i, α i) := s.pi G? And then you can show number_k_factors (imple_graph.pi s G) = ∏ i, number_k_factors (G i)?

[Yaël Dillies]

Well, I wasn't talking about the ismorphism, but counting kind of implies having the isomorphism under the rug. Sorry if that was unclear.

[Kyle Miller]

I for some reason thought you meant for the components of the sum to be connected, so I missed that.

I guess it's the difference between doing in synthetically (like yours) or analytically (like mine). The only way to know which is "better" is to implement it both ways.

[Kyle Miller]

But we still would want both points of view in the end.

[Kyle Miller]

It's like the whole thing about direct sums of vector spaces vs internal direct sums of subspaces.

[Yaël Dillies]

Oh yeah, I guess.

[Yaël Dillies]

So k-factors over subgraphs but isomorphism over disjoint graphs sounds like the most general setting?

[Kyle Miller]

What's the application? (Also, I'm having trouble parsing your suggestion.)

[Yaël Dillies]

Mario's formalization project. In particular, the bit that asks that the graph is connected if there are at least two perfect matchings and each edge is forced.

[Yaël Dillies]

Yes, what I'm asking for is overpowered.