# Zulip Chat Archive

## Stream: graph theory

### Topic: multigraph definition

#### Kyle Miller (Aug 18 2020 at 02:34):

Something that seems like a good definition for multigraphs is

[Chou94] Chou, Ching-Tsun. "A formal theory of undirected graphs in Higher-Order Logic." (1994) https://doi.org/10.1007/3-540-58450-1_40

I remember there also being some things in

Doczkal, Christian and Pous, Damien. (2019). Graph Theory in Coq: Minors, Treewidth, and Isomorphisms

The Chou approach is to have a vertex type `V`

and an edge type `E`

, then take a set of *links* on `V × E × V`

such that the projection onto `E`

is surjective, such that the set of links is closed under swapping the two vertices, and such that if two links project to the same edge then they are the same up to swapping.

Conceptually, a link is an edge orientation (for non-loop edges -- loop edges only have a single associated link).

There's an implementation of it at https://github.com/leanprover-community/mathlib/tree/graphs/src/combinatorics/graphs but I don't remember exactly what state the branch is in...

#### Kyle Miller (Jan 07 2021 at 23:09):

There are many ways to define unoriented multigraphs, and one of the sticking points to using Chou's definition is that the definition of `degree`

isn't very nice. My educated opinion for the design: a single-vertex graph with a single loop edge should have degree 2, since there are two incident half edges ("darts"). Chou's definition has a single link per loop edge but two links per non-loop edge, so you can't just count incident links to get the degree.

Here are five different definitions of multigraphs: https://gist.github.com/kmill/16257d58a662e570d4762723e762c7a8

I'm thinking something like `multigraph₄`

is the best, though its disadvantage is that you don't have an edge set per se, but at least in my applications "labeled edge" tends to actually mean "labeled dart." If you need labeled edges.

#### Kyle Miller (Jan 07 2021 at 23:10):

Anyway, if you have any other ideas for the definition of a multigraph (along with test implementations for some basic accessor functions, especially the `degree`

interface), please post them!

It'd be good to also think about how sub-objects would work for each design.

#### Kyle Miller (Jan 08 2021 at 00:01):

A commutative diagram for the structure of an unoriented multigraph along what the maps are supposed to mean:

image.png

#### Peter Nelson (Jan 08 2021 at 14:43):

I've been thinking a little about multigraphs, since they are the right setting for graphic matroids. I think a quite important test is whether it is easy to contract a set of edges. If contraction isn't easy, you're closing off some of the deepest work in graph theory.

I am in favour of a definition that eliminates the need for darts. Here is one in terms of a nat-valued 'incidence function', with math rather than code. A multigraph is a triple (V,E,inc), where V and E are sets, and inc is a function from V x E to nat, that sums to exactly 2 over each edge. If e has ends v1 and v2, then inc(v,e1) = inc(v,e2) = 1, and if e is a loop at v, then inc(v,e) = 2. Hence, the degree of v is just sum (inc( v, . )). This correctly allows loops to contribute degree 2, and proves the handshake theorem by formally reversing the order of summation.

Further, one can contract edges easily; to contract a set X of edges, you quotient V by the equivalence relation whose classes are the components of the subgraph G[X]; then the contraction G/X has this quotient as a vertex set, and its incidences come from summing inc over equivalence classes. This correctly turns nonloop edges into loops where appropriate, contracts non-parallel edges into parallel, etc etc.

#### Kyle Miller (Jan 10 2021 at 18:12):

Thanks @Peter Nelson, that's a clever encoding, and it's worth trying it out. I added my attempt at a formalization of that as `multigraph₆`

in the gist. One complexity is that the sum is over an infinite set, so I added in a `finset`

