Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: David WΓ€rn, Scott Morrison
Ported by: Scott Morrison

! This file was ported from Lean 3 source module combinatorics.quiver.basic
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Opposite

/-!
# 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 `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`.
-/

open Opposite

-- We use the same universe order as in category theory.
-- See note [CategoryTheory universes]
universe v vβ vβ u uβ uβ

/-- 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.
-/
class Quiver: {V : Type u} β (V β V β Sort v) β Quiver VQuiver (V: Type uV : Type u: Type (u+1)Type u) where
/-- The type of edges/arrows/morphisms between a given source and target. -/
Hom: {V : Type u} β [self : Quiver V] β V β V β Sort vHom : V: Type uV β V: Type uV β Sort v: Type vSortSort v: Type v v
#align quiver Quiver: Type u β Type (maxuv)Quiver
#align quiver.hom Quiver.Hom: {V : Type u} β [self : Quiver V] β V β V β Sort vQuiver.Hom

/--
Notation for the type of edges/arrows/morphisms between a given source and target
in a quiver or category.
-/
infixr:10 " βΆ " => Quiver.Hom: {V : Type u} β [self : Quiver V] β V β V β Sort vQuiver.Hom

/-- A morphism of quivers. As we will later have categorical functors extend this structure,
we call it a `Prefunctor`. -/
structure Prefunctor: {V : Type uβ} β
[inst : Quiver V] β
{W : Type uβ} β [inst_1 : Quiver W] β (obj : V β W) β ({X Y : V} β (X βΆ Y) β (obj X βΆ obj Y)) β Prefunctor V WPrefunctor (V: Type uβV : Type uβ: Type (uβ+1)Type uβ) [Quiver: Type ?u.7832 β Type (max?u.7832vβ)Quiver.{vβ} V: Type uβV] (W: Type uβW : Type uβ: Type (uβ+1)Type uβ) [Quiver: Type ?u.7837 β Type (max?u.7837vβ)Quiver.{vβ} W: Type uβW] where
/-- The action of a (pre)functor on vertices/objects. -/
obj: {V : Type uβ} β [inst : Quiver V] β {W : Type uβ} β [inst_1 : Quiver W] β Prefunctor V W β V β Wobj : V: Type uβV β W: Type uβW
/-- The action of a (pre)functor on edges/arrows/morphisms. -/
map: {V : Type uβ} β
[inst : Quiver V] β
{W : Type uβ} β
[inst_1 : Quiver W] β
(self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (Prefunctor.obj self X βΆ Prefunctor.obj self Y)map : β {X: VX Y: VY : V: Type uβV}, (X: VX βΆ Y: VY) β (obj: V β Wobj X: VX βΆ obj: V β Wobj Y: VY)
#align prefunctor Prefunctor: (V : Type uβ) β [inst : Quiver V] β (W : Type uβ) β [inst : Quiver W] β Sort (max(max(max(uβ+1)(uβ+1))vβ)vβ)Prefunctor

pp_extended_field_notation Prefunctor.obj: {V : Type uβ} β [inst : Quiver V] β {W : Type uβ} β [inst_1 : Quiver W] β Prefunctor V W β V β WPrefunctor.obj
pp_extended_field_notation Prefunctor.map: {V : Type uβ} β
[inst : Quiver V] β
{W : Type uβ} β [inst_1 : Quiver W] β (self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)Prefunctor.map

namespace Prefunctor

@[ext]
theorem ext: β {V : Type u} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] {F G : Prefunctor V W}
(h_obj : β (X : V), F.obj X = G.obj X),
(β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))) β
F = Gext {V: Type uV : Type u: Type (u+1)Type u} [Quiver: Type ?u.22889 β Type (max?u.22889vβ)Quiver.{vβ} V: Type uV] {W: Type uβW : Type uβ: Type (uβ+1)Type uβ} [Quiver: Type ?u.22894 β Type (max?u.22894vβ)Quiver.{vβ} W: Type uβW] {F: Prefunctor V WF G: Prefunctor V WG : Prefunctor: (V : Type ?u.22914) β
[inst : Quiver V] β
(W : Type ?u.22913) β [inst : Quiver W] β Sort (max(max(max(?u.22914+1)(?u.22913+1))?u.22916)?u.22915)Prefunctor V: Type uV W: Type uβW}
(h_obj: β (X : V), F.obj X = G.obj Xh_obj : β X: ?m.22928X, F: Prefunctor V WF.obj: {V : Type ?u.22933} β [inst : Quiver V] β {W : Type ?u.22932} β [inst_1 : Quiver W] β Prefunctor V W β V β Wobj X: ?m.22928X = G: Prefunctor V WG.obj: {V : Type ?u.22951} β [inst : Quiver V] β {W : Type ?u.22950} β [inst_1 : Quiver W] β Prefunctor V W β V β Wobj X: ?m.22928X)
(h_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))h_map : β (X: VX Y: VY : V: Type uV) (f: X βΆ Yf : X: VX βΆ Y: VY),
F: Prefunctor V WF.map: {V : Type ?u.22981} β
[inst : Quiver V] β
{W : Type ?u.22980} β
[inst_1 : Quiver W] β (self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map f: X βΆ Yf = Eq.recOn: {Ξ± : Sort ?u.23032} β
{a : Ξ±} β
{motive : (a_1 : Ξ±) β a = a_1 β Sort ?u.23033} β {a_1 : Ξ±} β (t : a = a_1) β motive a (_ : a = a) β motive a_1 tEq.recOn (h_obj: β (X : V), F.obj X = G.obj Xh_obj Y: VY).symm: β {Ξ± : Sort ?u.23058} {a b : Ξ±}, a = b β b = asymm (Eq.recOn: {Ξ± : Sort ?u.23078} β
{a : Ξ±} β
{motive : (a_1 : Ξ±) β a = a_1 β Sort ?u.23079} β {a_1 : Ξ±} β (t : a = a_1) β motive a (_ : a = a) β motive a_1 tEq.recOn (h_obj: β (X : V), F.obj X = G.obj Xh_obj X: VX).symm: β {Ξ± : Sort ?u.23104} {a b : Ξ±}, a = b β b = asymm (G: Prefunctor V WG.map: {V : Type ?u.23121} β
[inst : Quiver V] β
{W : Type ?u.23120} β
[inst_1 : Quiver W] β (self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map f: X βΆ Yf))) : F: Prefunctor V WF = G: Prefunctor V WG := byGoals accomplished! π
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = Gcases' F: Prefunctor V WF with F_obj: ?m.23192 β ?m.23194F_obj _V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WG: Prefunctor V WF_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβ }.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβ }.map f =     Eq.recOn (_ : G.obj Y = { obj := F_obj, map := mapβ }.obj Y)
(Eq.recOn (_ : G.obj X = { obj := F_obj, map := mapβ }.obj X) (G.map f))mk{ obj := F_obj, map := mapβ } = G
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = Gcases' G: Prefunctor V WG with G_obj: ?m.23275 β ?m.23277G_obj _V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)G_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (G_obj X βΆ G_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := G_obj, map := mapβ }.map f))mk.mk{ obj := F_obj, map := mapβΒΉ } = { obj := G_obj, map := mapβ }
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = Gobtain: F_obj = G_objobtain rfl: ?mβrfl : F_obj: ?m.23192 β ?m.23194F_obj = G_obj: ?m.23275 β ?m.23277G_obj := V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)G_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (G_obj X βΆ G_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := G_obj, map := mapβ }.map f))mk.mk{ obj := F_obj, map := mapβΒΉ } = { obj := G_obj, map := mapβ }byGoals accomplished! π
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)G_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (G_obj X βΆ G_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := G_obj, map := mapβ }.map f))F_obj = G_objext X: ?Ξ±XV: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)G_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (G_obj X βΆ G_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := G_obj, map := mapβ }.map f))X: VhF_obj X = G_obj X
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)G_obj: V β Wmapβ: {X Y : V} β (X βΆ Y) β (G_obj X βΆ G_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := G_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := G_obj, map := mapβ }.map f))F_obj = G_objapply h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := G_obj, map := mapβ }.obj Xh_objGoals accomplished! π
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = GcongrV: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ, mapβ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := F_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := F_obj, map := mapβ }.map f))mk.mk.e_mapmapβΒΉ = mapβ
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = Gfunext X: ?Ξ±X Y: ?Ξ±Y f: ?Ξ±fV: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF_obj: V β WmapβΒΉ, mapβ: {X Y : V} β (X βΆ Y) β (F_obj X βΆ F_obj Y)h_obj: β (X : V), { obj := F_obj, map := mapβΒΉ }.obj X = { obj := F_obj, map := mapβ }.obj Xh_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := F_obj, map := mapβ }.map f))X, Y: Vf: X βΆ Ymk.mk.e_map.h.h.hmapβΒΉ f = mapβ f
V: Type uinstβΒΉ: Quiver VW: Type uβinstβ: Quiver WF, G: Prefunctor V Wh_obj: β (X : V), F.obj X = G.obj Xh_map: β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))F = Gsimpa using h_map: β (X Y : V) (f : X βΆ Y),
{ obj := F_obj, map := mapβΒΉ }.map f =     Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj Y = { obj := F_obj, map := mapβΒΉ }.obj Y)
(Eq.recOn (_ : { obj := F_obj, map := mapβ }.obj X = { obj := F_obj, map := mapβΒΉ }.obj X)
({ obj := F_obj, map := mapβ }.map f))h_map X: ?Ξ±X Y: ?Ξ±Y f: ?Ξ±fGoals accomplished! π
#align prefunctor.ext Prefunctor.ext: β {V : Type u} [inst : Quiver V] {W : Type uβ} [inst_1 : Quiver W] {F G : Prefunctor V W}
(h_obj : β (X : V), F.obj X = G.obj X),
(β (X Y : V) (f : X βΆ Y), F.map f = Eq.recOn (_ : G.obj Y = F.obj Y) (Eq.recOn (_ : G.obj X = F.obj X) (G.map f))) β
F = GPrefunctor.ext

