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.

source
@[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
source
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
source
@[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
source
def prefunctor.id (V : Type u_1) [quiver V] :
V ⥤q V

The identity morphism between quivers.

Equations
Instances for prefunctor.id
source
@[simp]
theorem prefunctor.id_map (V : Type u_1) [quiver V] (X Y : V) (f : X ⟶ Y) :
(𝟭q V).map f = f
source
@[simp]
theorem prefunctor.id_obj (V : Type u_1) [quiver V] (a : V) :
(𝟭q V).obj a = id a
source
@[protected, instance]
def prefunctor.inhabited (V : Type u_1) [quiver V] :
inhabited (V ⥤q V)
Equations
source
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
source
@[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)
source
@[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)
source
@[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
source
@[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
source
@[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)
source
@[protected, instance, irreducible]
def quiver.opposite {V : Type u_1} [quiver V] :
quiver Vᵒᵖ

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

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

The opposite of an arrow in V.

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

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

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

A type synonym for a quiver with no arrows.

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

A quiver is thin if it has no parallel arrows.

Equations