feat(Quiv): add the empty, vertex, point, interval, and walking quivers

[robertmaxton42]

Add:

• The empty quiver
• The vertex quiver (one vertex, and no edges) and the point quiver (one vertex, one self-edge)
• The interval quiver (two vertices with an edge between them)
• The walking quiver (vertices 0 and 1 with two edges both 0 -> 1. Functors from the walking quiver to Type define quivers, by interpreting F.obj 0 as the type of vertices, F.obj 1 as the type of edges, using one of the two edges to label the source of every edge and using the other to label the target.)

• depends on: [Merged by Bors] - feat: homOfEq lemmas #24538

---

[github-actions]

PR summary b6771ef6f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Category.Quiv.WalkingQuiver (new file)	504
Mathlib.CategoryTheory.Category.Quiv.Shapes (new file)	708

---

Declarations diff

+ Empty
+ Interval
+ Interval.casesOn_hom
+ Interval.hom
+ Interval.left
+ Interval.prefunctor
+ Interval.prefunctor.ext
+ Interval.prefunctor.ext_iff
+ Interval.right
+ Point
+ Point.prefunctor
+ Point.prefunctor.ext
+ Point.prefunctor.ext_iff
+ Shrink.out
+ Vert
+ Vert.prefunctor
+ Vert.prefunctor.ext
+ WalkingQuiver
+ WalkingQuiver.Hom
+ WalkingQuiver.forget
+ casesOn'
+ casesOn_fun
+ delabWalkingQuiverOne
+ delabWalkingQuiverZero
+ emptyIsInitial
+ forallHom_byCases
+ forall_byCases
+ forall₀₀
+ forall₀₁
+ forall₁₀
+ forall₁₁
+ funByCases
+ funByCases_eq
+ hom₀₁_empty
+ id_def
+ initialIsoEmpty
+ instance (X Y : WalkingQuiver) :
+ instance : Category WalkingQuiver
+ instance : ConcreteCategory WalkingQuiver WalkingQuiver.Hom
+ instance : HasInitial Quiv := emptyIsInitial.hasInitial
+ instance : HasTerminal Quiv := pointIsTerminal.hasTerminal
+ instance : IsEmpty Empty
+ instance : OfNat WalkingQuiver 0 := ⟨WalkingQuiver.zero⟩
+ instance : OfNat WalkingQuiver 1 := ⟨WalkingQuiver.one⟩
+ instance : One 𝕀 := ⟨Interval.right⟩
+ instance : Quiver.{v + 1} Empty.{v}
+ instance : Quiver.{v + 1} Interval.{v}
+ instance : Quiver.{v + 1} Point.{v}
+ instance : Quiver.{v + 1} Vert.{v}
+ instance : Zero 𝕀 := ⟨Interval.left⟩
+ one_eq
+ pointIsTerminal
+ terminalIsoPoint
+ zero_eq
+ 𝕀.hom
+ 𝕀.left
+ 𝕀.right

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat: homOfEq lemmas #24538
  By Dependent Issues (🤖). Happy coding!

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[robin-carlier]

I apologize if this is a stupid question, but why does the "Walking Quiver" have an id morphism? Isn’t that making it the walking reflexive quiver? It also seems to me that this construction is identical to CategoryTheory.Limits.WalkingParallelPair.

[joelriou]

I do not think we want/need this definition (which seems to be unused in the rest of the PR).

[robertmaxton42]

It is used in a following PR on (co)limits in Quivers, where it greatly simplifies notation by enabling the projection notation: x.out versus having (equivShrink _).symm x everywhere.

That said, I forget why I lumped it into this PR.

[joelriou]

There are a few issues with this PR. One of these is that in category theory (and the same should apply for quivers and refl quivers), it is better practice not to define directly objects in Cat, but rather define a Category instance on a type, and only later, we may use Cat.of C if we need a term in Cat.
As it was observed by @robin-carlier , some of the quivers considered in this PR are refl quivers or even categories (and may have already been defined elsewhere), which also supports my previous remark about Quiver vs Quiv.

[robertmaxton42]

Mmm. Maybe. The original reason for that is that it is difficult to define quiver shapes with a specific morphism universe level without defining the carrier type and the Quiver instance at the same time. But I did recently pick up a trick for that, so... let's see if it works!

[robertmaxton42]