support for the summation (I think it's important to be able to handle infinite multigraphs). Another change I made was to have a special `inc_type`

enumeration rather than a `nat`

so that doing things by cases is easier.

That's a good point about needing to support contractions (or, better, minors). I figured being able to define `degree`

shows a basic amount of viability for a multigraph definition, and a definite next step would be to try to implement contraction/minors.

#### Kyle Miller (Jan 10 2021 at 18:15):

(I'll try to get around to make a proper mathlib branch with the definitions under consideration, with one file per multigraph definition. Doing a gist for now was just easier to try to get the conversation going.)

#### Kyle Miller (Jul 10 2021 at 20:02):

Here's another entry for a multigraph definition, and it seems rather promising to me. There's also a potential definition for graph minors that should have reasonable relationships between contraction and deletion. A small difference from the usual notion of a graph minor is that if labels are re-used in the multigraph then when contracting edges might merge.

```
structure multigraph (V : Type*) (α : Type*) :=
(labels : V → V → set α)
(sym : ∀ v w, labels v w = labels w v) -- flip labels = labels
namespace multigraph
variables {V : Type*} {α : Type*} (G : multigraph V α)
@[reducible]
def adj (v w : V) : Prop := (G.labels v w).nonempty
lemma adj_comm {v w : V} : G.adj v w ↔ G.adj w v :=
by simp [adj, G.sym]
def loopless := irreflexive G.adj
def to_simple_graph (h : G.loopless) : simple_graph V :=
{ adj := G.adj,
loopless := h,
sym := λ v w hvw, by rwa adj_comm }
def labels' : sym2 V → set α :=
quotient.lift (function.uncurry G.labels) begin
rintros _ _ (_|⟨v, w⟩),
refl,
exact G.sym v w,
end
/-- We go through this work to define it this way so that `mem_edge_set` is proved by `refl` -/
def edge_set : set (sym2 V × α) := set_of $ function.uncurry (λ e v, v ∈ G.labels' e)
def incidence_set (v : V) : set (sym2 V × α) := {e ∈ G.edge_set | v ∈ e.1}
@[simp]
lemma mem_edge_set {v w : V} {a : α} : (⟦(v, w)⟧, a) ∈ G.edge_set ↔ a ∈ G.labels v w :=
iff.rfl
/-- The degree where incident loop edges are counted once. -/
def degree' (v : V) [fintype (G.incidence_set v)] : ℕ :=
fintype.card (G.incidence_set v)
/-- The degree where incident loop edges are counted twice (once for each incident half edge).
This satisfies the degree-sum formula `∑ (v : V), G.degree v = 2 * card G.edge_set`. -/
def degree (v : V) [fintype (G.incidence_set v)] [fintype (G.labels v v)] : ℕ :=
G.degree' v + fintype.card (G.labels v v)
/-- A multigraph obtained from deleting vertices and contracting and deleting edges of a pre-existing multigraph.
We delete all edges outside `keep` and contract all edges inside `contr`. -/
structure minor (G : multigraph V α) :=
(keep_verts : set V)
(contr : set (sym2 V × α))
(keep : set (sym2 V × α))
(contr_sub : contr ⊆ keep)
(keep_sub : keep ⊆ G.edge_set)
(keep_has : ∀ {e v}, e ∈ keep → v ∈ prod.fst e → v ∈ keep_verts)
variables {G}
def to_minor : G.minor :=
{ keep_verts := set.univ,
contr := ∅,
keep := G.edge_set,
contr_sub := set.empty_subset _,
keep_sub := set.subset.rfl,
keep_has := λ _ _ _ _, set.mem_univ _ }
/-- The relation that generates which vertices are identified -/
def minor.rel (G' : G.minor) (v w : G'.keep_verts) : Prop := ∃ (a : α), (⟦(coe v, coe w)⟧, a) ∈ G'.contr
def minor.verts (G' : G.minor) := quot G'.rel
/-- The labels on `G` itself after deleting those outside `keep` and inside `contr`. -/
def minor.labels' (G' : G.minor) (v w : V) : set α :=
{a : α | a ∈ G.labels v w ∧ (⟦(v, w)⟧, a) ∈ G'.keep \ G'.contr}
/-- The labels of the minor. -/
def minor.labels (G' : G.minor) (v' w' : G'.verts) : set α :=
{a : α | ∃ (v w : G'.keep_verts), v' = quot.mk G'.rel v ∧ w' = quot.mk G'.rel w ∧ a ∈ G'.labels' v w}
def minor.to_multigraph (G' : G.minor) : multigraph G'.verts α :=
{ labels := G'.labels,
sym := λ v' w', begin
ext a,
simp only [minor.labels, minor.labels', set_coe.exists, set.mem_diff,
exists_and_distrib_right, exists_and_distrib_left, set.mem_set_of_eq, subtype.coe_mk],
split;
{ rintro ⟨v, ⟨hv, rfl⟩, w, ⟨hw, rfl⟩, h⟩,
use w, use hw, use v, use hv, simpa [sym2.eq_swap, G.sym], },
end }
end multigraph
```

#### Kyle Miller (Jul 10 2021 at 20:16):

Comparing to the other versions in the gist a few messages up, this is like `multigraph₅`

but easier to work with. It's also nice how it mirrors the `simple_graph`

definition as `multigraph V unit`

(ignoring looplessness), and like `simple_graph`

it could be split up so it extends a `multidigraph`

.

#### Kyle Miller (Jul 10 2021 at 20:22):

A `submultigraph`

definition using this, mirroring the `simple_graph.subgraph`

definition in #8223:

```
structure submultigraph (G : multigraph V α) :=
(verts : set V)
(labels : V → V → set α)
(labels_sub : ∀ {v w : V}, labels v w ⊆ G.labels v w)
(edge_vert : ∀ {v w : V}, (labels v w).nonempty → v ∈ verts)
(sym : ∀ {v w : V}, labels v w = labels w v . obviously)
```

#### Kyle Miller (Jul 11 2021 at 00:18):

Though a definition for homomorphisms of these kinds of multigraphs seems to be less nice than they might be. Here's one avoiding any kinds of coercions:

```
/-- Homomorphisms of multigraphs. Defined in such a way that they are extensional. -/
@[ext]
structure hom {V V' α α'} (G : multigraph V α) (G' : multigraph V' α') :=
(on_verts : V → V')
(on_labels : Π {v w : V} (a : α), a ∈ G.labels v w → α')
(mem_labels : ∀ {v w : V} {a : α} (h : a ∈ G.labels v w), on_labels a h ∈ G'.labels (on_verts v) (on_verts w))
(sym : ∀ {v w : V} (a : α) (hvw : a ∈ G.labels v w) (hwv : a ∈ G.labels w v), on_labels a hvw = on_labels a hwv)
lemma mem_labels_comm {v w : V} {a : α} : a ∈ G.labels v w ↔ a ∈ G.labels w v :=
by rw G.sym
lemma hom.sym' {V V' α α'} (G : multigraph V α) (G' : multigraph V' α') (f : hom G G')
{v w : V} (a : α) (hvw : a ∈ G.labels v w) : f.on_labels a hvw = f.on_labels a (G.mem_labels_comm.mp hvw) :=
f.sym a _ _
```

It's probably silly writing the `sym`

member that way, rather than using `sym'`

directly, due to proof irrelevance.

#### Kyle Miller (Jul 11 2021 at 00:29):

This is the "more natural" definition given the `multigraph`

structure, but it might be considered to be slightly odd:

```
@[ext]
structure hom' {V V' α α'} (G : multigraph V α) (G' : multigraph V' α') :=
(on_verts : V → V')
(on_labels : α → α')
(mem_labels : ∀ {v w : V} {a : α}, a ∈ G.labels v w → on_labels a ∈ G'.labels (on_verts v) (on_verts w))
```

Though if each label is used exactly once, it's exactly the definition you want, so maybe it's ok.

#### Kyle Miller (Jul 11 2021 at 00:34):

And also if a `simple_graph`

is a loopless `multigraph V unit`

, this `hom'`

definition corresponds to homomorphisms of simple graphs.

#### Barrie Cooper (Jul 30 2021 at 13:59):

Hi. I'm new to Zulip and fairly new to Lean. I've been coding up some definitions and theorems on (multi)graphs, morphisms and isomorphisms from my 3rd-year course with the vague aim of getting students to play with some of these (e.g. as a "graphs game" like the natural number game). Thanks to all for the inspiring work you've done so far.

Anyway, if anyone is interested my approach is here: https://github.com/barriecooper/lean-graphs/. Feedback is very welcome (like I said, I'm fairly new to Lean). Thanks also to my colleague Gihan Marasingha for encouraging me to post something here.

#### Kevin Buzzard (Jul 30 2021 at 18:05):

I would really encourage you with this stuff -- I have a bunch of positive feedback for the natural number game but the other "games" I made which weren't interactive (e.g. the complex number game, which just involves filling in sorrys in VS Code) are far less popular.

#### Kevin Buzzard (Jul 30 2021 at 18:06):

Do you host preliminary versions anywhere? I used to put NNG experimental versions at `http:my_website/NNG_new_version`

or whatever

#### Kevin Buzzard (Jul 30 2021 at 18:06):

and I'd get Imperial kids to play them and watch them closely to see where they needed help.

#### Kevin Buzzard (Jul 30 2021 at 18:07):

One reason NNG is popular around Imperial is that the 1st year students actually have to take an exam on this stuff at the end of October each year! Not on Lean but on the material.

#### Barrie Cooper (Jul 30 2021 at 18:07):

@Kevin Buzzard : I've got a rough draft here: https://barriecooper.github.io/html/index.html. But that's basically my Lean file converted into the game. I need to put better discussion and hints for the various theorems and tactics needed.

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

@Barrie Cooper Looks nice! The definitions you've chosen seem good for a Graphs Game.

Something that might be useful (but not essential), if you want to have exercises involving different graphs with the same vertices, is pulling out `vertices`

like so:

```
structure graph (V : Type) :=
(edges : Type)
(endpoints : edges → sym2 V)
```

That's at the cost of needing two hypotheses `(V : Type) (g : graph V)`

when you want to introduce a graph, though.

You can still talk about graphs with a particular vertex type with your definition:

```
structure graph :=
(vertices : Type)
(edges : Type)
(endpoints : edges → sym2 vertices)
def graph_on (V : Type) := {g : graph // g.vertices = V}
```

However, this can get complicated because equalities between types (as in `g.vertices = V`

) can get very messy.

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

If the only way you're comparing graphs is through graph homomorphisms, then you can ignore what I'm saying.

#### Barrie Cooper (Jul 30 2021 at 18:16):

Thanks @Kyle Miller . I'm not sure how much I care about whether I want to use the same vertex/edge sets/types yet. I guess that will emerge if/when I define subgraphs, contraction-deletion, spanning trees etc. At one level, I'm perfectly happy to define subgraphs in terms of injective morphisms ...

I'm only just getting to grips with what Lean thinks is obvious regarding types and what it can't figure out ... so probably you're many steps ahead of me in seeing the potential problems :)

#### Kyle Miller (Jul 30 2021 at 18:24):

It's nice having subgraphs be a special type because then you get a bounded lattice. You can still take "unions" and "intersections" of injective morphisms, but things like associativity of unions become more elaborate, needing an associator.

Subgraphs can also a way to avoid the issues I was talking about -- you can have a `graph`

that's complete in some sense (i.e., has a large edge type with as many edges as you need between every pair of vertices), and then you study subgraphs of this. This way all the graphs under consideration have vertices and edges coming from the same types, which is a nice property when you want to rely on equality.

#### Yakov Pechersky (Jul 30 2021 at 18:25):

Barrie, are you familiar with the concept of "bundled morphisms" and "bundled equivalences"? In mathlib, most things that encode bijections are phrased as explicitly encoding both the forward and inverse functions. Your theory has isomorphisms as Props, which will make it difficult to "evaluate" the inverse of an isomorphism. Similarly, bundling morphisms allows you to say things like `f.comp g`

for your (f : H ↦ K) (g : G ↦ H) (modulo choice of argument/composition order)

#### Barrie Cooper (Jul 30 2021 at 18:28):

@Yakov Pechersky: No, but @Gihan Marasingha mentioned this when we had a video chat earlier today.

#### Barrie Cooper (Jul 30 2021 at 18:43):

@Kyle Miller : Yes, I see what you mean, but I'm also quite happy having an associator. I think I'd rather "H is a subgraph of G" to mean "there exists an injective morphism from H to G". Then a statement like "$A_2$ is a subgraph of $A_3$" is true irrespective of my constructions of $A_2$ and $A_3$.

But maybe I'll change my mind tomorrow, or next month ...

#### Yakov Pechersky (Jul 30 2021 at 18:51):

Would you more likely be using `is_subgraph X Y`

as a hypothesis, or as something to be proven? Also, if you assume classical logic, you can always extract an injective morphism from a proof of "there exists an injective morphism...".

#### Barrie Cooper (Jul 30 2021 at 19:01):

I think both ... and yes, I'm thinking primarily in terms of classical logic. That said, I'm interested to understand the alternatives and the advantages of the different approaches.

I'm also mindful of the audience and whilst I love abstractions and generalisations of theories so that they become more universal, there's a potential trade-off with them becoming incomprehensible or impractical for the ordinary user .... and a fortiori to students.

#### Yakov Pechersky (Jul 30 2021 at 19:04):

If I had a term of `H.is_subgraph_of G`

, then that could also be interpreted as, for example, `Hv ->_inj Gv`

where `Hv`

is the type of vertices of H (resp. G), and other generalizing coercions like `Hv -> Gv`

, where one forgets the injectivity. Coercions, when notated explicitly, can be confusing. However, we utilize them all the time implicitly in proofs and arguments when working in nonformal settings.

#### Yaël Dillies (Jul 30 2021 at 19:12):

Barrie Cooper said:

Then a statement like "$A_2$ is a subgraph of $A_3$" is true irrespective of my constructions of $A_2$ and $A_3$.

Note that another option is to define the same graph on different types, typically as a function `Π {α : Type*}, graph α`

.

#### Barrie Cooper (Jul 30 2021 at 19:57):

I'm not sure I follow ...

@Yakov Pechersky : Sure, but I've defined a morphism of graphs explicitly as a triple consisting of a vertex map, an edge map, and a compatability condition. As such, no additional coercion is needed, right?

@Yaël Dillies : Sure, it's not the types I'm so concerned about. If I construct A_2 with vertex set {1, 2} and A_3 with vertex set {3, 4, 5}, then "subgraph of" in terms of subsets doesn't work --- well, it's a lot more constrained than I'd want. I'd need to "consistently" define A_n on the set {1, ..., n}, say ... and I think I'd rather not do that (and I definitely don't want to force students to use any particular construction).

Apologies if I've misunderstood your comments ...

#### Yakov Pechersky (Jul 30 2021 at 20:00):

What I mean by coercion is not in the constructing or providing a morphism. Rather, given a morphism, utilizing it as an injective map from vertices to vertices, for example.

#### Barrie Cooper (Jul 30 2021 at 20:05):

... but that's part of the definition? If a morphism contains both the vertex map and edge map, and by "injective" we mean that both are injective, then I don't see the issue. Yes, the "injective morphism" is distinct from the "injective vertex map", but I'm never using the same notation/name/language. (In fact, I wouldn't actually even use the term "injective morphism" ... with students I use the term "embedding" because a morphism of graphs is a pair of functions rather than a single function.)

