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⟶ 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→ V → Sort 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.

ink

class Quiver (V : Type u) : Type (maxuv)

• The type of edges/arrows/morphisms between a given source and target.

  Hom : V → V → Sort v

A quiver G on a type V of vertices assigns to every pair a b : V of vertices a type a ⟶ b⟶ b of arrows from a to b.

For graphs with no repeated edges, one can use Quiver.{0} V, which ensures a ⟶ b : Prop⟶ b : Prop. For multigraphs, one can use Quiver.{v+1} V, which ensures a ⟶ b : Type v⟶ 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.

ink

def «term_⟶_» : Lean.TrailingParserDescr

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))

ink

structure Prefunctor (V : Type u₁) [inst : Quiver V] (W : Type u₂) [inst : Quiver W] : Sort (max(max(max(u₁+1)(u₂+1))v₁)v₂)

• The action of a (pre)functor on vertices/objects.

  obj : V → W

• The action of a (pre)functor on edges/arrows/morphisms.

  map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)

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

ink

theorem Prefunctor.ext {V : Type u} [inst : Quiver V] {W : Type u₂} [inst : Quiver W] {F : V ⥤q W} {G : V ⥤q W} (h_obj : ∀ (X : V), Prefunctor.obj F X = Prefunctor.obj G X) (h_map : ∀ (X Y : V) (f : X ⟶ Y), Prefunctor.map F f = Eq.recOn (_ : Prefunctor.obj G Y = Prefunctor.obj F Y) (Eq.recOn (_ : Prefunctor.obj G X = Prefunctor.obj F X) (Prefunctor.map G f))) : F = G

ink

@[simp]

theorem Prefunctor.id_obj (V : Type u_1) [inst : Quiver V] (X : V) : Prefunctor.obj (𝟭q V) X = X

ink

@[simp]

theorem Prefunctor.id_map (V : Type u_1) [inst : Quiver V] : ∀ {X Y : V} (f : X ⟶ Y), Prefunctor.map (𝟭q V) f = f

ink

def Prefunctor.id (V : Type u_1) [inst : Quiver V] : V ⥤q V

The identity morphism between quivers.

Equations

• 𝟭q V = { obj := fun X => X, map := fun {X Y} f => f }

ink

instance Prefunctor.instInhabitedPrefunctor (V : Type u_1) [inst : Quiver V] : Inhabited (V ⥤q V)

Equations

• Prefunctor.instInhabitedPrefunctor V = { default := 𝟭q V }

ink

@[simp]

theorem Prefunctor.comp_obj {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst : Quiver V] {W : Type u_5} [inst : Quiver W] (F : U ⥤q V) (G : V ⥤q W) (X : U) : Prefunctor.obj (F ⋙q G) X = Prefunctor.obj G (Prefunctor.obj F X)

ink

@[simp]

theorem Prefunctor.comp_map {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst : Quiver V] {W : Type u_5} [inst : Quiver W] (F : U ⥤q V) (G : V ⥤q W) : ∀ {X Y : U} (f : X ⟶ Y), Prefunctor.map (F ⋙q G) f = Prefunctor.map G (Prefunctor.map F f)

ink

def Prefunctor.comp {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst : Quiver V] {W : Type u_5} [inst : Quiver W] (F : U ⥤q V) (G : V ⥤q W) : U ⥤q W

Composition of morphisms between quivers.

Equations

• F ⋙q G = { obj := fun X => Prefunctor.obj G (Prefunctor.obj F X), map := fun {X Y} f => Prefunctor.map G (Prefunctor.map F f) }

ink

@[simp]

theorem Prefunctor.comp_id {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst : Quiver V] (F : U ⥤q V) : F ⋙q 𝟭q V = F

ink

@[simp]

theorem Prefunctor.id_comp {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst : Quiver V] (F : U ⥤q V) : 𝟭q U ⋙q F = F

ink

@[simp]

theorem Prefunctor.comp_assoc {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst : Quiver V] [inst : Quiver W] [inst : Quiver Z] (F : U ⥤q V) (G : V ⥤q W) (H : W ⥤q Z) : F ⋙q G ⋙q H = F ⋙q (G ⋙q H)

ink

def Prefunctor.«term_⥤q_» : Lean.TrailingParserDescr

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))

ink

def Prefunctor.«term_⋙q_» : Lean.TrailingParserDescr

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))

ink

def Prefunctor.«term𝟭q» : Lean.ParserDescr

Notation for the identity prefunctor on a quiver.

Equations

• Prefunctor.«term𝟭q» = Lean.ParserDescr.node `Prefunctor.term𝟭q 1024 (Lean.ParserDescr.symbol "𝟭q")

ink

instance Quiver.opposite {V : Type u_1} [inst : Quiver V] : Quiver Vᵒᵖ

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

Equations

• Quiver.opposite = { Hom := fun a b => Opposite.unop b ⟶ Opposite.unop a }

ink

def Quiver.Hom.op {V : Type u_1} [inst : Quiver V] {X : V} {Y : V} (f : X ⟶ Y) : Opposite.op Y ⟶ Opposite.op X

The opposite of an arrow in V.

Equations

• Quiver.Hom.op f = f

ink

def Quiver.Hom.unop {V : Type u_1} [inst : Quiver V] {X : Vᵒᵖ} {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

• Quiver.Hom.unop f = f

ink

def Quiver.Empty (V : Type u) : Type u

A type synonym for a quiver with no arrows.

Equations

• Quiver.Empty V = V

ink

instance Quiver.emptyQuiver (V : Type u) : Quiver (Quiver.Empty V)

Equations

• Quiver.emptyQuiver V = { Hom := fun x x => PEmpty }

ink

@[simp]

theorem Quiver.empty_arrow {V : Type u} (a : Quiver.Empty V) (b : Quiver.Empty V) : (a ⟶ b) = PEmpty

ink

def Quiver.IsThin (V : Type u) [inst : Quiver V] : Prop

A quiver is thin if it has no parallel arrows.

Equations

• Quiver.IsThin V = ∀ (a b : V), Subsingleton (a ⟶ b)