I apologize if this is a stupid question, but why does the "Walking Quiver" have an id morphism? Isn’t that making it the walking reflexive quiver? It also seems to me that this construction is identical to CategoryTheory.Limits.WalkingParallelPair.

It's a category, yes. I call it the WalkingQuiver because nLab does every functor $$\mathbf{WalkingQuiv}\Rightarrow\mathbf{Set}$$ defines a quiver, rather than being just a quiver in and of itself.

I hadn't thought of WalkingParallelPair; I'll see if its API is friendly enough to adapt the rest of the fork.

[robin-carlier]

I apologize if this is a stupid question, but why does the "Walking Quiver" have an id morphism? Isn’t that making it the walking reflexive quiver? It also seems to me that this construction is identical to CategoryTheory.Limits.WalkingParallelPair.

It's a category, yes. I call it the WalkingQuiver because nLab does every functor WalkingQuiv ⇒ Set defines a quiver, rather than being just a quiver in and of itself.

I hadn't thought of WalkingParallelPair; I'll see if its API is friendly enough to adapt the rest of the fork.

But a functor WalkingQuiv ⥤ Type will define you a reflexive quiver rather than a plain quiver (at least, the image quiver will have the images of the identities maps as distinguished hom), right?
To be reasonably called the "Walking quiver", you’d expect an equivalence of categories (WalkingQuiv ⥤ Type) ≌ Quiv (let’s ignore universes for now). In this case I believe you have an equivalence (WalkingQuiv ⥤ Type) ≌ ReflQuiv, but I don’t think the forgetful functor from ReflQuiv to Quiv is an equivalence (I don’t see how you can realize the "interval" quiver that you define in the essential image). Edit: I think I see the point that you can think of WalkingQuiver as shapes for quivers the same way we can think of reflexive quivers as certain 2-truncated simplicial types, but I think the name WalkingQuiver will just cause confusion (at least, I certainly was confused).

[robertmaxton42]

I apologize if this is a stupid question, but why does the "Walking Quiver" have an id morphism? Isn’t that making it the walking reflexive quiver? It also seems to me that this construction is identical to CategoryTheory.Limits.WalkingParallelPair.

It's a category, yes. I call it the WalkingQuiver because nLab does every functor WalkingQuiv ⇒ Set defines a quiver, rather than being just a quiver in and of itself.
I hadn't thought of WalkingParallelPair; I'll see if its API is friendly enough to adapt the rest of the fork.

But a functor WalkingQuiv ⥤ Type will define you a reflexive quiver rather than a plain quiver (at least, the image quiver will have the images of the identities maps as distinguished hom), right?

Nope! The quiver isn't the image of the functor, it just so happens to have the same data as the functor does. To construct an F : WalkingQuiv ⥤ Type, you need to provide:

• Two types, for 0 and for 1.
• Two functions, both between 0 and 1.

From this data, I can create a quiver by

• Using F.obj 0 as the carrier type, the type of vertices
• Using F.obj 1 as the 'total' hom type, a type that will end up being ≃ Σ (X Y : F.obj 0), X ⟶ Y
• Assigning the source of every hom e to the value of F.map .source e
• Assigning the target of every hom e to the value of F.map .target e

That is,

def quivOfFunc (F : WalkingQuiv ⥤ Type u) : Quiv.{u, u} where
  α := F.obj 0
  str := { Hom X Y := { e : F.obj 1 // F.map .source e = X ∧ F.map .target e = Y }

And naturally I can turn that around. So at least for 'homogenous' quivers (quivers .{u, u} with morphisms and objects at the same universe level), I can easily produce an equivalence between WalkingQuiv ⥤ Type u and Quiv.{u, u}. The case of mixed universe levels is more complicated.

[robin-carlier]

Yes, in the meantime I realized that this was what you were going for (again, this is similar to the construction OneTruncation₂ for reflexive quivers). Apologies for the confusion (and it’s really a brain fart on my end since I worked with OneTruncation₂ literally yesterday). Though I stick to the idea that we should find a better name than "WalkingQuiver" for this.
(edit: the name also becomes a non-issue if we use the existing WalkingParallelPair :D)

[joelriou]

Definitions of quivers should rather be in the folder Combinatorics.Quiver. For the naming conventions, instead of Quiv.Empty, we should use Quiver.Empty (see Combinatorics.Quiver.SingleObj for example).

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.