Documentation

Mathlib.Combinatorics.Quiver.Prefunctor

Morphisms of quivers #

source
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 : V → W

    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
    source
    theorem Prefunctor.mk_obj {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V} :
    { obj := obj, map := map }.obj X = obj X
    source
    theorem Prefunctor.mk_map {V : Type u_1} {W : Type u_2} [Quiver V] [Quiver W] {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X Y : V} {f : X ⟶ Y} :
    { obj := obj, map := map }.map f = map f
    source
    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 = Eq.recOn ⋯ (Eq.recOn ⋯ (G.map f))) :
    F = G
    source
    theorem Prefunctor.ext' {V W : Type u} [Quiver V] [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 = Quiver.homOfEq (G.map f) ⋯ ⋯) :
    F = G

    This may be a more useful form of Prefunctor.ext.

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

    The identity morphism between quivers.

    Equations
      Instances For
        source
        @[simp]
        theorem Prefunctor.id_obj (V : Type u_1) [Quiver V] (X : V) :
        (𝟭q V).obj X = X
        source
        @[simp]
        theorem Prefunctor.id_map (V : Type u_1) [Quiver V] {X✝ Y✝ : V} (f : X✝ ⟶ Y✝) :
        (𝟭q V).map f = f
        source
        instance Prefunctor.instInhabited (V : Type u_1) [Quiver V] :
        Inhabited (V ⥤q V)
        Equations
          source
          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
            Instances For
              source
              @[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)
              source
              @[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)
              source
              @[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
              source
              @[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
              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
              def Prefunctor.«term_⥤q_» :
              Lean.TrailingParserDescr

              Notation for a prefunctor between quivers.

              Equations
                Instances For
                  source
                  def Prefunctor.«term_⋙q_» :
                  Lean.TrailingParserDescr

                  Notation for composition of prefunctors.

                  Equations
                    Instances For
                      source
                      def Prefunctor.«term𝟭q» :
                      Lean.ParserDescr

                      Notation for the identity prefunctor on a quiver.

                      Equations
                        Instances For
                          source
                          theorem Prefunctor.congr_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} {f g : X ⟶ Y} (h : f = g) :
                          F.map f = F.map g
                          source
                          theorem Prefunctor.congr_obj {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) (X : U) :
                          F.obj X = G.obj X

                          An equality of prefunctors gives an equality on objects.

                          source
                          theorem Prefunctor.congr_hom {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U} (f : X ⟶ Y) :
                          Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

                          An equality of prefunctors gives an equality on homs.

                          source
                          @[simp]
                          theorem Prefunctor.homOfEq_map {U : Type u_1} {V : Type u_2} [Quiver U] [Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y) {X' Y' : U} (hX : X = X') (hY : Y = Y') :
                          F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

                          Prefunctors commute with homOfEq.