## Stream: graph theory

### Topic: simple_graphs2

#### Alena Gusakov (Aug 24 2020 at 22:24):

I pushed an error fix that Kevin helped me out with

#### Alena Gusakov (Aug 24 2020 at 22:24):

Basically just got rid of the problem in degree_le where Lean didn't know why we were allowed to compare the degrees because it didn't know degree (G'.in_subgraph hv) is a fintype

#### Alena Gusakov (Aug 24 2020 at 22:58):

just kidding, somehow there's still an error somewhere

#### Kyle Miller (Aug 24 2020 at 23:01):

I'm going to take a look -- I had some troubles with these instances because they caused class resolution to not terminate. (I'm trying to get my own changes to the branch in order so I can merge yours.)

#### Kyle Miller (Aug 25 2020 at 08:16):

Alena Gusakov said:

just kidding, somehow there's still an error somewhere

These instances are tricky, and I've been struggling with how to define these off and on for a while, but they might finally now be OK. It turns out you can't actually have them as instances because they "introduce metavariables", which are caused by variables on the LHS of the colon that cannot be totally inferred by either class resolution or the usual implicit argument elaboration.

Anyway, degree_le is now a lemma (with proof!), and it makes use of some new lemmas involving graph embeddings. The idea is that it's not hard to prove that the neighbor set of a vertex in a subgraph embeds in the neighbor set of that vertex in a supergraph, and then fintype.card_le_of_injective does the rest.

If you wanted, you could follow the same strategy with embedding.map_edge_set to show that the cardinality of an edge set of a subgraph is less than or equal to the cardinality of the supergraph's edge set.

#### Kyle Miller (Aug 25 2020 at 08:18):

A couple of other sorry's:

• complete_graph_min_colors is that a complete graph on n vertices needs at least n colors in a proper coloring.
• exists_path_eq_eqv_gen should follow from a lemma that if there is a walk between two vertices then there is a path between them.

#### Alena Gusakov (Aug 25 2020 at 13:16):

it seems like there are other errors now though - namely in the proofs of all of the map_edge_set definitions oops, restarted lean and the errors went away

#### Kyle Miller (Aug 26 2020 at 05:13):

After some discussion with @Alena Gusakov, the branch now has what seems to be an easier-to-work-with definition of subgraphs:

