## Stream: graph theory

### Topic: k-factors

#### Yaël Dillies (Nov 02 2021 at 11:06):

@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 (Nov 02 2021 at 11:07):

And is there a higher generality I'm missing?

#### Yaël Dillies (Nov 02 2021 at 11:09):

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 (Nov 02 2021 at 23:38):

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 (Nov 02 2021 at 23:40):

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 (Nov 02 2021 at 23:42):

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 (Nov 02 2021 at 23:43):

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 (Nov 02 2021 at 23:43):

Do we have the sum of simple_graphs?

#### Kyle Miller (Nov 02 2021 at 23:47):

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 (Nov 02 2021 at 23:50):

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 (Nov 02 2021 at 23:51):

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 (Nov 02 2021 at 23:52):

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

#### Kyle Miller (Nov 02 2021 at 23:53):

We'll want that equivalence eventually anyway.

#### Kyle Miller (Nov 02 2021 at 23:54):

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 (Nov 02 2021 at 23:55):

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

#### Yaël Dillies (Nov 02 2021 at 23:57):

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

#### Kyle Miller (Nov 03 2021 at 00:10):

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 (Nov 03 2021 at 00:16):

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

#### Yaël Dillies (Nov 03 2021 at 00:16):

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

#### Kyle Miller (Nov 03 2021 at 00:30):

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 (Nov 03 2021 at 00:31):

Yeah that's what I was describing above.

Where?

#### Yaël Dillies (Nov 03 2021 at 00:32):

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 (Nov 03 2021 at 00:33):

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 (Nov 03 2021 at 00:34):

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 (Nov 03 2021 at 00:35):

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

#### Kyle Miller (Nov 03 2021 at 00:35):

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

#### Yaël Dillies (Nov 03 2021 at 00:37):

Oh yeah, I guess.

#### Yaël Dillies (Nov 03 2021 at 00:37):

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

#### Kyle Miller (Nov 03 2021 at 00:39):

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

#### Yaël Dillies (Nov 03 2021 at 00:40):

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 (Nov 03 2021 at 00:41):

Yes, what I'm asking for is overpowered.

Last updated: Dec 20 2023 at 11:08 UTC