Morphisms of quivers #

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

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

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

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] (X : V) :

(𝟭q V).obj X = X

source

instance Prefunctor.instInhabited (V : Type u_1) [Quiver V] :

Inhabited (V ⥤q V)

Equations

Prefunctor.instInhabited V = { default := 𝟭q V }

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

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

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