I don't see where any coercion happens ... in fact, I think I've been careful to define things so that I'm never having to worry about coercion.

#### Kyle Miller (Jul 30 2021 at 20:09):

@Yakov Pechersky This might be a difference between algebraic structures with a primary type of elements (like most things in algebra) and graphs. The situation might be more similar to docs#category_theory.functor, which I don't think has a coercion to the `obj`

function.

#### Yakov Pechersky (Jul 30 2021 at 20:13):

OK, that makes sense to me. In my day-to-day life, where I have to construct data structures representing subgraph isos (molecular structure mapping), being able to utilize them to map between vertices implicitly improves usability.

#### Kyle Miller (Jul 30 2021 at 20:22):

Barrie Cooper said:

I use the term "embedding"

For simple graphs, apparently when people talk about embeddings they mean the image is an induced subgraph, which surprised me. (The notion that corresponds to the map on the graphs as topological spaces being an embedding is an injective homomorphism.) It's like a discrete version of the difference between injective smooth maps and embedded submanifolds.

I'm not sure how this embedding terminology correctly generalizes to multigraphs. I'd hazard a guess that it would be something such that, for each pair of vertices v and w, f.edge induces a bijection between the edges with endpoints v and w and the edges with endpoints f.vert v and f.vert w.

#### Kyle Miller (Jul 30 2021 at 20:25):

Then a function that's injective on both vertices and edges would be a monic morphism, I think.

This seems pedagogically complicated...

#### Barrie Cooper (Jul 30 2021 at 23:57):

@Kyle Miller : Indeed ... these are precisely the sort of things I ask my students to play with to demonstrate they understand what's going on.

Why do you say "pedagogically complicated"? Just curious ... it's the way it all seems to make sense to me, but perhaps my approach is somewhat idiosyncratic ... which can certainly have its advantages, especially during the last 15 months of open book online exams ...

#### Kyle Miller (Jul 30 2021 at 23:59):

@Barrie Cooper I didn't mean about what you're doing! I was only referring to dealing with both monic morphisms and embeddings. (In particular, introducing category theory concepts at the same time as everything else.)

#### Barrie Cooper (Aug 10 2021 at 11:27):

Suppose I want to have my students play with concrete examples of graphs and morphisms. How do I go about building such objects? For example, I've tried and struggled to build an A2.

Recall my definition of a graph:

```
structure graph :=
(vertices : Type)
(edges : Type)
(endpoints : edges → sym2 vertices)
```

(and I can change `Type`

to anything e.g. `Type*`

if necessary). What I've tried is to get hold of 3 distinct constants and define my endpoint map. I've tried variations on the following and the below is the closest I've got ...

```
constants a b c : ℕ
axiom ab : a ≠ b
axiom ac : a ≠ c
axiom bc : b ≠ c
def E₂ : set ℕ := { a }
def V₂ : set ℕ := {b, c}
def ε₂ : E₂ → sym2 V₂
| a := ⟦(b,c)⟧
```

Lean complains that `b`

and `c`

have the wrong type (ℕ rather than V₂), which I understand but I'm not sure how to 'fix' it. How do I do this properly (either by fixing my code, or via an alternative approach)?

#### Yaël Dillies (Aug 10 2021 at 11:46):

Functions in Lean are total. So you must provide a value for all inputs to `ε₂`

. Yes, you indeed do because `E₂ := {a}`

, but it's non-obvious to Lean that you've provided all cases.

#### Yaël Dillies (Aug 10 2021 at 11:48):

In that particular case, you can define `ε₂`

as `λ _, ⟦(b,c)⟧`

, the constant function whose value everywhere is `⟦(b,c)⟧`

.

#### Barrie Cooper (Aug 10 2021 at 11:50):

Thanks ... that doesn't seem to fix the issue with the Type for b though. (At least, I changed the a to _ in the function definition and Lean is still giving the same Type warning.)

#### Yaël Dillies (Aug 10 2021 at 11:51):

Better practice would be to not define `E₂`

and `V₂`

*at all* and instead use directly the correctly sized types for `vertices`

and `edges`

. So here I would do (untested)

```
def A₂ : graph :=
{ vertices := fin 2,
edges : fin 1,
endpoints := λ _, ⟦(0, 1)⟧ }
```

#### Yaël Dillies (Aug 10 2021 at 11:52):

Or maybe, to avoid complications using `fin`

,

```
def A₂ : graph :=
{ vertices := ℕ,
edges : unit,
endpoints := λ _, ⟦(0, 1)⟧ }
```

#### Barrie Cooper (Aug 10 2021 at 11:52):

Ok ... I'll try that, but typical exercises might be to use different labels for vertices and edges and get students to explicitly write down isomorphisms and morphisms between different concrete examples of graphs.

#### Yaël Dillies (Aug 10 2021 at 11:53):

Yeah, that's hard.

#### Barrie Cooper (Aug 10 2021 at 11:54):

Maybe I'm not the anticipated end user, but it feels to me that this is the stuff that Lean needs to be able to do if we're really going to be able to do all of undergraduate maths in it?

#### Yaël Dillies (Aug 10 2021 at 11:55):

Case-by-case analysis of concrete structures is tedious. For example, try simply proving that `x ∈ {a, b, c, d} ↔ x = a ∨ x = b ∨ x = c ∨ x = d`

.

#### Yaël Dillies (Aug 10 2021 at 11:56):

I don't think there's really any anticipated end user :wink: but one definitely must overcome a few difficulties to do stuff the mathlib way.

#### Barrie Cooper (Aug 10 2021 at 11:58):

