mathlib3 documentation

combinatorics.quiver.basic

Quivers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 arrow : 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.

@[class]
structure quiver (V : Type u) :
Type (max u v)

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.

Instances of this typeclass
Instances of other typeclasses for quiver
  • quiver.has_sizeof_inst
structure prefunctor (V : Type u₁) [quiver V] (W : Type u₂) [quiver W] :
Sort (max (imax (u₁+1) (u₁+1) v₁ v₂) (u₁+1) (u₂+1))

A morphism of quivers. As we will later have categorical functors extend this structure, we call it a prefunctor.

Instances for prefunctor
@[ext]
theorem prefunctor.ext {V : Type u} [quiver V] {W : Type u₂} [quiver W] {F G : V ⥤q W} (h_obj : (X : V), F.obj X = G.obj X) (h_map : (X Y : V) (f : X Y), F.map f = _.rec_on (_.rec_on (G.map f))) :
F = G
def prefunctor.id (V : Type u_1) [quiver V] :
V ⥤q V

The identity morphism between quivers.

Equations
Instances for prefunctor.id
@[simp]
theorem prefunctor.id_map (V : Type u_1) [quiver V] (X Y : V) (f : X Y) :
(𝟭q V).map f = f
@[simp]
theorem prefunctor.id_obj (V : Type u_1) [quiver V] (a : V) :
(𝟭q V).obj a = id a
@[protected, instance]
def prefunctor.inhabited (V : Type u_1) [quiver V] :
Equations
def prefunctor.comp {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : U ⥤q V) (G : V ⥤q W) :
U ⥤q W

Composition of morphisms between quivers.

Equations
Instances for prefunctor.comp
@[simp]
theorem prefunctor.comp_obj {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : U ⥤q V) (G : V ⥤q W) (X : U) :
(F ⋙q G).obj X = G.obj (F.obj X)
@[simp]
theorem prefunctor.comp_map {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] {W : Type u_5} [quiver W] (F : U ⥤q V) (G : V ⥤q W) (X Y : U) (f : X Y) :
(F ⋙q G).map f = G.map (F.map f)
@[simp]
theorem prefunctor.comp_id {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] (F : U ⥤q V) :
F ⋙q 𝟭q V = F
@[simp]
theorem prefunctor.id_comp {U : Type u_1} [quiver U] {V : Type u_3} [quiver V] (F : U ⥤q V) :
𝟭q U ⋙q F = F
@[simp]
theorem prefunctor.comp_assoc {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [quiver U] [quiver V] [quiver W] [quiver Z] (F : U ⥤q V) (G : V ⥤q W) (H : W ⥤q Z) :
F ⋙q G ⋙q H = F ⋙q (G ⋙q H)
@[protected, instance, irreducible]
def quiver.opposite {V : Type u_1} [quiver V] :

Vᵒᵖ reverses the direction of all arrows of V.

Equations
def quiver.hom.op {V : Type u_1} [quiver V] {X Y : V} (f : X Y) :

The opposite of an arrow in V.

Equations
Instances for quiver.hom.op
def quiver.hom.unop {V : Type u_1} [quiver V] {X Y : Vᵒᵖ} (f : X Y) :

Given an arrow in Vᵒᵖ, we can take the "unopposite" back in V.

Equations
Instances for quiver.hom.unop
@[nolint]
def quiver.empty (V : Type u) :

A type synonym for a quiver with no arrows.

Equations
Instances for quiver.empty
@[protected, instance]
Equations
@[simp]
theorem quiver.empty_arrow {V : Type u} (a b : quiver.empty V) :
(a b) = pempty
@[reducible]
def quiver.is_thin (V : Type u) [quiver V] :
Prop

A quiver is thin if it has no parallel arrows.

Equations