## Stream: Is there code for X?

### Topic: Graphs and paths in graphs

#### Floris Cnossen (Mar 27 2021 at 19:21):

I'm new to Lean and I was wondering if someone has already defined the most general form of a graph:
A directed multigraph. I will need paths in these graph and I'm looking for something like

class graph (V : Type u) : Type (max u (v+1)) :=
(arrows : V → V → Type v)

inductive paths {V : Type u} [G : graph V] (x : V) : V → Sort*
| id  []           : paths x
| append {y z : V} : paths y → graph.arrows y z → paths z


I will also need composition of paths and I already tried the following:

def path_comp {V : Type u} [G : graph V] {x y z : V}
(p : paths x y) (q : paths y z) : paths x z :=
begin
induction q with z' w' h qh pq,
exact p,
exact pq.append qh,
end


However, I would prefer a definition like

def path_comp {V : Type u} [G : graph V] {x y z : V} : paths x y → paths y z → paths x z
| p id            := p
| p (append q a)  := (path_comp p q).append a


but this gives multiple error that I don't understand yet. My question is if there already exists a
general theory for these types of graphs. And if not, what I'm doing wrong.

#### Julian Külshammer (Mar 27 2021 at 19:29):

They exist under the name of docs#quiver with some basic theory, fairly recent.

#### David Wärn (Mar 27 2021 at 19:44):

Yes, we have paths, and there is a PR for composition of paths #6847

#### David Wärn (Mar 27 2021 at 19:45):

The only problem with your definition seems to be that you need to generalize over z in the definition

#### David Wärn (Mar 27 2021 at 19:47):

def path_comp {V : Type u} [G : graph V] {x y : V} : Π {z}, paths x y → paths y z → paths x z
| y p (paths.id _)        := p
| z p (paths.append q a)  := (path_comp p q).append a


#### Floris Cnossen (Mar 27 2021 at 19:58):

Thank you, a quiver seems to be exactly what I need. Also thanks for fixing my definition. I think now I have a better understanding of the definition.

#### Scott Morrison (Mar 28 2021 at 00:22):

Do we have the free category on a graph?

#### Bhavik Mehta (Mar 28 2021 at 00:29):

Not that I know of

#### Adam Topaz (Mar 28 2021 at 00:57):

I made this construction at some point, but I don't remember if it was on a mathlib branch or not...

#### Adam Topaz (Mar 28 2021 at 00:59):

There was some discussion in the prefunctor(?) topic in this stream

#### Adam Topaz (Mar 28 2021 at 01:07):

I guess what I made is here branch#free_cat but it's now 7 months old

#### Adam Topaz (Mar 28 2021 at 01:08):

2537 commits behind master :expressionless:

#### Adam Topaz (Mar 28 2021 at 01:09):

The uniqueness of the lift construction seems to be missing there too...

#### David Wärn (Mar 28 2021 at 08:49):

The free category is also in branch#hedetniemi, but that's even older... #6847 defines all the operations in the underlying path category and shows associativity etc. What's missing is 1) a notion of graph homomorphism 2) a forgetful functor Cat => Graph 3) the universal property of the category of paths

#### Scott Morrison (Mar 28 2021 at 09:22):

I'm sure I can find an even older one... Maybe even 2017. :-)

#### Adam Topaz (Mar 28 2021 at 12:32):

Is there a reason docs#quiver is not a class?

#### David Wärn (Mar 28 2021 at 12:55):

Yes, I want to put different quivers on the same vertex set (e.g. a graph and its spanning tree)

#### Adam Topaz (Mar 28 2021 at 12:57):

Makes sense. Although it would be nice to automatically get a quiver from a category

#### David Wärn (Mar 28 2021 at 13:29):

