RFC: Quiver refactor

Stream: mathlib4

[Kevin Buzzard]

In her Lean Together talk, Sophie Morel was tripped up because she typed [Quiver.{v} V] and then got incomprehensible universe errors. Turns out that Mathlib is in fact full of [Quiver.{v + 1} V], because in 99% of our applications of quivers we need to demand that the hom types really are types rather than Prop. My proposal in #34228 is that we follow category theory and let hom types be Type v-valued rather than Sort v-valued; this removes about 60 +1s from mathlib.

However it breaks one thing: docs#Matrix.toQuiver is a construction which takes a square matrix over an ordered ring and returns a Prop-valued quiver on the type which indexes the rows and columns which is true iff the corresponding matrix entry is positive. Already one can see that this is the "wrong" definition, because Quiver is a class but Matrix.toQuiver is a definition rather than an instance.

My proposal is
(1) refactor Quiver so, like Category, the hom sets are Type-valued rather than Sort-valued
(2) change Matrix.toQuiver into Matrix.toDigraph.

@Matteo Cipollina is there a reason that you ultimately chose quivers rather than digraphs in #28728 ?

In #34228 I make a start on this refactor, just to see if I can get mathlib compiling. Right now I just use PLift to get the Matrix.toQuiver file compiling; Is this a satisfactory change or should I attempt the Digraph refactor? Right now I am a bit confused about why quivers are used here at all when digraphs seem more natural.

[Matteo Cipollina]

The issue was indeed raised in the review, I've chosen Quiver because it had more available API that was suited to the reasoning about paths and connectedness, as needed for the Perron Frobenius theorem.
I'll have a closer look, see how to refactor this where it is used (here) along your PR and let you know asap

[Kevin Buzzard]

If you look at #34228 (which is now compiling) then you can see what I've done currently: we're still using quivers, but the hom sets are in Type not Prop, and I use PLift.up and PLift.down to move between them.

[Matteo Cipollina]

It definitely looks the best solution, if we could avoid using Digraph it would be a smoother fix in my view. Thanks!

[Kevin Buzzard]

So what is wrong with Digraph? Looking at the repo you sent, you have this @Quiver.Path and @Path etc -- I suspect that here you're fighting the typeclass system, and presumably you won't have to do these @s if you use digraphs?

[Matteo Cipollina]

Screenshot 2026-01-21 at 21.36.15.png
The only thing wrong with Digraph was the lack of relevant API vs Quiver. It would have required providing or porting from Quiver a lot of API

[Joël Riou]

The standard procedure here would be to replace def toQuiver (A : Matrix n n R) : Quiver n := ... by the definition of a type synonym for n with A as a parameter and to set up a quiver structure on it.

[Matteo Cipollina]

something like this?

module

public import Mathlib.Combinatorics.Quiver.ConnectedComponent
public import Mathlib.Combinatorics.Quiver.Path.Vertices
public import Mathlib.Data.Matrix.Mul

@[expose] public section
namespace Matrix

open Quiver Quiver.Path

variable {n R : Type*} [Ring R] [LinearOrder R]

/- current definition
/-- The directed graph (quiver) associated with a matrix `A`,
with an edge `i ⟶ j` iff `0 < A i j`. -/
def toQuiver (A : Matrix n n R) : Quiver n :=
  ⟨fun i j => 0 < A i j⟩-/

def MatrixQuiver (_ : Matrix n n R) := n
instance (A : Matrix n n R) : Quiver (MatrixQuiver A) where
  Hom := fun i j => 0 < A i j

/-- A matrix `A` is irreducible if it is entrywise nonnegative and
its quiver of positive entries (`toQuiver A`) is strongly connected. -/
@[mk_iff] structure IsIrreducible (A : Matrix n n R) : Prop where
  nonneg (i j : n) : 0 ≤ A i j
  connected : @IsSStronglyConnected n (inferInstanceAs (Quiver (MatrixQuiver A)))

[Joël Riou]

Yes, and at the end IsSStronglyConnected (MatrixQuiver A) should work.
(Note that after Kevin's refactor, you will have to lift(0 < A i j) : Prop to Type.)

[Kevin Buzzard]

That's assuming the refactor happens! This construction here seems to be an argument against it? But everywhere else in mathlib we are writing Quiver.{v+1}. If there were a refactor the other way -- someone came along and said "I think Quiver homs should be Sort-valued, here's my PR, oh by the way I had to add 60 +1s" then people would probably say "I think that those 60 +1s are an indication that this is a bad idea".