/-- The identity morphism between quivers. -/
@[simps: β (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X βΆ Y), (id V).map f = fsimps]
def id: (V : Type u_1) β [inst : Quiver V] β Prefunctor V Vid (V: Type ?u.23954V : Type _: Type (?u.23954+1)Type _) [Quiver: Type ?u.23957 β Type (max?u.23957?u.23958)Quiver V: Type ?u.23954V] : Prefunctor: (V : Type ?u.23962) β
[inst : Quiver V] β
(W : Type ?u.23961) β [inst : Quiver W] β Sort (max(max(max(?u.23962+1)(?u.23961+1))?u.23964)?u.23963)Prefunctor V: Type ?u.23954V V: Type ?u.23954V where
obj := fun X: ?m.23993X => X: ?m.23993X
map f: ?m.24000f := f: ?m.24000f
#align prefunctor.id Prefunctor.id: (V : Type u_1) β [inst : Quiver V] β Prefunctor V VPrefunctor.id
#align prefunctor.id_obj Prefunctor.id_obj: β (V : Type u_1) [inst : Quiver V] (X : V), (id V).obj X = XPrefunctor.id_obj
#align prefunctor.id_map Prefunctor.id_map: β (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X βΆ Y), (id V).map f = fPrefunctor.id_map

instance: (V : Type u_1) β [inst : Quiver V] β Inhabited (Prefunctor V V)instance (V: Type ?u.24133V : Type _: Type (?u.24133+1)Type _) [Quiver: Type ?u.24136 β Type (max?u.24136?u.24137)Quiver V: Type ?u.24133V] : Inhabited: Sort ?u.24140 β Sort (max1?u.24140)Inhabited (Prefunctor: (V : Type ?u.24142) β
[inst : Quiver V] β
(W : Type ?u.24141) β [inst : Quiver W] β Sort (max(max(max(?u.24142+1)(?u.24141+1))?u.24144)?u.24143)Prefunctor V: Type ?u.24133V V: Type ?u.24133V) :=
β¨id: (V : Type ?u.24163) β [inst : Quiver V] β Prefunctor V Vid V: Type ?u.24133Vβ©