I don't mind tedium if it's fairly easy to code ... it's tedious checking that concrete examples of morphisms satisfy the compatability condition by hand, but it's good to get students to do it.

And I thought that the way functions are defined means it should be simple (naively) to check all cases because you just work through the cases listed in the function definition?

#### Yaël Dillies (Aug 10 2021 at 11:59):

Yes, but there's a huge difference between exhausting a type and exhausting a set.

#### Barrie Cooper (Aug 10 2021 at 11:59):

I can make things sets if necessary ... I'm certainly not familiar enough with all the differences ...

#### Yaël Dillies (Aug 10 2021 at 12:00):

Nono, I mean it the other way around.

#### Yaël Dillies (Aug 10 2021 at 12:00):

You defined your `vertices`

and `edges`

as sets (coerced to `Type`

). Lean has no clue how to exhaust those.

#### Yaël Dillies (Aug 10 2021 at 12:01):

Compare that with `ℕ`

where the two constructors are explicit from the inductive definition of `ℕ`

.

#### Barrie Cooper (Aug 10 2021 at 12:01):

Oh ok ... is there a way to avoid them being sets then? Sorry ... really not sure what is the right/wrong way of doing these things.

#### Yaël Dillies (Aug 10 2021 at 12:01):

What are the graphs you're after?

#### Yaël Dillies (Aug 10 2021 at 12:02):

And do you really need to label the edges?

#### Yaël Dillies (Aug 10 2021 at 12:03):

If not, you can spare a huge amount of work by ripping of the labels and defining `edges : set (sym2 V)`

.

#### Yaël Dillies (Aug 10 2021 at 12:04):

Then showing a graph isomorphism won't require you mapping explicitly the edges, which would have sounded a bit troublesome.

#### Barrie Cooper (Aug 10 2021 at 12:05):

But for (multi)graphs that's the point ... the vertex map doesn't determine the edge map.

#### Yaël Dillies (Aug 10 2021 at 12:06):

So you're multigraphs? That's much harder indeed!

#### Barrie Cooper (Aug 10 2021 at 12:07):

Indeed.

#### Barrie Cooper (Aug 10 2021 at 12:09):

I want my students to be able to make concrete examples of isomorphisms between different instances of say A4, D4, C4 and K4 and morphisms between these, or prove that morphisms don't exist.

From the point of view of general theory, it would also be nice to be able to prove that embeddings (vertex and edge maps injective) don't necessarily have left inverses e.g. by constructing counterexamples.

#### Yaël Dillies (Aug 10 2021 at 12:12):

One way to do it would then be to define the ground types inductively. For example,

```
inductive vert4 : Type
| a := vert4
| b := vert4
| c := vert4
| d := vert4
```

#### Barrie Cooper (Aug 10 2021 at 12:13):

Ah ... that seems like a nice approach :)

#### Yaël Dillies (Aug 10 2021 at 12:13):

For the edges, I don't really know. What's A4 already?

#### Barrie Cooper (Aug 10 2021 at 12:14):

4 vertices and 3 edges joined in a line.

#### Barrie Cooper (Aug 10 2021 at 12:14):

Sometimes called a path graph on 4 vertices.

#### Yaël Dillies (Aug 10 2021 at 12:15):

Ah yeah. And C4?

#### Barrie Cooper (Aug 10 2021 at 12:18):

Cycle graph on 4 vertices.

#### Barrie Cooper (Aug 10 2021 at 12:20):

I don't seem to be getting the `inductive`

type definition right. When I enter what you put, the first `:=`

gets underlined with the message `command expected`

.

#### Yaël Dillies (Aug 10 2021 at 12:21):

Actually there would be a neat way to build simple multigraphs by hand. Instead of having global labels, you have labels for each pair of vertices. Indexing them by `ℕ`

should be enough for your purposes.

```
inductive edges (vertices : Type) (f : sym2 vertices -> ℕ) : Type
| of_nat : \for e : sym2 vertices, \for n, n < f e -> vert4
```

#### Yaël Dillies (Aug 10 2021 at 12:22):

the idea being that you set `f ⟦(a, b)⟧`

to be the number of edges you want between `a`

and `b`

.

#### Barrie Cooper (Aug 10 2021 at 12:25):

Thanks - I'll have a play ...

#### Barrie Cooper (Aug 10 2021 at 12:36):

Based on your first approach @Yaël Dillies, I now seem to have an example that works ... many thanks!

```
inductive vert : Type
| I : vert
| II : vert
| III : vert
| IV : vert
inductive edge : Type
| a : edge
| b : edge
| c : edge
def ε₄ : edge → sym2 vert
| edge.a := ⟦(vert.I,vert.II)⟧
| edge.b := ⟦(vert.II,vert.III)⟧
| edge.c := ⟦(vert.III,vert.IV)⟧
def A₄ := graph.mk (vert) (edge) (ε₄)
```

#### Eric Rodriguez (Aug 10 2021 at 12:36):

Yaël Dillies said:

Case-by-case analysis of concrete structures is tedious. For example, try simply proving that

`x ∈ {a, b, c, d} ↔ x = a ∨ x = b ∨ x = c ∨ x = d`

.

particularly bad example, it turns out:

`example : x ∈ ({a, b, c, d} : set α) ↔ x = a ∨ x = b ∨ x = c ∨ x = d := iff.rfl`

(surprised me too!)

#### Yaël Dillies (Aug 10 2021 at 12:37):

Oh hmm... I had something similar which turned out to be a real pain.

#### Yaël Dillies (Aug 10 2021 at 12:37):

And great Barrie!

#### Yaël Dillies (Aug 10 2021 at 12:38):

Though note that this approach hardly scales. Hope you're not lurking on infinite graphs :stuck_out_tongue:

#### Yakov Pechersky (Aug 10 2021 at 12:46):

I think the solution here is using fintypes

#### Barrie Cooper (Aug 10 2021 at 12:46):

I'll settle for finite graphs for now, but it would be good to be able to do something similar for infinite graphs. I like to give my students the example of edges = ℝ, vertices = ℤ, and the floor and ceiling functions as the endpoint map. Sounds fun to try to get that working ...

#### Yakov Pechersky (Aug 10 2021 at 12:46):

One can do @[derive fintype] on those inductive types

#### Yakov Pechersky (Aug 10 2021 at 12:50):

And you could say

