Documentation

Mathlib.Combinatorics.Quiver.Basic

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.

class 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.

  • Hom : VVSort 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
    Instances For
      structure Prefunctor (V : Type u₁) [Quiver V] (W : Type u₂) [Quiver W] :
      Sort (max (max (max (u₁ + 1) (u₂ + 1)) v₁) v₂)

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

      • obj : VW

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

      • map : {X Y : V} → (X Y)(self.obj X self.obj Y)

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

      Instances For
        theorem Prefunctor.mk_obj {V : Type u_1} [Quiver V] {obj : VV} {map : {X Y : V} → (X Y)(obj X obj Y)} {X : V} :
        { obj := obj, map := map }.obj X = obj X
        theorem Prefunctor.mk_map {V : Type u_1} [Quiver V] {obj : VV} {map : {X Y : V} → (X Y)(obj X obj Y)} {X : V} {Y : V} {f : X Y} :
        { obj := obj, map := map }.map f = map f
        theorem Prefunctor.ext {V : Type u} [Quiver V] {W : Type u₂} [Quiver W] {F : V ⥤q W} {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 = Eq.recOn (Eq.recOn (G.map f))) :
        F = G
        @[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] (X : V) :
        (𝟭q V).obj X = X
        def Prefunctor.id (V : Type u_1) [Quiver V] :
        V ⥤q V

        The identity morphism between quivers.

        Equations
        • 𝟭q V = { obj := fun (X : V) => X, map := fun {X Y : V} (f : X Y) => f }
        Instances For
          @[simp]
          theorem Prefunctor.comp_map {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {W : Type u_3} [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_obj {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {W : Type u_3} [Quiver W] (F : U ⥤q V) (G : V ⥤q W) (X : U) :
          (F ⋙q G).obj X = G.obj (F.obj X)
          def Prefunctor.comp {U : Type u_1} [Quiver U] {V : Type u_2} [Quiver V] {W : Type u_3} [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 : U) => G.obj (F.obj X), map := fun {X Y : U} (f : X Y) => G.map (F.map f) }
          Instances For
            @[simp]
            theorem Prefunctor.comp_id {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) :
            F ⋙q 𝟭q V = F
            @[simp]
            theorem Prefunctor.id_comp {U : Type u_1} {V : Type u_2} [Quiver U] [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)

            Notation for a prefunctor between quivers.

            Equations
            Instances For

              Notation for composition of prefunctors.

              Equations
              Instances For

                Notation for the identity prefunctor on a quiver.

                Equations
                Instances For
                  instance 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 : V} {Y : V} (f : X Y) :

                  The opposite of an arrow in V.

                  Equations
                  • f.op = { unop := f }
                  Instances For
                    def Quiver.Hom.unop {V : Type u_1} [Quiver V] {X : Vᵒᵖ} {Y : Vᵒᵖ} (f : X Y) :
                    Y.unop X.unop

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

                    Equations
                    • f.unop = f.unop
                    Instances For
                      def Quiver.Empty (V : Type u) :

                      A type synonym for a quiver with no arrows.

                      Equations
                      Instances For
                        Equations
                        @[simp]
                        theorem Quiver.empty_arrow {V : Type u} (a : Quiver.Empty V) (b : Quiver.Empty V) :
                        @[reducible]
                        def Quiver.IsThin (V : Type u) [Quiver V] :

                        A quiver is thin if it has no parallel arrows.

                        Equations
                        Instances For