structure subgraph :=
(V' : set (V G))
(adj' : V G → V G → Prop)
(adj_sub : ∀ ⦃v w : V G⦄, adj' v w → v ~g w)
(edge_vert : ∀ ⦃v w : V G⦄, adj' v w → v ∈ V')
(symm' : symmetric adj')


(It has the correct extensionality property, which I had trouble getting right with this sort of formulation, that there is exactly one term per subgraph. That's why the earlier definition used a subset of edges.)

As an experiment in a technique to show two definitions are equivalent, I kept the old definition as a protected definition in the simple_graph.subgraph namespace:

protected structure of_edge_set' (G : α) :=
(V' : set (V G))
(edge_set' : set (sym2 (V G)))
(edge_sub : edge_set' ⊆ edge_set G)
(has_verts : ∀ ⦃e : sym2 (V G)⦄ ⦃v : V G⦄, e ∈ edge_set' → v ∈ e → v ∈ V')


Then I gave it a simple_graphs instance and proved two statements:

protected def equiv_of_edge_set' : subgraph G ≃ of_edge_set' G

def iso_of_edge_set' (G' : subgraph G) : G' ≃g subgraph.equiv_of_edge_set' G'


That is to say, the types are equivalent, and that equivalence carries graphs to isomorphic graphs. (This is what I meant in the matroids topic -- matroids have multiple definitions, and this seems to be a structured way to formalize that the definitions are equivalent.)

#### Kyle Miller (Aug 26 2020 at 20:19):

I've added formalizations of the first two theorems in Bollobas's book in this branch.

-- The type of all embedded cycles in a given graph
def cycles (G : α) := Σ (n : {n : ℕ // 3 ≤ n}), cycle_graph n.1 n.2 ↪g G

/--
Veblen 1912 (theorem 1 in book).  Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
(∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (cycles G),
∀ (e : edge_set G), !∃ (c : cycles G), c ∈ partition ∧
e ∈ set.image (embedding.map_edge_set c.2) set.univ) :=
sorry

/--
Mantel 1907 (theorem 2 in book). If a graph with n vertices and m edges satisfies
floor(n^2 /4) < m, then it contains a triangle.
-/
theorem has_triangle (G : α) [fintype (V G)] (h : (fintype.card (V G))^2 / 4 < (edge_finset G).card) :
nonempty (cycle_graph 3 (by linarith) ↪g G) :=
sorry


(Proving these will take a good amount of theory building still.)

For the first theorem, it's probably better to formalize cycles as being subgraphs that are isomorphic to a cycle graph, since with the current formulation every cyclic shift of a cycle is considered to be a different cycle. It's probably also good to formalize the idea of edge-disjoint partitions by subgraphs.

#### Kyle Miller (Aug 26 2020 at 20:32):

Changed it to be in terms of subgraphs that are cycles:

/--
Veblen 1912 (theorem 1 in book). Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
(∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (subgraph G), (∀ G' ∈ partition, subgraph.is_cycle G') ∧
∀ (e ∈ edge_set G), !∃ (c : subgraph G), c ∈ partition ∧
e ∈ c.edge_set') :=
sorry


#### Alena Gusakov (Aug 30 2020 at 17:12):

so for the second implication here

lemma exists_path_eq_exists_walk : exists_path G = exists_walk G :=
begin
ext v w,
split,
intro h,
rcases h with ⟨n, ⟨f, hf⟩⟩,
split,
use n,
rw walk,
use f.to_homomorphism,
exact hf,

intro h,
rcases h with ⟨n, ⟨f, hf⟩⟩,
sorry,
end


would having open_locale classical and then contracting edges between repeated vertices be a good strategy? i'm kind of stumped with this one

#### Alena Gusakov (Aug 30 2020 at 17:24):

also, i wonder if it might be useful to define some notion of the image of a graph homomorphism (unless i'm missing something that's already defined)

#### Kyle Miller (Aug 30 2020 at 17:26):

Feel free to make the lemma noncomputable and use the classical tactic for now. (I think classical does the equivalent of open_locale classical inside a proof, but I'll have to check)

#### Kyle Miller (Aug 30 2020 at 17:27):

I was imagining doing strong induction on the length of a walk. If a walk isn't a path, then there must be a repeated vertex, and then if you cut out the portion of the walk that occurred between the two vertices, the walk length gets shorter, hence it has a corresponding path by induction

#### Aaron Anderson (Aug 30 2020 at 17:28):

Do you even need noncomputable if you're just using classical inside a proof of a Prop?

Probably not

#### Alena Gusakov (Aug 30 2020 at 17:31):

also, is it possible to like, "concatenate" functions? like make a new function out of two that you already have

#### Kyle Miller (Aug 30 2020 at 17:32):

The easiest-to-remember way is using lambda expressions

#### Kyle Miller (Aug 30 2020 at 17:32):

There's a whole bunch of function combinators in the function namespace, too, but they don't seem to be used much

#### Kyle Miller (Aug 30 2020 at 17:35):

I tried using combine in the definition of graph homomorphisms, but there were some type errors (I think because it involved Prop?) and I reconsidered. It even has fancy notation: (f -[h]- g) x y = h (f x y) (g x y)

#### Alena Gusakov (Aug 30 2020 at 17:52):

I don't know if combine is what I'm looking for - it looks like it takes functions with two arguments

#### Alena Gusakov (Aug 30 2020 at 17:57):

I'm currently working on the concatenation of walks definition

#### Kyle Miller (Aug 30 2020 at 18:03):

combine was just one of the many examples of combinators. i don't think it's useful for what you're doing.

for walks, this is gluing walks together, right? I'm not sure how gluing functions together works elsewhere in mathlib (how do the sheaf axioms glue functions? maybe that's to general to be useful here)

(When you said "contract" earlier, this might be where it'd be nice to actually have a quotient construction, using the expanded notion of graph homomorphism that was in the ncatlab article)

#### Alena Gusakov (Aug 30 2020 at 18:09):

I think I might've found a way to do it, does this look legit?
to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,

#### Alena Gusakov (Aug 30 2020 at 18:09):

context:

def walk.concat {n : ℕ} {m : ℕ} {v w u : V G} (p : walk G n u v) (q : walk G m v w) :
walk G (n + m) u w :=
{ val :=
{ to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,
property := sorry, }


#### Alena Gusakov (Aug 30 2020 at 18:10):

wait no it's not cause x is a vertex. I'll smooth that out I guess

#### Alena Gusakov (Aug 30 2020 at 18:12):

It seems like it would just be to_fun := λ x, if x.1 ≤ n then p.1.to_fun x else q.1.to_fun x,

#### Kyle Miller (Aug 30 2020 at 18:24):

I just realized that I have this partially defined in that file already, it's just too big and disorganized, sorry. Take a look at walk_join

#### Kyle Miller (Aug 30 2020 at 18:25):

It still lacks the proof that the result is a walk

#### Kyle Miller (Aug 30 2020 at 18:26):

(I'm assuming you're using simple_graphs2 based on the exists_path_eq_exists_walk lemma)

ohhh okay, ty

#### Alena Gusakov (Aug 30 2020 at 21:19):

we can't have paths on a single vertex right? that contradicts the definition of path

#### Alena Gusakov (Aug 30 2020 at 21:19):

should we have a lemma that explicitly states that?

#### Kyle Miller (Aug 30 2020 at 21:21):

Are zero-length paths not ok?

#### Kyle Miller (Aug 30 2020 at 21:21):

for compositions of walks, I thought those would be identity elements

#### Kyle Miller (Aug 30 2020 at 21:25):

walks themselves should form a category (I forget the exact terminology, maybe a dagger category? some kind of category where objects are self-dual and morphisms have duals). objects of the category are vertices of the graph, morphisms are walks from a vertex to another vertex, composition of walks is the concatenation of the walks, identities are the zero-length walks, and duals are parameterization reversal

#### Kyle Miller (Aug 30 2020 at 21:26):

once you have all this set up, then "there exists a morphism from x to y" is an equivalence relation on objects of the category

#### Kyle Miller (Aug 30 2020 at 21:27):

i.e., "there exists a walk of any length from x to y" is an equivalence relation.

#### Jalex Stark (Aug 30 2020 at 23:47):

I remember writing path code that used path.empty v to be the empty path rooted at vertex v

#### Alena Gusakov (Sep 01 2020 at 15:04):

I'm having trouble working with simple_graph_from_rel - specifically, I can't seem to figure out how to treat the vertices in the graph as the original objects they were defined as

#### Kyle Miller (Sep 01 2020 at 17:14):

One trick is you can use the change tactic to change the type to whatever it's actually equal to.

Another is to add this missing lemma and use it to rewrite V G:

lemma simple_graph_on.verts_eq (α : Type u) (G : simple_graph_on α) : V G = α := rfl


Yet another thing you could do, I think, is to use erw rather than rw.

#### Alena Gusakov (Sep 01 2020 at 18:43):

now i'm getting hung up on trying to coerce the numbers from fin to nat

#### Alena Gusakov (Sep 01 2020 at 19:07):

should we add nontrivial to the definition of connected?

#### Alena Gusakov (Sep 01 2020 at 19:08):

actually wait no, i guess it's trivially true for...the trivial case

#### Alena Gusakov (Sep 01 2020 at 19:10):

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

#### Alena Gusakov (Sep 01 2020 at 19:10):

but it's an absolute nightmare

#### Aaron Anderson (Sep 01 2020 at 19:15):

I'm maybe behind the times on what definition of connected you're using, but perhaps it'd actually be easier to prove something more general: if you have a set of vertices, and no vertex in the set is adjacent to any vertex outside the set, then no vertex in the set is path-connected to any vertex outside the set

#### Alena Gusakov (Sep 01 2020 at 19:27):

My definition of connected is there exists a path between every vertex, but what I want to prove is that this means every vertex has at least one edge to it

#### Alena Gusakov (Sep 01 2020 at 19:29):

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

#### Aaron Anderson (Sep 01 2020 at 19:30):

Alena Gusakov said:

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

This should be at least pretty easy if we're using an embedding or subgraph definition of acyclic

#### Aaron Anderson (Sep 01 2020 at 19:31):

I'm going over to simple_graphs2 to check out what I've missed

#### Alena Gusakov (Sep 01 2020 at 19:31):

My current problem is when I say is_acyclic (subgraph G) it doesn't recognize the subgraph as a simple graph

#### Alena Gusakov (Sep 01 2020 at 19:32):

sorry, I should've said I'm having trouble stating it

#### Aaron Anderson (Sep 01 2020 at 19:39):

One note: @Kyle Miller, I know that we have good reasons to doubt whether graph homomorphisms should be modeled with rel_homs, but I'm confused why simple_graphs2 uses rel_iso to define isomorphisms, but doesn't use rel_embedding to define embeddings, when I'm pretty sure the custom structure for embeddings has the exact same information as rel_embedding

#### Kyle Miller (Sep 01 2020 at 19:40):

I was going to change it back eventually. Your new PR wasn't there yet

#### Kyle Miller (Sep 01 2020 at 19:40):

though my embedding was a mono, vs regular mono

#### Aaron Anderson (Sep 01 2020 at 19:42):

Kyle Miller said:

though my embedding was a mono, vs regular mono

Ah right, sorry

#### Aaron Anderson (Sep 01 2020 at 19:49):

Anyway, the main advantage of a non-regular mono is that an arbitrary subgraph has an inclusion embedding

#### Aaron Anderson (Sep 01 2020 at 19:50):

Have we put that in lean yet?

#### Aaron Anderson (Sep 01 2020 at 19:50):

Because I'd imagine that's how you'd prove that a subgraph of an acyclic graph is acyclic

#### Aaron Anderson (Sep 01 2020 at 19:50):

or I guess you redefine/show that it's equivalent to nonexistent of a subgraph which is a cycle

#### Aaron Anderson (Sep 01 2020 at 19:51):

in which case you want to use transitivity of subgraph

#### Aaron Anderson (Sep 01 2020 at 20:02):

Alena Gusakov said:

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

I think I have a sketch if you're willing to use the eqv_gen version, which is defined on simple_graphs2, but the equivalence is currently sorry

#### Aaron Anderson (Sep 01 2020 at 20:03):

Say you have a set S of vertices. Then you define an equivalence relation (actually a setoid) where two vertices are equivalent iff they're both in S or both not in S.

#### Aaron Anderson (Sep 01 2020 at 20:06):

What this tells you is that if (for all x y : V, x ~g y implies s.rel x y), where s.rel is our new equivalence relation

#### Aaron Anderson (Sep 01 2020 at 20:07):

then (eqv_gen G.adj) x y implies s.rel x y

#### Aaron Anderson (Sep 01 2020 at 20:07):

In other words, x being connected to y implies x and y are both in S or both not in S

#### Kyle Miller (Sep 01 2020 at 20:08):

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y


#### Aaron Anderson (Sep 01 2020 at 20:08):

This basically proves the lemma that if a set S is closed under adjacency, that its vertices are not connected to outside vertices

#### Aaron Anderson (Sep 01 2020 at 20:09):

and to prove the exact theorem you wanted, @Alena Gusakov , the only remaining step is to let S be a singleton. Then you find that if your singleton has degree 0, then it's closed under adjacency, so its one element is not connected to anything else, the contrapositive of what you wanted.

#### Aaron Anderson (Sep 01 2020 at 20:09):

Does that make sense?

#### Aaron Anderson (Sep 01 2020 at 20:14):

Kyle Miller said:

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y


Ok, so then it should be relatively easy to prove at least that if a subgraph S is NOT acyclic, then there is an embedding from a cycle graph into S, which you can then compose with subgraph.map to get an embedding from the cycle graph into the subgraph top

#### Aaron Anderson (Sep 01 2020 at 20:15):

Then it's a matter of showing that a graph isomorphic to an acyclic graph is acyclic, which can also work by composing embeddings

#### Kyle Miller (Sep 01 2020 at 21:14):

(Speaking of eqv_gen G.adj, one thing @Alena Gusakov is helping with is showing that three different definitions of connectivity are equal: there exists a path between vertices, there exists a walk between vertices, and eqv_gen G.adj.)

#### Alena Gusakov (Sep 01 2020 at 21:15):

yeah i've been poking around those lemmas, they're also a nightmare

#### Kyle Miller (Sep 01 2020 at 21:16):

I'm sure we'll figure out how to make it nice eventually :smile:

#### Kyle Miller (Sep 01 2020 at 21:35):

@Aaron Anderson I was considering replacing f : G ↪g G' with f : G →g G' having some kind of mono instance, not sure the right name. It's can't be the category theory one, unfortunately, for some of the usual reasons. It would be nice if injective were a typeclass here, because injective f ends up being the correct notation, given the has_coe_to_fun instance for graph homomorphisms.

#### Kyle Miller (Sep 01 2020 at 21:39):

I hesitate to do this, though, because ↪g seems to have been convenient so far to mean monomorphism since it extends function.embedding so can find some immediate use in some cardinality arguments. However, it seems possible to define a cast of a function with a mono-like instance to get a function.embedding as needed.

#### Kyle Miller (Sep 21 2020 at 01:14):

I've reorganized the simple_graphs2 repository in a number of ways:

• Now a simple graph is merely a term of simple_graph. This is a bundled simple_graph_on α term, for simple graphs with vertex type α.
• To give the terms of a type the structure of a simple graph, one implements has_coe_to_simple_graph. This gives you access to a new coercion arrow, ↟, which coerces graph-like things to simple graphs. This circumvents an issue where typeclass resolution won't assert two universe metavariables are equal, so has_coe cannot work, but perhaps in a future version of Lean this will be resolved. Until then, ↟ works well enough.
• The code has been broken up into multiple files in https://github.com/leanprover-community/mathlib/tree/simple_graphs2/src/combinatorics/simple_graph so hopefully it's easier to follow now!
• Graph homomorphisms have been changed to use order.rel_iso exclusively. Monomorphisms are graph homomorphisms that implement thesimple_graph.hom.mono typeclass.

More about ↟: Of the many ways of organizing the simple graph library so that derived objects like subgraphs can be graphs, too, this seems to be the least-bad of all of them, and it has the benefit that, in the future, these arrows might disappear entirely. While you might need to specify universe variables, like (G : simple_graph.{u}), so far I don't think I've been required to do this and have only done so for clarity in definitions.

When writing theorems about graphs in general, make sure to do it for terms of type simple_graph. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I've also added walks to the library. There are two ways they are represented, either as an inductive type that's essentially a list of adjacent vertices or as graph homomorphisms from path graphs into the graph. There is a proof that these are structurally equivalent (I visited heq on the way, one of the circles of dependent typed hell, but that's all gone now, thankfully -- I have a special version of heterogeneous equality in the library still, which seems like it could be useful, but if it finds no use it'll be removed). The walk type is essentially defining a category of walks, and it might be nice to actually give it a category structure, too.

Warning: not every definition makes sense and not every lemma with a sorry is provable -- I also, unfortunately, haven't necessarily fixed all errors. The documentation is probably not up to date either!

#### Kyle Miller (Sep 21 2020 at 01:34):

(The coercion arrow, by the way, didn't change the code much. The previous version still was about coercions, and it was just a matter of changing who is responsible for inserting them, so to speak.)

#### Jalex Stark (Sep 22 2020 at 01:47):

Wow! I guess there's a lot of shovel-ready work for filling in sorries and carving off PRs to mathlib.

#### Jalex Stark (Sep 22 2020 at 01:48):

Do you think that the current definition of simple graphs in mathlib should be replaced or just given an instance of the new coercion arrow?

#### Jalex Stark (Sep 22 2020 at 01:51):

Kyle Miller said:

When writing theorems about graphs in general, make sure to do it for terms of type simple_graph. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I guess this implies that you think the current theorem statements should be rejiggered to be about terms of type simple_graph. But if we give the old simple graph type an instance of the new coercion arrow, then e.g. the proof of freek 83 in the mathlib archive won't need changes, except maybe to add some arrows?

#### Jalex Stark (Sep 22 2020 at 01:54):

I am like 8000 messages in the hole in terms of staying up to date on the server... have you advertised this stuff on #maths or are you waiting until more of the sorries and errors are fixed?

#### Jalex Stark (Sep 22 2020 at 01:55):

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

#### Kyle Miller (Sep 22 2020 at 02:23):

Jalex Stark said:

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

Like this? (Good point :smile:)

#### Jalex Stark (Sep 22 2020 at 02:26):

Kyle Miller said:

Graph homomorphisms have been changed to use order.rel_iso exclusively. Monomorphisms are graph homomorphisms that implement thesimple_graph.hom.mono typeclass.

I guess @Aaron Anderson will be happy to hear this

#### Kyle Miller (Sep 22 2020 at 02:26):

The conversion to using simple_graph is almost entirely just removing vertex type arguments and then doing v : V G. It's pretty much painless.

#### Jalex Stark (Sep 22 2020 at 02:27):

What do you think the next PR from this branch should be?

#### Kyle Miller (Sep 22 2020 at 02:29):

It would be nice to sort out the coercion. There's a little discussion in #Is there code for X? (the auto-coercions thread) about how has_coe is almost but not quite sufficient, but it seems fixing this involves modifying Lean itself.

#### Kyle Miller (Sep 22 2020 at 02:29):

But maybe making the arrow a local notation is good enough for now.

#### Kyle Miller (Sep 22 2020 at 04:00):

Jalex Stark said:

What do you think the next PR from this branch should be?

Most of simple_graph/basic.lean seems good, except for the incomplete stuff about graph operations. Some simp lemmas relating simple_graph_on to simple_graph might not make sense. Also simple_graph_from_rel_adj can probably wait.

The definitions in simple_graph/hom.lean seem fine, but the lemmas should be reviewed since the api is underutilized and seems somewhat incomplete.

simple_graph/subgraph.lean seems good, except for things about cycles and maybe induced graphs. Cardinality results should be reviewed -- there's no application of them yet so the design might not be good.

simple_graph/simple_graph_on.lean is fine enough. It could certainly be expanded, but it at least has a bounded_lattice instance.

simple_graph/degree_sum.lean is close, but I think it can still be simplified a lot given a person sufficiently competent with big_operators. It also would be nice to have an explicit handshake lemma.

#### Kyle Miller (Sep 22 2020 at 04:01):

simple_graph/adj_matrix.lean is just the current adj_matrix.lean but modified to use this new simple_graph type.

#### Alena Gusakov (Oct 11 2020 at 22:17):

I think I completed the edge contraction definition

#### Alena Gusakov (Oct 11 2020 at 22:17):

I also created an edge deletion definition

#### Alena Gusakov (Oct 11 2020 at 22:17):

I tried messing around with paths and walks after that, as well as trees, but really didn't get anywhere

#### Alena Gusakov (Oct 11 2020 at 22:18):

I managed to prove the first direction of the statement map_rel_iff' in fin.flip.invol

#### Alena Gusakov (Oct 11 2020 at 22:19):

but the other direction has me stumped

#### Bhavik Mehta (Oct 11 2020 at 22:33):

Since it's an involution can't you just use the first direction and some equivalence properties?

#### Bhavik Mehta (Oct 11 2020 at 22:33):

I might be misremembering what you're trying to prove though

#### Alena Gusakov (Oct 12 2020 at 01:55):

i think i got stuck trying to do exactly that

#### Alena Gusakov (Oct 12 2020 at 02:59):

Trying to figure out how to define matchings currently. I'm thinking some structure like

structure matching_on (G : simple_graph) :=
(disjoint : )


#### Alena Gusakov (Oct 12 2020 at 02:59):

where disjoint is the property that the edges are disjoint

#### Alena Gusakov (Oct 12 2020 at 03:00):

but I'm not quite sure how to get there

#### Alena Gusakov (Oct 12 2020 at 03:00):

maybe a class? something like

class matching (M : set (sym2 (V G))) :=
(disjoint : ∀ e f ∈ M, ∀ v : V G, v ∈ e → v ∉ f)


#### Kyle Miller (Oct 13 2020 at 06:58):

A class seems like a reasonable approach. I haven't tested it, but maybe this definition?

class matching (M : set (sym2 (V G))) :=
(sub_edges : M ⊆ E G)
(disjoint : ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f)

class perfect_matching (P : set (sym2 (V G))) extends matching P :=
(cover : ∀ v : V G, ∃ e ∈ P, v ∈ e)


#### Kyle Miller (Oct 13 2020 at 07:02):

There are upsides and downsides to classes for this, so you might need to experiment. Structures would be fine too, but if you had a perfect matching, you'd need to use its to_matching function to turn it into a matching when necessary.

Another thing to consider is predicates

def matching {G : simple_graph} (M : set (sym2 (V G)) := M ⊆ E G ∧ ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f
def perfect_matching {G : simple_graph} (P : set (sym2 V G)) := matching P ∧ ∀ v : V G, ∃ e ∈ P, v ∈ e


but a downside here is that you can't access the sub-properties as easily.

#### Alena Gusakov (Oct 13 2020 at 21:45):

ah yeah thank you, the class definition you gave makes more sense

#### Alena Gusakov (Oct 13 2020 at 21:46):

forgot to add the part where the edges come from G

#### Bhavik Mehta (Oct 14 2020 at 12:55):

I feel like you want a structure rather than a class (they can also extend) since you might want to consider multiple matchings on the same set

#### Kyle Miller (Oct 14 2020 at 18:11):

I was thinking that too, but then I realized Alena's class was the matching itself, and all the fields are just propositions so the class is a subsingleton. It seems like it's similar to using mono.

#### Bhavik Mehta (Oct 14 2020 at 21:16):

I think mono should be a proposition though :) I think that change is gonna happen in the category theory library as soon as someone actually puts in the effort to make it

#### Alena Gusakov (Oct 17 2020 at 16:38):

Is there something we can do about the builds failing?

#### Alena Gusakov (Nov 23 2020 at 14:36):

I've been away for a bit so I'm a bit out of the loop, are we still trying to go with the definition simple_graph_on where we turn it into simple_graph later? Just looking at the file in mathlib and it doesn't seem to be the case right now

#### Alena Gusakov (Nov 23 2020 at 14:40):

If we are going to do that then I can start slicing off simple_graphs2 into PRs

#### Alena Gusakov (Nov 23 2020 at 14:50):

Btw I think when I was initially trying to figure things out I muddled up a lot of the code in simple_graphs2 so I'm sorry if that caused anyone to step back

#### Jalex Stark (Nov 24 2020 at 22:47):

I think the simple_graph_on proposal is still the best one, and I'd support you in making PRs about it

#### Aaron Anderson (Nov 25 2020 at 00:19):

I’d be happy to help a PR to refactor to simple_graph_on etc. if someone else gets it started

#### Aaron Anderson (Nov 25 2020 at 00:21):

(Mostly I’m volunteering to translate over the friendship graph material)

#### Alena Gusakov (Nov 25 2020 at 00:40):

I think we pretty much do have everything refactored ah wait, forgot that we need to catch up to all of the mathlib changes since september

#### Alena Gusakov (Nov 25 2020 at 00:40):

Like, I didn't even need to do the work, it's already there in simple_graphs2

#### Alena Gusakov (Nov 25 2020 at 00:40):

But I'll pull the file into its own PR

#### Alena Gusakov (Dec 02 2020 at 20:40):

So I managed to adapt some of the lemmas and definitions from simple_graphs2 into a branch that doesn't rely on simple_graph_on

#### Alena Gusakov (Dec 02 2020 at 20:45):

@Bhavik Mehta just gonna pull you into this conversation cause I'm probably not going to be able to explain why I wasn't using simple_graph_on very well

#### Alena Gusakov (Dec 02 2020 at 20:46):

Also @Eric Wieser

#### Aaron Anderson (Dec 02 2020 at 20:49):

I think it still makes sense to eventually have a PR that adds no new features, and just converts to simple_graph_on, because I think that conversion will cause enough discussion by itself.

#### Aaron Anderson (Dec 02 2020 at 20:50):

You could always have another PR that is blocked by that simple_graph_on PR, adding features on top of simple_graph_on, if you think that those features would be a good demonstration of why simple_graph_on is good.

#### Alena Gusakov (Dec 02 2020 at 20:55):

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

#### Alena Gusakov (Dec 02 2020 at 20:56):

The one annoying thing is not using simple_graph_on means we don't have the special notation for adjacency

#### Alena Gusakov (Dec 02 2020 at 20:56):

But if I do find problems/advantages I'll try to do that

#### Kyle Miller (Dec 02 2020 at 21:20):

Alena Gusakov said:

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

We haven't gotten to subgraphs in mathlib yet is why :smile:

I think it's better to leave it as simple_graph for now and then do the refactor later when a simple_graph_on is clearly needed -- and since putting it off might cause more work, I'm willing to do it when it comes to that. (I think it will actually be less work long-term to not change it now.)

#### Alena Gusakov (Dec 02 2020 at 21:21):

Got it, I'll try to do subgraphs in the next PR (assuming this first one gets approved)

#### Hunter Monroe (Jul 06 2021 at 18:28):

@Alena Gusakov can I do a pull request with subgraph.lean and hom.lean from the simple_graph_subgraph branch? I would add a definition of graph isomorphism.

abbreviation iso (G : simple_graph V) (G' : simple_graph W) : Type (max u v) :=


Go for it!

#### Alena Gusakov (Jul 06 2021 at 19:48):

I don't remember how much I did with that branch tbh

#### Kyle Miller (Jul 06 2021 at 20:32):

For what it's worth, @Aaron Anderson had written the following for a PR a while back. It seems fine, though I think the definition of embedding is surprising for graphs (I think you'd want a result that every subgraph of $G$ embeds in the graph $G$ -- so an embedding would be an injective homomorphism). I think the terminology comes from model theory -- it's a useful concept, but I don't know the proper graph-theoretic terminology for it.

section maps

variables {W : Type*} (G) (H : simple_graph W)

/-- A graph homomorphism maps adjacent vertices to adjacent vertices -/

infix  →g  : 50 := hom

/-- A graph embedding is an embedding f such that for vertices v w : V,
G.adj f(v) f(w) ↔ G.adj v w -/

infix  ↪g  : 50 := embedding

/-- A graph isomorphism is an equivalence that preserves adjacency-/

infix  ≃g  : 50 := iso

end maps


(deleted)

#### Hunter Monroe (Jul 07 2021 at 16:23):

A relationship embedding rel_embedding maps G to an induced subgraph of H (a bijection for all edges of the involved vertices of H), right? Also, I want to be certain that all of these maps are injective, which is my reading of the definitions.

Kyle Miller said:

abbreviation embedding := rel_embedding G.adj H.adj


#### Hunter Monroe (Jul 07 2021 at 16:30):

I will leave out embedding which is an obscure concept within graph theory. The only reference I could find was to "induced subgraph isomorphism" within complexity theory.

#### Yakov Pechersky (Jul 07 2021 at 16:52):

Embedding is by definition injective. An injective map can be called an embedding. Not all rel_homs will be injective.

#### Kevin Buzzard (Jul 07 2021 at 16:53):

In topology an embedding is a specific kind of injective map -- the words aren't entirely interchangeable

#### Bhavik Mehta (Jul 07 2021 at 16:59):

Hunter Monroe said:

I will leave out embedding which is an obscure concept within graph theory. The only reference I could find was to "induced subgraph isomorphism" within complexity theory.

embeddings essentially let you define induced subgraphs, which I'd argue aren't at all obscure, I think they should definitely be added

#### Kyle Miller (Jul 07 2021 at 17:16):

Yeah, I didn't mean to suggest that rel_embedding was obscure, just that calling it an "embedding" seems to be. I personally think hook arrow for "injectively maps onto an induced subgraph" would be surprising, but I'm happy to follow consensus.

@Kevin Buzzard At least in this case, injective homomorphisms induce topological embeddings for the graphs' geometric realizations as CW complexes.

#### Kevin Buzzard (Jul 07 2021 at 17:21):

There is a more general concept of injection where you're allowed to send adjacent vertices to non-adjacent vertices which are connected by a path I guess. I remember learning the statement (but not proof) of a theorem of perhaps Kuratowski saying that topological K5's and K(3,3)'s are the only obstruction to planarity

#### Kyle Miller (Jul 07 2021 at 17:24):

The rel_embedding definition is a regular monomorphism, but the injective rel_hom definition is a monomorphism, in the category of simple graphs where maps have to preserve adjacency. There are at least two different ways to define this category, however (and ncatlab describes both). In the other one, maps can send adjacent pairs to adjacent pairs, or collapse them to a single vertex.

#### Kyle Miller (Jul 07 2021 at 17:25):

Maybe this is why they deserve to be called embeddings, now that I've thought it through again in front of everyone.

#### Hunter Monroe (Jul 08 2021 at 00:57):

I have created a pull request for subgraph and maps (homomorphism, isomorphism, embedding).

#### Johan Commelin (Jul 08 2021 at 04:41):

@Hunter Monroe Just fyi, if you type #8223 in Zulip, it will render as #8223 and also link to your PR.

#### Hunter Monroe (Jul 08 2021 at 13:39):

I have incorporated review comments and reverted the formatting. Note one substantive change at @Bhavik Mehta's suggestion: hom and iso no longer assume that G and G' have vertices of the same type.

#### Bhavik Mehta (Jul 08 2021 at 13:52):

Note that Kyle's suggestion above also did not have this assumption

#### Kyle Miller (Jul 08 2021 at 16:31):

How do we want naming of lemmas for subgraphs to work? There are a number of useful definitions and lemmas for subgraphs that reflect lemmas about simple graphs. Right now in the PR, they use ' to distinguish them. For example, simple_graph.edge_set versus subgraph.edge_set'. It seems like it would be sensible going for subgraph.edge_set since namespaces or dot notation can distinguish them.

#### Kyle Miller (Jul 08 2021 at 16:32):

I'm also wondering about where subgraph should live. It seems like the name will conflict with subgraphs of other types of graphs, like multigraphs. Should it be put into the simple_graph namespace?

#### Hunter Monroe (Jul 08 2021 at 17:50):

My thought was to put subgraph under simple_graph, and in the next PR generalize to allow directed graphs, etc.

#### Kyle Miller (Jul 08 2021 at 17:55):

Right now subgraph is not in the simple_graph namespace -- it might be the combinatorics.simple_graph.subgraph module, but inside the file you have to manage namespaces yourself. I'm essentially suggesting that inside this module, there should be namespace simple_graph rather than open simple_graph, but I'm wondering what other graph theorists think.

#### Kyle Miller (Jul 08 2021 at 17:59):

Hunter Monroe said:

in the next PR generalize to allow directed graphs, etc.

Would you mind discussing this in a new topic here in the #graph theory stream? Even simple_graph went through a good amount of redesign before it made it into mathlib.

#### Hunter Monroe (Jul 08 2021 at 19:02):

@Kyle Miller I see two options for pursuing that issue: (1) put this version of subgraph in the simple_graph namespace since it clearly only applies to simple graphs given the presence of sym', and delay broader discussions about a broader structure that encompasses multigraphs and directed graphs while wrapping up this PR (this is my preference), or (2) consider the broader structure including how subgraph fits in before wrapping up this PR. I am worried that we could get bogged down this way, and there is some history of that. We could get lost trying to build a subgraph concept for directed multi hypergraphs. If I have misunderstood the question you are asking, let me know.

#### Kyle Miller (Jul 08 2021 at 19:30):

@Hunter Monroe (1) is what I meant. I had been expecting each notion of graph will have its own notion of subgraph, which is why I bring this up.

#### Kyle Miller (Jul 08 2021 at 19:36):

(For some context, I had written about three or four different definitions of subgraph, and after some experimentation the one you've kindly PR'd seemed to be the best one. There wasn't really anything that used subgraphs yet, so the work to polish it and PR it hadn't happened...)

#### Kyle Miller (Jul 08 2021 at 19:37):

By the way, I knew that there was some place where I had developed it more (like when I mentioned there was a version when I had removed all the primes), and I just found it: https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/subgraph.lean (sorry)

#### Kyle Miller (Jul 08 2021 at 19:38):

I also understand the purpose of adj_symm now. It's that symmetric is a one-way implication, but it's nice to have it as an iff.

#### Kyle Miller (Jul 08 2021 at 20:12):

@Hunter Monroe By the way, I'm happy to help with merging this subgraph.lean with yours for the PR.

#### Hunter Monroe (Jul 08 2021 at 20:31):

I will give it a try.

#### Kyle Miller (Jul 08 2021 at 20:37):

Feel free to defer as much as you want to a later PR. ( Also, I'm not sure all of it makes sense.)

It turns out there's also a bunch of stuff about homomorphisms here https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/hom.lean (This can also wait)

#### Yaël Dillies (Jul 08 2021 at 20:44):

Kyle Miller said:

I also understand the purpose of adj_symm now. It's that symmetric is a one-way implication, but it's nice to have it as an iff.

Then it should be called adj_comm

#### Yaël Dillies (Jul 08 2021 at 20:45):

The rule is unfortunately quite lax, but having symmlemmas to be one-way and comm lemmas to be two-ways (so including equality) is pretty useful to the ear.

#### Kyle Miller (Jul 08 2021 at 20:50):

I wasn't aware of this convention -- this should be fixed in simple_graph/basic.lean then with edge_symm, which probably should be called adj_comm. (I don't remember how it got the name edge_symm exactly.)

#### Kyle Miller (Jul 08 2021 at 20:55):

Maybe it would make sense to rename sym in the simple_graph structure to adj_symm, add the @[symm] attribute to it, and delete the edge_symm' lemma. (This might not all work due to the obviously autoparam.)

(If I recall, it's sym rather than symm so it doesn't conflict with the symm in the root namespace, which isn't actually used by the library.)

#### Hunter Monroe (Jul 09 2021 at 15:07):

@Kyle Miller actually yes could you help with this? Merging subgraph.lean would also affect basic.lean including additional code from hom.lean.

Kyle Miller said:

Hunter Monroe By the way, I'm happy to help with merging this subgraph.lean with yours for the PR.

#### Kyle Miller (Jul 09 2021 at 19:33):

Thanks for your work, @Hunter Monroe, to get this PR together. I think I'm done editing now.

#### Kyle Miller (Jul 09 2021 at 19:34):

Oh, there are some linter errors and other errors to fix still. I'll try to take care of those

#### Kyle Miller (Jul 09 2021 at 21:31):

#8223 seems ready for more review

Part of this, I changed edge_symm to adj_comm, as suggested by @Yaël Dillies

#### Hunter Monroe (Jul 09 2021 at 22:45):

Looks good, let's see what the reviewers think.

Here is an approach for handling any type of graph in one framework. A typeclass graph has a set of vertices V, a type E for edges which is a multiset, and a function incidence that maps each edge to a subset of V. This is enough to define a generic approach to subgraphs and maps. An instance specifies what an edge is: an unordered pair of V without loops and without duplication (graph), an ordered pair of V with the same constraints (direct graph), edges with more than two vertices with the same constraints with permuting those vertices gives the same edge (hypergraph), without such permuting (directed hypergraph), and allow duplication (multigraph), etc. The condition for G' to be a subgraph of G is generic: given any subset VS of V, the multiset of edges of G' incident on VS is a submultiset of the multiset of edges of G incident on VS. The maps can also be defined generically. All the action happens in the definition of edge. The constraints can be stated generically: has_symm (permuting the vertices gives the same edge), no_loops, 2_edge (two vertices per edge), n_edge (hypergraphs), no_dups (does not hold for multigraphs).

#### Kyle Miller (Jul 09 2021 at 23:18):

Here's a proposal along those lines (and similar to something I worked on for a while to try to make it so that submultigraphs could be used as if they were multigraphs):

class graph_like (α : Type*) :=
(V : α → Type*)
(E : α → Type*)
(incidence : Π (G : α), E G → set (V G))

-- Example instance
instance (V : Type*) : graph_like (simple_graph V) :=
{ V := λ G, V,
E := λ G, G.edge_set,
incidence := λ G e, {v : V | v ∈ (e : sym2 V)} }


A tradeoff with this is that you lose dot notation if you only have generic code.

There's also a question about whether having generic code will result in less code overall.

#### Kyle Miller (Jul 09 2021 at 23:29):

Before the definition of subgraph that was in this PR, there was a definition involving a subset of the edge set of the simple graph, rather than a sub-relation of the adjacency relation. This wasn't so easy to work with because there were levels of stuff you had to get through (like sym2).

#### Kyle Miller (Jul 09 2021 at 23:33):

To be clear, I do like this idea of having something that would let there be generic definitions, and I like the ideas you have. The design trick is figuring out how to do this in a way that is ergonomic and that definitely makes things simpler. It's worth designing something generic, even right now, but also I think in the short term making non-generic things is a good way to inform a generic design.

Re ergonomics: if anyone looks at that directed_graph definition I made, one annoying problem is that the adjacency relation G.adj v w renders as G.to_directed_graph.adj v w. Maybe a reducible definition can fix this? I was wanting to avoid a notation, but perhaps there will eventually a v ~[G] w defined by something like

notation v ~[ G ] w := ∃ (e : graph_like.E G), graph_like.incidence G e = {v, w}


#### Yaël Dillies (Jul 10 2021 at 07:03):

Hunter are you sure this works that great with hypergraphs? Hypergraphs want set V → Prop and multigraphs want V → V → Prop.

#### Yaël Dillies (Jul 10 2021 at 07:09):

Kyle Miller said:

Here's a proposal along those lines (and similar to something I worked on for a while to try to make it so that submultigraphs could be used as if they were multigraphs):

I actually kind of like this presentation! Not being a multigraph then becomes injective incidence. The problem I see is that set (V G ) doesn't allow you to express oriented edges. Also, we don't have to use only generic code. We can redefine functions for every kind of graphs we care about and use the common API to avoid boilerplate.

#### Kyle Miller (Jul 10 2021 at 07:11):

An unspoken idea here is that this is only giving a common interface. A directed graph is free to peer into the E type, for example.

#### Kyle Miller (Jul 10 2021 at 07:12):

I'm curious what you mean about set V -> Prop and V -> V -> Prop. What's the objection?

#### Kyle Miller (Jul 10 2021 at 07:47):

Here's another multigraph definition along with a graph_like instance:

/-- Multigraphs as graphs with labeled edges. An edge is identified with the
unordered pair of endpoints and the label. -/
structure multigraph (V : Type*) (α : Sort*) :=
(links : set (α × V × V))
(sym : prod.map id prod.swap '' links = links)

def multigraph.is_simple {V : Type*} {α : Sort*} (G : multigraph V α) :=
∀ {a : α} {v w : V}, (a,v,w) ∈ G.links → v ≠ w

def multigraph.edges {V : Type*} {α : Sort*} (G : multigraph V α) : set (α × sym2 V) :=
(λ (l : α × V × V), (l.1, ⟦(l.2.1, l.2.2)⟧)) '' G.links

instance (V : Type*) (α : Sort*) : graph_like (multigraph V α) :=
{ V := λ _, V,
E := λ G, G.edges,
incidence := λ G e, {v : V | v ∈ e.1.2}}


#### Kyle Miller (Jul 10 2021 at 07:55):

I like how this definition of multigraph exposes some useful parameters, lets you give edges identity, and is fairly simple. It even would have a lattice instance. (The seemingly unattainable property is to also have it so that the degree-sum formula will work with loop edges without special casing or having a significantly more complicated definition. Here, there is a single element of links for loop edges, and two elements for non-loop edges.) The "links" terminology comes from a paper by Chou, "A formal theory of undirected graphs in higher-order logic", 1994. In that paper, there are additional constraints that each edge has its own unique label and all the labels are used. I think that can be relaxed.

Last updated: Dec 20 2023 at 11:08 UTC