variables {V : Type} [fintype V] (a b c : V) (h : (finset.univ : finset V) = {a, b, c}) (h' : fintype.card = 3)

#### Yakov Pechersky (Aug 10 2021 at 12:52):

You'll probably want to do @[derive decidable_eq] on your inductive types too. That'll let you do case bash by "dec_trivial"

#### Yaël Dillies (Aug 10 2021 at 12:59):

Yakov Pechersky said:

And you could say

variables {V : Type} [fintype V] (a b c : V) (h : (finset.univ : finset V) = {a, b, c}) (h' : fintype.card = 3)

But then you fall into the very problem I was trying to get out of: How do you define a map from `V`

?

#### Yaël Dillies (Aug 10 2021 at 16:08):

Barrie Cooper said:

I'll settle for finite graphs for now, but it would be good to be able to do something similar for infinite graphs. I like to give my students the example of edges = ℝ, vertices = ℤ, and the floor and ceiling functions as the endpoint map. Sounds fun to try to get that working ...

Actually this one is easy

```
def floor_ceil_graph := graph.mk ℤ ℝ (λ x, ⟦(floor x, ceil x)⟧)
```

#### Kyle Miller (Aug 10 2021 at 16:45):

@Barrie Cooper To save some typing tedium, when an inductive type is just an enumeration you don't need to specify the types of the constructors. Also, you might like `{graph. vertices := ..., edges := ..., endpoints := ...}`

notation.

```
import data.sym2
structure graph :=
(vertices : Type)
(edges : Type)
(endpoints : edges → sym2 vertices)
inductive vert
| I | II | III | IV
inductive edge
| a | b | c
def ε₄ : edge → sym2 vert
| edge.a := ⟦(vert.I,vert.II)⟧
| edge.b := ⟦(vert.II,vert.III)⟧
| edge.c := ⟦(vert.III,vert.IV)⟧
def A₄ :=
{ graph.
vertices := vert,
edges := edge,
endpoints := ε₄ }
def A₄' := graph.mk vert edge ε₄
def A₄'' : graph :=
{ vertices := vert,
edges := edge,
endpoints := ε₄ }
```

#### Kyle Miller (Aug 10 2021 at 17:01):

Developing @Yaël Dillies's idea, here's a way to create a multigraph using a specified number of edges between pairs of vertices:

```
structure inc_edges {V : Type} (f : sym2 V → ℕ) :=
(e : sym2 V)
(i : fin (f e))
def graph.of_inc (V : Type) (f : sym2 V → ℕ) : graph :=
{ vertices := V,
edges := inc_edges f,
endpoints := inc_edges.e }
-- path with n edges
def path (n : ℕ) := graph.of_inc (fin (n + 1))
(sym2.lift ⟨(λ (v w : fin (n + 1)),
if v + 1 = w ∨ w + 1 = v then 1 else 0),
by simp [or_comm]⟩)
```

#### Kyle Miller (Aug 10 2021 at 17:02):

(`sym2.lift`

is a nice new function for defining functions whose domain is `sym2`

)

#### Kyle Miller (Aug 10 2021 at 17:12):

Another way to construct graphs, from a list of edges. The second element in each pair is an edge label that you can use to distinguish edges (here I just used `unit`

since I didn't need to distinguish edges).

```
def graph.of_edge_spec (V : Type) (α : Type) (edges : list (sym2 V × α)) : graph :=
{ vertices := V,
edges := {s | s ∈ edges},
endpoints := λ e, prod.fst (e : sym2 V × α) }
inductive vert
| I | II | III | IV
def A₄ := graph.of_edge_spec vert unit
[(⟦(vert.I, vert.II)⟧, ()),
(⟦(vert.II, vert.III)⟧, ()),
(⟦(vert.III, vert.IV)⟧, ())]
```

#### Kyle Miller (Aug 10 2021 at 17:19):

Or, by instead using duplicates in a list to indicate multiple edges:

```
def graph.of_list (V : Type) (edges : list (sym2 V)) : graph :=
{ vertices := V,
edges := {p : ℕ × sym2 V | p ∈ edges.map_with_index prod.mk},
endpoints := λ e, prod.snd (e : ℕ × sym2 V) }
inductive vert
| I | II | III | IV
def A₄ := graph.of_list vert
[⟦(vert.I, vert.II)⟧,
⟦(vert.II, vert.III)⟧,
⟦(vert.III, vert.IV)⟧]
def konigsberg := graph.of_list (fin 4)
[⟦(0, 1)⟧,
⟦(0, 2)⟧,
⟦(0, 3)⟧,
⟦(1, 2)⟧, ⟦(1, 2)⟧,
⟦(2, 3)⟧, ⟦(2, 3)⟧]
```

#### Barrie Cooper (Aug 10 2021 at 17:42):

Thanks :) Incidentally, what's the proof that these vertices/edges are distinct? For example, that `vert.I ≠ vert.II`

. I'm guessing I might need those facts when proving that morphisms are embeddings etc.

#### Kyle Miller (Aug 10 2021 at 17:49):

Here's one way to write a tactic proof:

```
example : vert.I ≠ vert.II :=
begin
intro h,
injection h,
end
```

#### Kyle Miller (Aug 10 2021 at 17:50):

(or digging into the weeds, a term-mode proof: `example : vert.I ≠ vert.II := λ h, vert.no_confusion h`

)

#### Kyle Miller (Aug 10 2021 at 17:55):

I didn't know this would work:

```
example : vert.I ≠ vert.II := by trivial
```

#### Kyle Miller (Aug 10 2021 at 17:56):

`trivial`

seems to be doing this:

```
def foo : vert.I ≠ vert.II := by contradiction
```

#### Kyle Miller (Aug 10 2021 at 17:57):

#### Eric Rodriguez (Aug 10 2021 at 17:59):

not even that, `def foo : vert.I ≠ vert.II.`

works

#### Eric Rodriguez (Aug 10 2021 at 17:59):

it's equation compiler magic iirc

#### Kyle Miller (Aug 10 2021 at 18:01):

That's not so useful in the middle of a proof, but it's always worth pointing out the power of the equation compiler.

#### Kyle Miller (Aug 10 2021 at 18:02):

One more option:

```
@[derive decidable_eq]
inductive vert
| I | II | III | IV
example : vert.I ≠ vert.II := dec_trivial
```

(If I understand how it works correctly, `derive decidable_eq`

effectively defines a function `vert -> vert -> bool`

that implements the equality check, and then `dec_trivial`

evaluates it, making sure the value is false. This isn't exactly how it works, because rather than `bool`

it's using `decidable`

, which more naturally connects the truth value with the `Prop`

.)

#### Barrie Cooper (Aug 10 2021 at 19:27):

Thanks - I knew it would be something simple.

#### Barrie Cooper (Aug 30 2021 at 07:59):

So I'm now happy defining specific examples of (multi)graphs and morphisms, but I'm not sure of the syntax to do this *within* a proof. For example, if I want to prove that there exists a morphism `A₂ → C₃`

, I can set everything up in advance e.g.

```
def φ₁ : A₂.vertices → C₃.vertices
| vert₂.I := vert₃.I
| vert₂.II := vert₃.II
def ψ₁ : A₂.edges → C₃.edges
| edge₁.a := edge₃.a
theorem comp₁ : C₃.endpoints ∘ ψ₁ = sym2.map φ₁ ∘ A₂.endpoints :=
begin
apply funext,
intro x,
cases x,
refl,
end
def α₁ := morphism.mk (φ₁) (ψ₁) (comp₁)
example : nonempty (A₂ ↦ C₃) :=
begin
use α₁,
end
```

How can I do this 'on-the-fly' within the proof itself? I've tried various combinations of things like `let`

, but with no success ...

(Heads up: I'll probably be back when I try to prove that there are no morphisms in the other direction.)

#### Kevin Buzzard (Aug 30 2021 at 08:08):

You can do everything the equation compiler can do using recursors. Type `#print phi-whatever-the-next-character-is`

(I'm on mobile and it's not displaying properly) to see how the equation compiler turned your definition into a lean term.

#### Kevin Buzzard (Aug 30 2021 at 08:09):

It will have used a function called something.rec at the end of the day. But actually I think your approach of defining them outside is much more readable. You correctly observe that you can't use the equation compiler in the middle of a proof in lean 3 (maybe you can with `match`

? Not sure). Maybe lean 4 is better in this regard?

#### Barrie Cooper (Aug 30 2021 at 08:13):

Thanks - yes, the result using `#print`

and drilling down isn't very readable. I'd like to set `nonempty (A₂ ↦ C₃)`

as a proof to be completed in a lean game, say, so students would need to be able to define their own morphism on-the-fly within the proof (in an easy-to-read way).

#### Mario Carneiro (Aug 30 2021 at 08:13):

match should work for that

#### Barrie Cooper (Aug 30 2021 at 08:14):

I'd also rather that the definitions are local to the proof so I don't have to think up new names all the time (or clear the names I've used already so I can redefine them).

#### Barrie Cooper (Aug 30 2021 at 09:27):

Thanks Kevin, Mario - I think I've got it.

```
example : nonempty (A₂ ↦ C₃) :=
begin
let φ₁ : A₂.vertices → C₃.vertices := λ v,
match v with
| vert₂.I := vert₃.I
| vert₂.II := vert₃.II
end,
let ψ₁ : A₂.edges → C₃.edges := λ e,
match e with
| edge₁.a := edge₃.a
end,
let α₁ := morphism.mk (φ₁) (ψ₁) _,
use α₁,
apply funext,
intro x,
cases x,
refl,
end
```

Is there a way to simplify those function definitions for `φ₁`

and `ψ₁`

or is this as close as it gets to my original `def`

versions?

#### Mario Carneiro (Aug 30 2021 at 09:38):

you can also inline them into `α₁`

#### Mario Carneiro (Aug 30 2021 at 09:39):

you can also prove the proof part using a `match`

if you want to

#### Mario Carneiro (Aug 30 2021 at 09:41):

If I were writing this in a golfing mood I would do something like

```
example : nonempty (A₂ ↦ C₃) :=
⟨λ v, match v with
| vert₂.I := vert₃.I
| vert₂.II := vert₃.II
end,
λ e, match e with
| edge₁.a := edge₃.a
end,
funext $ λ x, by cases x; refl⟩
```

#### Mario Carneiro (Aug 30 2021 at 09:41):

or

```
example : nonempty (A₂ ↦ C₃) :=
⟨λ v, vert₂.rec_on v vert₃.I vert₃.II, λ _, edge₃.a, funext $ λ x, by cases x; refl⟩
```

#### Mario Carneiro (Aug 30 2021 at 09:42):

(note - untested)

#### Peter Nelson (May 26 2022 at 01:31):

After quite some time away, I've decided (along with @Alena Gusakov ) to restart thinking about lean with a new approach to multigraphs, which is now in the `graph2`

branch, all under `combinatorics.graph`

.

As a researcher in graph/matroid theory, I think it's quite important that the edges of a multigraph not be anonymous, instead being decoupled from the vertices as their own type. This will be important when defining minors, as well as things like surface embeddings, not to mention graphic matroids.

When proving theorems in the wild, defining a graph as a set of vertex pairs is great for areas like colouring and induced subgraph theory, but when working with the minor order (and to an extent, the subgraph order), the edges having their own 'names' is often quite important for things to be clean.

Anyway, the approach first defines a `digraph`

as follows (so each edge `e`

has a head `G.ends 0 e`

and a tail `G.ends 1 e`

):

```
structure digraph (V E : Type*) :=
(ends : fin 2 → E → V)
```

then (after a bunch of lemmas), defines an equivalence relation stating when two digraphs are the same up to reorienting edges

```
def orientation_equiv (G G' : digraph V E) : Prop :=
∀ (e : E), ∃ (φ : fin 2 ≃ fin 2), ∀ (i : fin 2), G.ends i e = G'.ends (φ i) e
```

and defines `graph`

as a quotient of `digraph`

by this relation. The code gets as far as proving the handshake theorem (first in the directed setting and, via the quotient, in the undirected setting) without anything too horrible. Indeed, handshaking motivated this digraph/quotient approach - it seems like one of the only ways to prove things like the handshake theorem without making ugly special cases for loops, which should contribute degree 2 to their end.

Another thing to note is that `deg`

is defined noncomputably via `nat.card`

to avoid the definition containing data.

This is my first time writing anything involving `quot`

and I'm currently trying to figure out how to make it work nicely with typeclasses (for instance, what is the right way to transfer the `locally_finite`

typeclass from `digraph`

to `graph`

?) I'd be interested to hear any comments on this.

#### Kyle Miller (May 26 2022 at 03:14):

(Direct link to the folder: https://github.com/leanprover-community/mathlib/tree/graphs2/src/combinatorics/graph)

That seems like a reasonable way to encode darts and to make it so that loop edges inherently get two. I like that these satisfy the degree-sum formula.

Regarding `locally_finite`

, I don't think you want that to be a typeclass but rather an abbreviation (or a `reducible`

def). Take a look at docs#simple_graph.locally_finite. To get this to work for multiple types of graphs, you'd want something like this set up:

```
class has_nhd (α : Type*) (V : out_param $ Type*) :=
(nhd : α → V → Type*)
def deg {α : Type*} (G : α) {V : Type*} [has_nhd α V] (v : V) : ℕ :=
nat.card (has_nhd.nhd G v)
```

I've been trying to see what kind of feature we could have in Lean 3 that would be supported in Lean 4 that would allow us to still write `G.deg v`

with dot notation. Maybe writing abbreviations should be enough for now.

I'll have more comments later.

#### Junyan Xu (Jun 23 2022 at 13:45):

Is `fin 2`

easier to use than `bool`

?

And is there any problem with using `E → V × V`

?

#### Yaël Dillies (Jun 23 2022 at 14:42):

Or, better, `src tgt : E → V`

.

#### Yaël Dillies (Jun 23 2022 at 14:43):

You can even `extends (E → V) × (E → V)`

to access `prod.swap`

(which corresponds to reversing the arrows).

#### Yaël Dillies (Aug 17 2022 at 15:26):

Heads up everyone that @Antoine Labelle and I just PRed a definition of `multigraph`

in #16100. This is very similar to @Peter Nelson's approach here and works very well to define the Laplacian and Picard group as you can witness on branch#graph_riemann_roch.

#### Yaël Dillies (Aug 17 2022 at 15:26):

The goal is to give the graph theoretic Riemann-Roch as a project to undergraduates at @Kevin Buzzard's workshop at the end of September.

#### Yaël Dillies (Aug 17 2022 at 15:31):

The main difference with Peter and Alena's definition is that we bundle the types of vertices and edges in the structure, rather than taking them as parameters. The reason being that there's no interesting structure to describe on multigraphs with vertices `V`

and edges `E`

and that this allows us to reuse the type of multigraphs as the category of multigraphs, with the hope of reducing boilerplate by using category theoretic machinery.

#### Yaël Dillies (Aug 17 2022 at 15:33):

I would be happy to rename our new definition to `indexed_multigraph`

to contrast with @Kyle Miller's definition in branch#multigraphs, which more resembles docs#quiver.

#### Kyle Miller (Aug 17 2022 at 15:36):

Where are you getting the "indexed multigraph" terminology? As far as I know, this is a multigraph (except for the fact that it allows half loops, which I'm not so sure about -- we should either disallow them or require one at every vertex)

#### Kyle Miller (Aug 17 2022 at 15:41):

I also think it would be good having `V`

be exposed as a parameter, since it's worth thinking about different multigraph structures on the same vertex type. Not having `E`

be exposed makes sense to me (there are some alternatives, but it's fine the way it is).

#### Bhavik Mehta (Aug 17 2022 at 16:16):

Peter gives some reasons why it's useful to have an exposed type of vertices and edges above - it seems like this definition can struggle to do the things he mentions?

#### Kyle Miller (Aug 17 2022 at 16:24):

@Bhavik Mehta I believe Peter is talking about making sure the edges have individual identities, rather than necessarily exposing an edge type. In a previous version, Peter was considering multigraphs where there was a mere count of the number of edges between pairs of vertices.

#### Bhavik Mehta (Aug 17 2022 at 16:39):

Ah I missed that context, thanks

#### Bhavik Mehta (Aug 17 2022 at 16:51):

Kyle Miller said:

Where are you getting the "indexed multigraph" terminology? As far as I know, this is a multigraph (except for the fact that it allows half loops, which I'm not so sure about -- we should either disallow them or require one at every vertex)

About the half loops point - I think it wouldn't be too hard to extend this structure to disallow them or require them all, so it seems like this version generalises both in a relatively clean way?

#### Antoine Labelle (Aug 17 2022 at 17:02):

Yes, we can just have a typeclass `no_half_loops`

that we put on a graph if we want to exclude them, right?

#### Kyle Miller (Aug 17 2022 at 17:09):

I wouldn't use the word "just" there, but that's a possible solution. An issue is that when you're manipulating multigraphs you likely will need to help Lean with typeclass inference.

#### Kyle Miller (Aug 17 2022 at 17:11):

One reason I'm not too keen on having the vertex and edge types be contained in the structure is that suggests we should never use `=`

between multigraphs... Maybe this is ok, especially if it turns out it is sufficient working with subgraphs of a big enough multigraph.

#### Antoine Labelle (Aug 17 2022 at 17:53):

To be able to use `=`

we would need both the vertex and the edge type out of the structure, right?

#### Kyle Miller (Aug 17 2022 at 17:54):

Yes, but also making `E`

be a parameter doesn't make much sense for this definition.

#### Kyle Miller (Aug 17 2022 at 17:58):

I had to take some time to remember what was going on with branch#multigraphs. It's a generalization to Chou's multigraph definition (see the reference at multigraph/basic.lean)

It might look like it's paralleling the quiver definition, but the `labels`

field has type `V → V → set α`

so that the `symm`

axiom can be stated in a clean way. That type is equivalent to `set (V × α × V)`

, which is the set of "links," using Chou's terminology. Having `α`

be exposed gives you a good amount of flexibility, and this `multigraph`

type enjoys extensional equality as well as a lattice structure.

#### Kyle Miller (Aug 17 2022 at 18:00):

This version of a multigraph is a generalization of simple graphs in the sense that we could define `def simple_graph (V : Type u) := {G : multigraph V unit // G.loopless}`

#### Kyle Miller (Aug 17 2022 at 18:08):

Admittedly this multigraph definition is not completely compatible with the one in #16100.

Here's a design question: for #16100, what would be the type for the edges of a multigraph?

#### Antoine Labelle (Aug 17 2022 at 19:35):

I'm not sure I understand the question. The type for the edges in #16100 is `multigraph.E`

.

#### Kyle Miller (Aug 17 2022 at 20:07):

Wouldn't a graph with two vertices and a single edge between them have an `E`

type with two terms?

#### Antoine Labelle (Aug 17 2022 at 20:12):

Oh yeah sorry, `multigraph.E`

is the type of oriented edges. The set of unoriented edges would be the quotient of that by the `inv`

involution.

#### Antoine Labelle (Aug 17 2022 at 20:14):

(At least in the case of no half-loops, I'm not sure what you would consider as an unoriented edge when there are half-loops).

#### Peter Nelson (Aug 18 2022 at 19:29):

Nice job, @Yaël Dillies !

I'm not sure I like the edge and vertex types being bundled, though. For instance, if G is a multigraph on edge set E, and G' is obtained from G by identifying vertices, then G' has edge set E, and one can show that the cycle space of G' is a subspace of the cycle space of G (the cycle space of a graph H on edge set E is the subspace of F_2^E spanned by the indicator vectors of cycles of H). This fact would be awkward to state without type equality if the type is bundled.

I think there will be many issues of this sort when using the edges/vertices to do things like index rows/columns of matrices or the elements of a matroid; bundling will make it harder to talk about the relationship between different graphs that have vertex/edge sets in common.

#### Peter Nelson (Aug 18 2022 at 19:33):

This is probably more of an issue for bundled vertices than for bundled edges, by the way.

#### Yaël Dillies (Aug 18 2022 at 19:49):

From my understanding, the only difference between having a given argument `foo`

as a parameter or as a field to some structure `bar`

is when the `bar`

with fixed `foo`

form a structure (like a `lattice`

or a `group`

).

But here `multigraph V E`

(having both parameters) certainly isn't a `lattice`

or a `group`

(what structure would you expect from the type of graphs with a fixed number of vertices and edges?), and `multigraph V`

(having `V`

a parameter and `E`

a field) certainly isn't either because `E : Type*`

as a field stops you from using equality.

So there is no gain in having `V`

and `E`

out, so we might as well put them in, because that gives us a category, and all the machinery that goes with it.

#### Yaël Dillies (Aug 18 2022 at 19:50):

I suspect what you're missing is the fact that bundling the types doesn't stop them from having defeqs.

#### Yaël Dillies (Aug 18 2022 at 19:52):

Here's how I would translate your example:

```
def identified (G : multigraph) : multigraph :=
{ V := some_quotient_of_G_V
E := G.E }
example : G.identified.E = G.E := rfl -- works
```

so you can still state whatever you were stating before.

#### Yaël Dillies (Aug 18 2022 at 19:54):

One fair concern is that `G.V`

and `G.E`

are not syntactically equal to their definitions, so instances don't go through. Typically, if you have a graph whose vertices are indexed by `ℕ`

, then you might have to fiddle to add or multiply them. But I suspect this is circumventable by carefully stating all lemmas in terms of `ℕ`

rather than `G.V`

.

#### Peter Nelson (Aug 19 2022 at 14:01):

The multigraphs on a fixed edge set E do form a lattice: the homomorphism lattice, where H \le G if (up to renaming vertices), the graph H arises from G by identifying vertices. There are also a number of structures on [matroids on a ground set E], such as the lattices of weak/strong maps, that specialize to [multigraphs on edge set E] via graphic matroids.

#### Yaël Dillies (Aug 19 2022 at 14:07):

The "up to renaming vertices" is precisely what makes them not a lattice. What is a lattice is the quotient of multigraphs on a fixed edge set by equivalence of vertices. My point is that as soon as you put a type as a field, you will need to take a quotient to make equality meaningful. So the only two real options are `multigraph V E`

(which still doesn't seem to form any algebraic structure) and `multigraph`

(which forms a category).

#### Peter Nelson (Aug 19 2022 at 14:09):

What about `multigraph E`

?

#### Yaël Dillies (Aug 19 2022 at 14:10):

There's `V`

as a field, right? So equality is meaningless.

#### Peter Nelson (Aug 19 2022 at 14:14):

If I have `G_1 G_2 : multigraph E`

, they may have defeq vertex sets, or we may have `G_1 \le G_2`

in the homomorphism lattice on `multigraph E`

, or the corresponding `M_1 M_2 : matroid E`

may be related by a weak map, etc etc. Wouldn't this be useful?

#### Yaël Dillies (Aug 19 2022 at 14:15):

Maybe, but you can't prove `lattice (multigraph E)`

which I think you will need for anything remotely non trivial.

#### Peter Nelson (Aug 19 2022 at 14:15):

Why not?

#### Peter Nelson (Aug 19 2022 at 14:15):

Ah right, it's not a partial order.

#### Peter Nelson (Aug 19 2022 at 14:29):

Still, it seems to me like for many purposes the quotient of multigraph by renaming vertices is a more natural structure than multigraph itself; will it be easy to work with this?

#### Kyle Miller (Aug 19 2022 at 15:30):

I'd like to point out again that the multigraph definition in branch#multigraphs forms a lattice, since this seems to have been overlooked.

The way it works is that the alpha type corresponds to edge labels, between any pair of vertices an edge with a given label can appear at most once, and edge labels can otherwise be re-used.

#### Kyle Miller (Aug 19 2022 at 15:37):

The main weakness with that definition is that loops only have a single dart (if you don't treat loops specially), which doesn't seem right to me -- I would think the number of orientations of a graph should double every time you subdivide an edge, but for loops it's a factor of four.

#16100 allows either one or two darts per loop. This is the incompatibility I was meaning to refer to earlier.

#### Antoine Labelle (Aug 19 2022 at 15:49):

Yes I believe usual loops should have two darts and half-loops should have one.

#### Kyle Miller (Nov 24 2022 at 11:06):

Sorry it took awhile to evaluate #16100. I've left a comment about the definition, and I'm leaving a message here so that people interested in multigraphs are aware (ping @Peter Nelson).

This week Floris helped me think through the plethora of multigraph definitions, and the one that has the most promise is one with an exposed vertex type `V`

, containing an edge type `E`

, and having a function `E → sym2 V`

assigning each edge to its incident vertices. We also thought having an extra `sym2 V → set E`

function would be useful for definitional convenience.

```
structure multigraph (V : Type u) :=
(E : Type v)
(edge_verts : E → sym2 V)
-- The following is for definitional convenience
(edges : sym2 V → set E)
(mem_edges_iff : ∀ (z : sym2 V) (e : E), e ∈ edges z ↔ edge_verts e = z)
```

This also has a natural homomorphism definition:

```
structure multigraph.hom {V V' : Type*} (G : multigraph V) (G' : multigraph V') :=
(on_vert : V → V')
(on_edge : G.E → G'.E)
(comm : ∀ (e : G.E), G'.edge_verts (on_edge e) = sym2.map on_vert (G.edge_verts e))
```

and there are good conversions to and from simple graphs:

```
def simple_graph.to_multigraph {V : Type u} (G : simple_graph V) : multigraph V :=
{ E := G.edge_set,
edge_verts := λ e, e,
edges := λ z, {e : G.edge_set | ↑e = z},
mem_edges_iff := λ vs e, iff.rfl }
/-- Create a simple graph by forgetting loop edges and multiple edges. -/
def multigraph.to_simple_graph {V : Type u} (G : multigraph V) : simple_graph V :=
simple_graph.from_edge_set {z | (G.edges z).nonempty}
```

#### Kyle Miller (Nov 24 2022 at 11:07):

There are more thoughts in the comment on #16100.

#### Kyle Miller (Nov 24 2022 at 11:09):

But one thing that I think is important is that our first `multigraph`

definition be one that corresponds to what we commonly mean by a multigraph. This definition is such that `E`

actually is the edge type (instead of a type of darts in the PR), and there's no distinction between loops and half-loops, which I could see being useful in some contexts, but for basic material about multigraphs I think we'd rather not deal with this distinction.

#### Antoine Labelle (Nov 24 2022 at 12:38):

I'm not sure I understand your arguement against half-loops. Do you have an example where allowing half-loops would make things more complicated? My impression is that in practice you don't have to think too much about them, most definitions work basically the same way with or without half-loops, so we might as well have them allowed (since I'd say we definitely want them as soon as we're talking about quotient graphs).

#### Antoine Labelle (Nov 24 2022 at 12:44):

Also in my experience it's not that uncommon to say (oriented) edges to mean what you call darts, but that's probably very much a subfield-dependant thing. Anyway, in any case that's not really a fundamental problem of #16100, the field `E`

there could always be renamed `darts`

.

#### Kyle Miller (Nov 24 2022 at 12:48):

My main argument against half-loops (at least for the main `multigraph`

definition) is that multigraphs as they appear in the literature to not have them.

Regarding using darts in the definition of a multigraph, it seems more straightforward to define a multigraph to be `E -> sym2 V`

. For example, an edge labeling is then any function `E -> L`

rather than a function `D -> L`

that is invariant under the dart involution.

#### Antoine Labelle (Nov 24 2022 at 12:49):

For the record, I'm currently trying to do some multigraph stuff with @Rémi Bottinelli using quivers directly (there a few open PR about that currently). I think that can work, the biggest issue with that is dependant type hell due to edge types depending on vertices, but it's manageable using `cast`

.

#### Kyle Miller (Nov 24 2022 at 12:53):

The `E -> sym2 V`

definition is the one that's obviously multigraphs, and I think the burden of proof is not on whether `E -> sym2 V`

would be more or less complicated, but on the question of whether this alternative definition that diverges from the literature will always work out fine for standard stuff about multigraphs. I think it's easier and safer to go with `E -> sym2 V`

.

#### Kyle Miller (Nov 24 2022 at 12:54):

Regarding quotients, I imagine you're talking about, for example, the case where you have a single-vertex graph with a self loop and you have Z/2Z acting on it by reflection, then you want to take the quotient. In geometric group theory I've seen this handled where you first subdivide each edge into two edges.

#### Kyle Miller (Nov 24 2022 at 12:55):

It's not clear to me that it's worth ensuring there is always a quotient that coincides with the quotient of the topological realization if that means using a definition that's different from the usual one.

#### Kyle Miller (Nov 24 2022 at 12:57):

Antoine Labelle said:

For the record, I'm currently trying to do some multigraph stuff with Rémi Bottinelli using quivers directly (there a few open PR about that currently). I think that can work, the biggest issue with that is dependant type hell due to edge types depending on vertices, but it's manageable using

`cast`

.

Thanks for going on this expedition into dependent type hell! :smile:

#### Antoine Labelle (Nov 24 2022 at 13:02):

For example, an edge labeling is then any function

`E -> L`

rather than a function`D -> L`

that is invariant under the dart involution.

But when talking about stuff like the graph laplacian, you need the vector space of function on D such that `f (inv e)=-f e`

! You can't do that with unoriented edges without choosing an arbitrary orientation and then showing that everything you define is independant of that choice of orientation, which is quite annoying.

#### Antoine Labelle (Nov 24 2022 at 13:13):

I'm not convinced about `E -> sym2 V`

being "the standard definition in the litterature", personally I must have seen at least 10 different definitions of multigraphs by different people, so I don't feel like any of them is particularly standard.

#### Kyle Miller (Nov 24 2022 at 13:14):

There's no need for arbitrary orientations. For example, here's one possible way to define a type of darts where every edge has two darts:

```
inductive multigraph.D {V : Type u} (G : multigraph V)
| dart {u v : V} (f : u = v → bool) (e : G.edges ⟦(u, v)⟧) : multigraph.D
```

The `f`

is a hack to get a type of size `2`

or `1`

depending on whether it's a loop or not.

#### Antoine Labelle (Nov 24 2022 at 13:15):

Definitely depends on the field at least, maybe your definition in standard in extremal combinatorics but I wouldn't say so in geometric group theory.

#### Kyle Miller (Nov 24 2022 at 13:16):

Antoine Labelle said:

personally I must have seen at least 10 different definitions of multigraphs by different people

Yes, the plethora of definitions is what's been a stumbling block for defining multigraphs. While `E -> sym2 V`

is not *literally* standard, I think it captures what we mean by multigraphs in combinatorics. Of those 10 different definitions, did any admit half-loops?

#### Antoine Labelle (Nov 24 2022 at 13:18):

Yes I've seen definitions allowing normal loops and half-loops, allowing only normal loops or even allowing only half-loops :smile:

#### Kyle Miller (Nov 24 2022 at 13:18):

Geometric group theory cares more about the geometric realization of a multigraph I'd say, but the subdivision trick like the one I mentioned helps smooth over the difference. (Subdividing every edge yields a quasi-isometric graph, right?)

#### Antoine Labelle (Nov 24 2022 at 13:19):

Sure but the subdivision trick feels very hacky and definitely introduces some extra bookkeeping to work with the subdivided graph.

#### Antoine Labelle (Nov 24 2022 at 13:21):

Another important advantage of the dart-based definition in my opinion is that it can extend unoriented graphs, so it prevents a lot of code duplication between oriented and nonoriented graphs.

#### Rémi Bottinelli (Nov 24 2022 at 13:23):

Maybe graphs are too ubiquitous/basic for there to be one best definition covering everything, and we should accept to have a few different ones.

#### Kyle Miller (Nov 24 2022 at 13:24):

Right, I said "first definition of multigraph" earlier very intentionally with this in mind

#### Rémi Bottinelli (Nov 24 2022 at 13:25):

In this optic, assuming the quiver-based approach is meant to be kept in the near/middle term, it might also be reasonable to have your proposed approach "as far away" as possible from it. I'm not sure I'm making much sense, but I mean that "we" might as well cover as much ground between the two implementations as possible.

#### Kyle Miller (Nov 24 2022 at 13:38):

For what it's worth, the wikipedia definition of an unoriented multigraph is a triple `(V, E, E -> sym2 V)`

. The only variation in the handful of sources I rechecked this against were whether loops were allowed at all.

(By the way, I was considering being so bold as to just call the type `graph`

, but I'd rather not conflict with for example `function.graph`

if someone does `open function`

.)

#### Kyle Miller (Nov 24 2022 at 13:39):

I've only seen half-loops before in very non-combinatorics settings. One was an explanation of using presheafs to represent graph structures, and I think I also saw it on ncatlab

#### Kyle Miller (Nov 24 2022 at 13:41):

I like ncatlab, but I think it goes without saying that it has a particular point of view

#### Antoine Labelle (Nov 24 2022 at 13:44):

I've seen half-loops mostly when doing spectral graph theory, and I admit it was in somewhat number-theory/algebra oriented litterature.

#### Kyle Miller (Nov 24 2022 at 13:47):

Just to check, you mean half-loops (and not just half-edges/darts) were in spectral graph theory literature?

#### Antoine Labelle (Nov 24 2022 at 13:47):

Yes

#### Antoine Labelle (Nov 24 2022 at 13:48):

(For darts but no half-loops, I'd say it's also standard in Bass-Serre theory).

#### Kyle Miller (Nov 24 2022 at 13:51):

Maybe we have to admit that multigraphs and 1D cell complexes are just different things, and we normally confuse them because they have the same pictures.

#### Antoine Labelle (Nov 24 2022 at 14:02):

Maybe :shrug:

#### Yaël Dillies (Nov 24 2022 at 14:11):

That would remind me of abstract simplicial complexes and lower sets.

#### Antoine Labelle (Nov 24 2022 at 14:19):

1D simplicial complexes are just simple graphs, no? Multigraphs are more like delta complexes (I don't think delta complexes allow half-loops, though I think I've seen a variant that allows them at some point).

#### Kyle Miller (Nov 24 2022 at 14:20):

I said "cell complex" not "simplicial complex," but yes, delta complexes or CW complexes

#### Kyle Miller (Nov 24 2022 at 14:20):

delta complexes don't allow half-loops, at least in the version I learned in Hatcher's book

#### Antoine Labelle (Nov 24 2022 at 14:22):

I said "cell complex" not "simplicial complex," but yes, delta complexes or CW complexes

Yes, I was just answering to Yaël.

Last updated: Dec 20 2023 at 11:08 UTC