Sophie Morel - Nori's construction in Lean

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic for the talk.

[Kevin Buzzard]

Wait a minute. I am looking through the files in Mathlib/Combinatorics/Quiver/ and out of all the ones I've looked at so far, every single one starts with something like

variable {U : Type _} [Quiver.{u + 1} U] {V : Type _} [Quiver.{v + 1} V] (φ : U ⥤q V) {W : Type _}
  [Quiver.{w + 1} W] (ψ : V ⥤q W)

Why do we not just refactor Quiver so that the arrows are type-valued? What is the counter-argument? It looks like the authors of the quiver files are already thinking this.

[Joël Riou]

Yes, I agree. The mathematical reason to allow Prop for morphisms in a quiver is to force that there is at most one morphism from X to Y, but we could introduce a typeclass saying exactly that (oh, it already exists: this is Quiver.IsThin).

[Kevin Buzzard]

Even Path.lean , which does allow Sort-valued quivers, has inductive Path {V : Type u} [Quiver.{v} V] (a : V) : V → Sort max (u + 1) v and that target Sort can never be Prop (because the max of u+1 and v can't be 0) but I suspect that this is the sort of thing which Lean would be very bad at knowing.

[Kevin Buzzard]

Joël Riou said:

(oh, it already exists: this is Quiver.IsThin).

Even better!

[Kevin Buzzard]

Ha ha ha, in the docstring of Quiver it says "For graphs with no repeated edges, one can use Quiver.{0} V, which ensures
a ⟶ b : Prop. " but if you search Mathlib for Quiver.{0} there are only two occurrences and they're both in docstrings :-) And even funnier, the second occurrence is in a Digraph file and it basically says "We could have used Quiver.{0} but actually this doesn't work because Quiver is a class and we don't want this, so we make Digraph V which is just copying the definition of Quiver.{0}.

So in fact we already have Digraph V for anyone who wants Quiver.{0}

[Kevin Buzzard]

(I'm trying the refactor)

[Sophie Morel]

Then we can talk about NatTrans. :grinning_face_with_smiling_eyes:

[Antoine Chambert-Loir]

Do you have slides that you can share?

[Sophie Morel]

expose.pdf
Here. (I did fix a couple of mistakes. One of my arrows was going in the wrong direction. :scream: )

[Patrick Massot]

You should not call this a mistake, call it duality.

[Joël Riou]

One of the missing ingredients in Sophie's talk, the fact that the localization of an abelian category with respect to a Serre class is also abelian, is in the draft PR #34444.