Quivers #
This module defines quivers. A quiver on a type V
of vertices assigns to every
pair a b : V
of vertices a type a ⟶ b
of arrows from a
to b
. This
is a very permissive notion of directed graph.
Implementation notes #
Currently Quiver
is defined with Hom : V → V → Sort v
.
This is different from the category theory setup,
where we insist that morphisms live in some Type
.
There's some balance here: it's nice to allow Prop
to ensure there are no multiple arrows,
but it is also results in error-prone universe signatures when constraints require a Type
.
A quiver G
on a type V
of vertices assigns to every pair a b : V
of vertices
a type a ⟶ b
of arrows from a
to b
.
For graphs with no repeated edges, one can use Quiver.{0} V
, which ensures
a ⟶ b : Prop
. For multigraphs, one can use Quiver.{v+1} V
, which ensures
a ⟶ b : Type v
.
Because Category
will later extend this class, we call the field Hom
.
Except when constructing instances, you should rarely see this, and use the ⟶
notation instead.
- Hom : V → V → Sort v
The type of edges/arrows/morphisms between a given source and target.
Instances
Notation for the type of edges/arrows/morphisms between a given source and target in a quiver or category.
Equations
- «term_⟶_» = Lean.ParserDescr.trailingNode `term_⟶_ 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶ ") (Lean.ParserDescr.cat `term 10))
Instances For
A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a Prefunctor
.
- obj : V → W
The action of a (pre)functor on vertices/objects.
The action of a (pre)functor on edges/arrows/morphisms.
Instances For
Equations
- Prefunctor.instInhabited V = { default := 𝟭q V }
Notation for a prefunctor between quivers.
Equations
- Prefunctor.«term_⥤q_» = Lean.ParserDescr.trailingNode `Prefunctor.term_⥤q_ 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥤q ") (Lean.ParserDescr.cat `term 51))
Instances For
Notation for composition of prefunctors.
Equations
- Prefunctor.«term_⋙q_» = Lean.ParserDescr.trailingNode `Prefunctor.term_⋙q_ 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋙q ") (Lean.ParserDescr.cat `term 61))
Instances For
Notation for the identity prefunctor on a quiver.
Equations
- Prefunctor.«term𝟭q» = Lean.ParserDescr.node `Prefunctor.term𝟭q 1024 (Lean.ParserDescr.symbol "𝟭q")
Instances For
Vᵒᵖ
reverses the direction of all arrows of V
.
Equations
- Quiver.opposite = { Hom := fun (a b : Vᵒᵖ) => (Opposite.unop b ⟶ Opposite.unop a)ᵒᵖ }
The opposite of an arrow in V
.
Equations
- f.op = Opposite.op f
Instances For
Given an arrow in Vᵒᵖ
, we can take the "unopposite" back in V
.
Equations
- f.unop = Opposite.unop f
Instances For
Equations
- Quiver.emptyQuiver V = { Hom := fun (x x : Quiver.Empty V) => PEmpty.{?u.13} }
A quiver is thin if it has no parallel arrows.
Equations
- Quiver.IsThin V = ∀ (a b : V), Subsingleton (a ⟶ b)