It would be nice. It's possible that we'd be better off making quiver a class (or just using docs#category_theory.has_hom) and introducing a type synonym whenever we put a new quiver on our vertex set. We'll need a type synonym anyway for the path category on a graph. But for the stuff I've done so far, the current setup works well, and I don't have any plans to add more stuff

#### Adam Topaz (Mar 28 2021 at 13:32):

You could also use bundled subquivers to talk about spanning trees

#### David Wärn (Mar 28 2021 at 16:25):

Actually now that I think about it, it shouldn't be difficult to refactor docs#quiver to use has_hom instead. We'd need a type synonym for docs#quiver.symmetrify, but everything else should work well

#### David Wärn (Mar 28 2021 at 16:32):

(Currently I need to promote subquivers to quivers to talk about paths in a subquiver. But you could alternatively show that a subquiver gives you a subquiver of the path quiver)

#### Adam Topaz (Mar 28 2021 at 17:08):

The usual trick is to define a coercion to type on bundled subobjects, and construct an instance of the class on the associated type

#### Scott Morrison (Apr 10 2021 at 06:13):

1) make quiver a class
2) replace has_hom with quiver
3) install prefunctor (or some other name) above functor, for morphisms of quivers?

If this doesn't seem crazy, I can give it a go. I would like to have a convenient API for path categories soon.

#### David Wärn (Apr 10 2021 at 08:02):

Sounds good to me!

#### Scott Morrison (Apr 10 2021 at 10:49):

Ah: @David Wärn, a problem here will be that we would have to change quiver so arrows live in Type v, rather than Sort v (for the same reasons this is necessary in the category theory library). Can you live with this?

#### Scott Morrison (Apr 10 2021 at 10:49):

Note the restriction is actually already hiding in your code, but obscured because there aren't explicit universe annotations. For example symmetrify secretly requires v > 0.

#### David Wärn (Apr 10 2021 at 10:56):

I don't mind, I only use Type v-valued quivers. But is it really necessary? Can't we e.g. make category extend quiver.{v+1}? (Btw, this obfuscation is ameliorated in #6840.)

#### Scott Morrison (Apr 10 2021 at 11:19):

Maybe? To be honest, I still have nightmares from changing between Type v and Sort v in the category definition several times, and would prefer to keep things uniform and simple. :-)

#### Scott Morrison (Apr 10 2021 at 11:31):

@David Wärn, I've converted it to a class in #7150. If you could have a look over that it would be great.

#### Scott Morrison (Apr 10 2021 at 11:31):

I'll immediately try to replace has_hom with quiver, however.

#### Scott Morrison (Apr 10 2021 at 11:44):

As long as you don't mind if the arrow field of quiver gets renamed to hom, this turns out to be completely straightforward.

#### Scott Morrison (Apr 10 2021 at 11:47):

(It would not be insane to rename the hom field of category to arrow, of course, just a lot of work.)

#### Scott Morrison (Apr 10 2021 at 11:49):

This replacement is up as #7151.

#### Adam Topaz (Apr 10 2021 at 23:05):

I'm a bit late to respond here... but I'm 100% supportive of this refactor!

What are the immediate applications besides the free category on a quiver construction?

#### Scott Morrison (Apr 10 2021 at 23:41):

The reason I'm doing this now is that I want cheap access to limits and colimits of chain complexes. The plan is to show that our new "shapeless" complexes are equivalent to a particular subcategory of functors from the path category on the complete quiver of the indexing type. That subcategory is the subcategory of functors supported on the paths of length one (because d^2 = 0) and which are allowed by the shape. Finally, not only do functor categories J \func C have whatever limits C has, the subcategory of functors supported on some specified set of morphisms in J has those same limits. (I think?)

#### Scott Morrison (Apr 10 2021 at 23:42):

I have another branch with bundled Quiver, and the free and forget functors. I'll see if the adjunction runs into any 2-categorical horrors, and if not make a separate PR then mark all three for review.

#### Adam Topaz (Apr 10 2021 at 23:43):

I think the category of prefunctors(?) from J to C where C is a category is equivalent to the category of functors from the free cat on J to C, so this sounds reasonable!

#### Scott Morrison (Apr 11 2021 at 03:05):

I'm a little tempted to introduce semicategories and semifunctors (no mention of identities) at some point. I think that karoubi (=idempotent) completion has some nice property when thought of as sending semicategories to categories. (Right adjoint to forgetting identities?) Semicategories are occasionally useful, e.g. in geometric field theory where every slice of spacetime has non-zero thickness. But not something we're going to get to anytime soon!

Last updated: May 07 2021 at 22:14 UTC