Graphs and paths in graphs

Stream: Is there code for X?

[Floris Cnossen]

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]

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

[Julian Külshammer]

@David Wärn added it.

[David Wärn]

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

[David Wärn]

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

[David Wärn]

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]

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]

Do we have the free category on a graph?

[Bhavik Mehta]

Not that I know of

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

2537 commits behind master :expressionless:

[Adam Topaz]

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

[David Wärn]

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]

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

[Adam Topaz]

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

[David Wärn]

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

[Adam Topaz]

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

[David Wärn]

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]

You could also use bundled subquivers to talk about spanning trees

[David Wärn]

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]

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

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]

@Adam Topaz, @David Wärn, how about we try the following:
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]

Sounds good to me!

[Scott Morrison]

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]

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]

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]

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]

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

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

[Scott Morrison]

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]

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

[Scott Morrison]

This replacement is up as #7151.

[Adam Topaz]

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]

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]

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]

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]

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!