/-- Composition of morphisms between quivers. -/
@[simps: β {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
(F : Prefunctor U V) (G : Prefunctor V W) (X : U), (comp F G).obj X = G.obj (F.obj X)simps]
def comp: {U : Type ?u.24207} β
[inst : Quiver U] β
{V : Type ?u.24214} β
[inst_1 : Quiver V] β {W : Type ?u.24221} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp {U: Type ?u.24207U : Type _: Type (?u.24207+1)Type _} [Quiver: Type ?u.24210 β Type (max?u.24210?u.24211)Quiver U: Type ?u.24207U] {V: Type ?u.24214V : Type _: Type (?u.24214+1)Type _} [Quiver: Type ?u.24217 β Type (max?u.24217?u.24218)Quiver V: Type ?u.24214V] {W: Type ?u.24221W : Type _: Type (?u.24221+1)Type _} [Quiver: Type ?u.24224 β Type (max?u.24224?u.24225)Quiver W: Type ?u.24221W]
(F: Prefunctor U VF : Prefunctor: (V : Type ?u.24229) β
[inst : Quiver V] β
(W : Type ?u.24228) β [inst : Quiver W] β Sort (max(max(max(?u.24229+1)(?u.24228+1))?u.24231)?u.24230)Prefunctor U: Type ?u.24207U V: Type ?u.24214V) (G: Prefunctor V WG : Prefunctor: (V : Type ?u.24245) β
[inst : Quiver V] β
(W : Type ?u.24244) β [inst : Quiver W] β Sort (max(max(max(?u.24245+1)(?u.24244+1))?u.24247)?u.24246)Prefunctor V: Type ?u.24214V W: Type ?u.24221W) : Prefunctor: (V : Type ?u.24260) β
[inst : Quiver V] β
(W : Type ?u.24259) β [inst : Quiver W] β Sort (max(max(max(?u.24260+1)(?u.24259+1))?u.24262)?u.24261)Prefunctor U: Type ?u.24207U W: Type ?u.24221W where
obj X: ?m.24298X := G: Prefunctor V WG.obj: {V : Type ?u.24301} β [inst : Quiver V] β {W : Type ?u.24300} β [inst_1 : Quiver W] β Prefunctor V W β V β Wobj (F: Prefunctor U VF.obj: {V : Type ?u.24317} β [inst : Quiver V] β {W : Type ?u.24316} β [inst_1 : Quiver W] β Prefunctor V W β V β Wobj X: ?m.24298X)
map f: ?m.24335f := G: Prefunctor V WG.map: {V : Type ?u.24338} β
[inst : Quiver V] β
{W : Type ?u.24337} β
[inst_1 : Quiver W] β (self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map (F: Prefunctor U VF.map: {V : Type ?u.24362} β
[inst : Quiver V] β
{W : Type ?u.24361} β
[inst_1 : Quiver W] β (self : Prefunctor V W) β {X Y : V} β (X βΆ Y) β (self.obj X βΆ self.obj Y)map f: ?m.24335f)
#align prefunctor.comp Prefunctor.comp: {U : Type u_1} β
[inst : Quiver U] β
{V : Type u_3} β
[inst_1 : Quiver V] β {W : Type u_5} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U WPrefunctor.comp
#align prefunctor.comp_obj Prefunctor.comp_obj: β {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
(F : Prefunctor U V) (G : Prefunctor V W) (X : U), (comp F G).obj X = G.obj (F.obj X)Prefunctor.comp_obj
#align prefunctor.comp_map Prefunctor.comp_map: β {U : Type u_1} [inst : Quiver U] {V : Type u_3} [inst_1 : Quiver V] {W : Type u_5} [inst_2 : Quiver W]
(F : Prefunctor U V) (G : Prefunctor V W) {X Y : U} (f : X βΆ Y), (comp F G).map f = G.map (F.map f)Prefunctor.comp_map

pp_extended_field_notation Prefunctor.comp: {U : Type u_1} β
[inst : Quiver U] β
{V : Type u_3} β
[inst_1 : Quiver V] β {W : Type u_5} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U WPrefunctor.comp

@[simp]
theorem comp_id: β {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), F.comp (id V) = Fcomp_id {U: Type ?u.31803U V: Type ?u.31806V : Type _: Type (?u.31806+1)Type _} [Quiver: Type ?u.31809 β Type (max?u.31809?u.31810)Quiver U: Type ?u.31803U] [Quiver: Type ?u.31813 β Type (max?u.31813?u.31814)Quiver V: Type ?u.31806V] (F: Prefunctor U VF : Prefunctor: (V : Type ?u.31818) β
[inst : Quiver V] β
(W : Type ?u.31817) β [inst : Quiver W] β Sort (max(max(max(?u.31818+1)(?u.31817+1))?u.31820)?u.31819)Prefunctor U: Type ?u.31803U V: Type ?u.31806V) :
F: Prefunctor U VF.comp: {U : Type ?u.31839} β
[inst : Quiver U] β
{V : Type ?u.31837} β
[inst_1 : Quiver V] β {W : Type ?u.31835} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp (id: (V : Type ?u.31861) β [inst : Quiver V] β Prefunctor V Vid _: Type ?u.31861_) = F: Prefunctor U VF := rfl: β {Ξ± : Sort ?u.31887} {a : Ξ±}, a = arfl
#align prefunctor.comp_id Prefunctor.comp_id: β {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), F.comp (id V) = FPrefunctor.comp_id

@[simp]
theorem id_comp: β {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), (id U).comp F = Fid_comp {U: Type u_1U V: Type ?u.31930V : Type _: Type (?u.31930+1)Type _} [Quiver: Type ?u.31933 β Type (max?u.31933?u.31934)Quiver U: Type ?u.31927U] [Quiver: Type ?u.31937 β Type (max?u.31937?u.31938)Quiver V: Type ?u.31930V] (F: Prefunctor U VF : Prefunctor: (V : Type ?u.31942) β
[inst : Quiver V] β
(W : Type ?u.31941) β [inst : Quiver W] β Sort (max(max(max(?u.31942+1)(?u.31941+1))?u.31944)?u.31943)Prefunctor U: Type ?u.31927U V: Type ?u.31930V) :
(id: (V : Type ?u.31959) β [inst : Quiver V] β Prefunctor V Vid _: Type ?u.31959_).comp: {U : Type ?u.31969} β
[inst : Quiver U] β
{V : Type ?u.31967} β
[inst_1 : Quiver V] β {W : Type ?u.31965} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp F: Prefunctor U VF = F: Prefunctor U VF := rfl: β {Ξ± : Sort ?u.32011} {a : Ξ±}, a = arfl
#align prefunctor.id_comp Prefunctor.id_comp: β {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : Prefunctor U V), (id U).comp F = FPrefunctor.id_comp

@[simp]
theorem comp_assoc: β {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
[inst_3 : Quiver Z] (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z),
(F.comp G).comp H = F.comp (G.comp H)comp_assoc {U: Type ?u.32055U V: Type ?u.32058V W: Type ?u.32061W Z: Type ?u.32064Z : Type _: Type (?u.32055+1)Type _} [Quiver: Type ?u.32067 β Type (max?u.32067?u.32068)Quiver U: Type ?u.32055U] [Quiver: Type ?u.32071 β Type (max?u.32071?u.32072)Quiver V: Type ?u.32058V] [Quiver: Type ?u.32075 β Type (max?u.32075?u.32076)Quiver W: Type ?u.32061W] [Quiver: Type ?u.32079 β Type (max?u.32079?u.32080)Quiver Z: Type ?u.32064Z]
(F: Prefunctor U VF : Prefunctor: (V : Type ?u.32084) β
[inst : Quiver V] β
(W : Type ?u.32083) β [inst : Quiver W] β Sort (max(max(max(?u.32084+1)(?u.32083+1))?u.32086)?u.32085)Prefunctor U: Type ?u.32055U V: Type ?u.32058V) (G: Prefunctor V WG : Prefunctor: (V : Type ?u.32100) β
[inst : Quiver V] β
(W : Type ?u.32099) β [inst : Quiver W] β Sort (max(max(max(?u.32100+1)(?u.32099+1))?u.32102)?u.32101)Prefunctor V: Type ?u.32058V W: Type ?u.32061W) (H: Prefunctor W ZH : Prefunctor: (V : Type ?u.32115) β
[inst : Quiver V] β
(W : Type ?u.32114) β [inst : Quiver W] β Sort (max(max(max(?u.32115+1)(?u.32114+1))?u.32117)?u.32116)Prefunctor W: Type ?u.32061W Z: Type ?u.32064Z) :
(F: Prefunctor U VF.comp: {U : Type ?u.32135} β
[inst : Quiver U] β
{V : Type ?u.32133} β
[inst_1 : Quiver V] β {W : Type ?u.32131} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp G: Prefunctor V WG).comp: {U : Type ?u.32176} β
[inst : Quiver U] β
{V : Type ?u.32174} β
[inst_1 : Quiver V] β {W : Type ?u.32172} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp H: Prefunctor W ZH = F: Prefunctor U VF.comp: {U : Type ?u.32213} β
[inst : Quiver U] β
{V : Type ?u.32211} β
[inst_1 : Quiver V] β {W : Type ?u.32209} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp (G: Prefunctor V WG.comp: {U : Type ?u.32235} β
[inst : Quiver U] β
{V : Type ?u.32233} β
[inst_1 : Quiver V] β {W : Type ?u.32231} β [inst_2 : Quiver W] β Prefunctor U V β Prefunctor V W β Prefunctor U Wcomp H: Prefunctor W ZH) :=
rfl: β {Ξ± : Sort ?u.32285} {a : Ξ±}, a = arfl
#align prefunctor.comp_assoc Prefunctor.comp_assoc: β {U : Type u_1} {V : Type u_2} {W : Type u_3} {Z : Type u_4} [inst : Quiver U] [inst_1 : Quiver V] [inst_2 : Quiver W]
[inst_3 : Quiver Z] (F : Prefunctor U V) (G : Prefunctor V W) (H : Prefunctor W Z),
(F.comp G).comp H = F.comp (G.comp H)Prefunctor.comp_assoc

/-- Notation for a prefunctor between quivers. -/
infixl:50 " β₯€q " => Prefunctor: (V : Type uβ) β [inst : Quiver V] β (W : Type uβ) β [inst : Quiver W] β Sort (max(max(max(uβ+1)(uβ+1))vβ)vβ)Prefunctor

/-- Notation for composition of prefunctors. -/
infixl:60 " βq " => Prefunctor.comp: {U : Type u_1} β
[inst : Quiver U] β
{V : Type u_3} β [inst_1 : Quiver V] β {W : Type u_5} β [inst_2 : Quiver W] β U β₯€q V β V β₯€q W β U β₯€q WPrefunctor.comp

/-- Notation for the identity prefunctor on a quiver. -/
notation "π­q" => id: (V : Type u_1) β [inst : Quiver V] β V β₯€q Vid

end Prefunctor

namespace Quiver

/-- `Vα΅α΅` reverses the direction of all arrows of `V`. -/
instance opposite: {V : Type ?u.54166} β [inst : Quiver V] β Quiver Vα΅α΅opposite {V: ?m.54163V} [Quiver: Type ?u.54166 β Type (max?u.54166?u.54167)Quiver V: ?m.54163V] : Quiver: Type ?u.54170 β Type (max?u.54170?u.54171)Quiver V: ?m.54163Vα΅α΅ :=
β¨fun a: ?m.54183a b: ?m.54186b => (unop: {Ξ± : Sort ?u.54195} β Ξ±α΅α΅ β Ξ±unop b: ?m.54186b βΆ unop: {Ξ± : Sort ?u.54199} β Ξ±α΅α΅ β Ξ±unop a: ?m.54183a)α΅α΅β©
#align quiver.opposite Quiver.opposite: {V : Type u_1} β [inst : Quiver V] β Quiver Vα΅α΅Quiver.opposite

/-- The opposite of an arrow in `V`.
-/
def Hom.op: {V : Type ?u.54258} β [inst : Quiver V] β {X Y : V} β (X βΆ Y) β (Opposite.op Y βΆ Opposite.op X)Hom.op {V: ?m.54255V} [Quiver: Type ?u.54258 β Type (max?u.54258?u.54259)Quiver V: ?m.54255V] {X: VX Y: VY : V: ?m.54255V} (f: X βΆ Yf : X: VX βΆ Y: VY) : op: {Ξ± : Sort ?u.54288} β Ξ± β Ξ±α΅α΅op Y: VY βΆ op: {Ξ± : Sort ?u.54291} β Ξ± β Ξ±α΅α΅op X: VX := β¨f: X βΆ Yfβ©
#align quiver.hom.op Quiver.Hom.op: {V : Type u_1} β [inst : Quiver V] β {X Y : V} β (X βΆ Y) β (op Y βΆ op X)Quiver.Hom.op

pp_extended_field_notation Quiver.Hom.op: {V : Type u_1} β [inst : Quiver V] β {X Y : V} β (X βΆ Y) β (op Y βΆ op X)Quiver.Hom.op

/-- Given an arrow in `Vα΅α΅`, we can take the "unopposite" back in `V`.
-/
def Hom.unop: {V : Type u_1} β [inst : Quiver V] β {X Y : Vα΅α΅} β (X βΆ Y) β (Y.unop βΆ X.unop)Hom.unop {V: ?m.57901V} [Quiver: Type ?u.57904 β Type (max?u.57904?u.57905)Quiver V: ?m.57901V] {X: Vα΅α΅X Y: Vα΅α΅Y : V: ?m.57901Vα΅α΅} (f: X βΆ Yf : X: Vα΅α΅X βΆ Y: Vα΅α΅Y) : unop: {Ξ± : Sort ?u.57946} β Ξ±α΅α΅ β Ξ±unop Y: Vα΅α΅Y βΆ unop: {Ξ± : Sort ?u.57949} β Ξ±α΅α΅ β Ξ±unop X: Vα΅α΅X := Opposite.unop: {Ξ± : Sort ?u.57965} β Ξ±α΅α΅ β Ξ±Opposite.unop f: X βΆ Yf
#align quiver.hom.unop Quiver.Hom.unop: {V : Type u_1} β [inst : Quiver V] β {X Y : Vα΅α΅} β (X βΆ Y) β (Y.unop βΆ X.unop)Quiver.Hom.unop

pp_extended_field_notation Quiver.Hom.unop: {V : Type u_1} β [inst : Quiver V] β {X Y : Vα΅α΅} β (X βΆ Y) β (Y.unop βΆ X.unop)Quiver.Hom.unop

/-- A type synonym for a quiver with no arrows. -/
-- Porting note: no has_nonempty_instance linter yet
-- @[nolint has_nonempty_instance]
def Empty: Type u β Type uEmpty (V: Type uV : Type u: Type (u+1)Type u) : Type u: Type (u+1)Type u := V: Type uV
#align quiver.empty Quiver.Empty: Type u β Type uQuiver.Empty

instance emptyQuiver: (V : Type u) β Quiver (Empty V)emptyQuiver (V: Type uV : Type u: Type (u+1)Type u) : Quiver: Type ?u.61563 β Type (max?u.61563u)Quiver.{u} (Empty: Type ?u.61564 β Type ?u.61564Empty V: Type uV) := β¨fun _: ?m.61574_ _: ?m.61577_ => PEmpty: Sort ?u.61579PEmptyβ©
#align quiver.empty_quiver Quiver.emptyQuiver: (V : Type u) β Quiver (Empty V)Quiver.emptyQuiver

@[simp]
theorem empty_arrow: β {V : Type u} (a b : Empty V), (a βΆ b) = PEmptyempty_arrow {V: Type uV : Type u: Type (u+1)Type u} (a: Empty Va b: Empty Vb : Empty: Type ?u.61630 β Type ?u.61630Empty V: Type uV) : (a: Empty Va βΆ b: Empty Vb) = PEmpty: Sort ?u.61646PEmpty := rfl: β {Ξ± : Sort ?u.61670} {a : Ξ±}, a = arfl
#align quiver.empty_arrow Quiver.empty_arrow: β {V : Type u} (a b : Empty V), (a βΆ b) = PEmptyQuiver.empty_arrow

/-- A quiver is thin if it has no parallel arrows. -/
@[reducible]
def IsThin: (V : Type u) β [inst : Quiver V] β PropIsThin (V: Type uV : Type u: Type (u+1)Type u) [Quiver: Type ?u.61693 β Type (max?u.61693?u.61694)Quiver V: Type uV] : Prop: TypeProp := β a: Va b: Vb : V: Type uV, Subsingleton: Sort ?u.61705 β PropSubsingleton (a: Va βΆ b: Vb)
#align quiver.is_thin Quiver.IsThin: (V : Type u) β [inst : Quiver V] β PropQuiver.IsThin

end Quiver
```