multigraph definition

Stream: graph theory

[Kyle Miller]

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]

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]

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]

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

[Peter Nelson]

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]

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]

(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]

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]

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]

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]

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]

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]

And also if a simple_graph is a loopless multigraph V unit, this hom' definition corresponds to homomorphisms of simple graphs.

[Barrie Cooper]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

@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]

@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]

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

[Barrie Cooper]

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]

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]

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]

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

[Barrie Cooper]

@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]

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]

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]

If I had a term of H.is_subgraph_of G, then that could also be interpreted as, for example, Hv ->_inj Gvwhere 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]

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]

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]

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]

... 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]

@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]

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]

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]

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

This seems pedagogically complicated...

[Barrie Cooper]

@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]

@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]

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]

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]

In that particular case, you can define ε₂ as λ _, ⟦(b,c)⟧, the constant function whose value everywhere is ⟦(b,c)⟧.

[Barrie Cooper]

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]

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]

Or maybe, to avoid complications using fin,

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

[Barrie Cooper]

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]

Yeah, that's hard.

[Barrie Cooper]

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]

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]

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]

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]

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

[Barrie Cooper]

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

[Yaël Dillies]

Nono, I mean it the other way around.

[Yaël Dillies]

You defined your vertices and edges as sets (coerced to Type). Lean has no clue how to exhaust those.

[Yaël Dillies]

Compare that with ℕ where the two constructors are explicit from the inductive definition of ℕ.

[Barrie Cooper]

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]

What are the graphs you're after?

[Yaël Dillies]

And do you really need to label the edges?

[Yaël Dillies]

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

[Yaël Dillies]

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

[Barrie Cooper]

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

[Yaël Dillies]

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

[Barrie Cooper]

Indeed.

[Barrie Cooper]

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]

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]

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

[Yaël Dillies]

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

[Barrie Cooper]

4 vertices and 3 edges joined in a line.

[Barrie Cooper]

Sometimes called a path graph on 4 vertices.

[Yaël Dillies]

Ah yeah. And C4?

[Barrie Cooper]

Cycle graph on 4 vertices.

[Barrie Cooper]

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]

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]

the idea being that you set f ⟦(a, b)⟧ to be the number of edges you want between a and b.

[Barrie Cooper]

Thanks - I'll have a play ...

[Barrie Cooper]

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]

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]

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

[Yaël Dillies]

And great Barrie!

[Yaël Dillies]

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

[Yakov Pechersky]

I think the solution here is using fintypes

[Barrie Cooper]

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]

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

[Yakov Pechersky]

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]

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]

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]

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]

@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]

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]

(sym2.lift is a nice new function for defining functions whose domain is sym2)

[Kyle Miller]

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]

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]

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]

Here's one way to write a tactic proof:

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

[Kyle Miller]

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

[Kyle Miller]

I didn't know this would work:

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

[Kyle Miller]

trivial seems to be doing this:

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

[Kyle Miller]

tactic#contradiction

[Eric Rodriguez]

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

[Eric Rodriguez]

it's equation compiler magic iirc

[Kyle Miller]

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]

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_trivialevaluates 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]

Thanks - I knew it would be something simple.

[Barrie Cooper]

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]

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]

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]

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]

match should work for that

[Barrie Cooper]

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]

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]

you can also inline them into α₁

[Mario Carneiro]

you can also prove the proof part using a match if you want to

[Mario Carneiro]

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]

or

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

[Mario Carneiro]

(note - untested)

[Peter Nelson]

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]

(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]

Is fin 2 easier to use than bool?

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

[Yaël Dillies]

Or, better, src tgt : E → V.

[Yaël Dillies]

You can even extends (E → V) × (E → V) to access prod.swap (which corresponds to reversing the arrows).

[Yaël Dillies]

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]

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]

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]

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]

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]

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]

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]

@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]

Ah I missed that context, thanks

[Bhavik Mehta]

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]

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]

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]

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]

To be able to use = we would need both the vertex and the edge type out of the structure, right?

[Kyle Miller]

Yes, but also making E be a parameter doesn't make much sense for this definition.

[Kyle Miller]

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]

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]

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]

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

[Kyle Miller]

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

[Antoine Labelle]

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]

(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]

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]

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

[Yaël Dillies]

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]

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

[Yaël Dillies]

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]

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]

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]

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]

What about multigraph E?

[Yaël Dillies]

There's V as a field, right? So equality is meaningless.

[Peter Nelson]

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]

Maybe, but you can't prove lattice (multigraph E) which I think you will need for anything remotely non trivial.

[Peter Nelson]

Why not?

[Peter Nelson]

Ah right, it's not a partial order.

[Peter Nelson]

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]

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]

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]

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

[Kyle Miller]

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]

There are more thoughts in the comment on #16100.

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kyle Miller]

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]

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

[Antoine Labelle]

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]

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]

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

[Rémi Bottinelli]

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]

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]

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]

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

[Antoine Labelle]

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]

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

[Antoine Labelle]

Yes

[Antoine Labelle]

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

[Kyle Miller]

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]

Maybe :shrug:

[Yaël Dillies]

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

[Antoine Labelle]

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]

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

[Kyle Miller]

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

[Antoine Labelle]

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

Yes, I was just answering to Yaël.