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.
/-
Copyright (c) 2021 David Wärn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Wärn, Scott Morrison
Ported by: Scott Morrison

! This file was ported from Lean 3 source module combinatorics.quiver.basic
! leanprover-community/mathlib commit 56adee5b5eef9e734d82272918300fca4f3e7cef
! 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 V
Quiver
(
V: Type u
V
:
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 v
Hom
:
V: Type u
V
→
V: Type u
V
→
Sort v: Type v
Sort
Sort 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 v
Quiver.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 v
Quiver.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 W
Prefunctor
(
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 → W
obj
:
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: V
X
Y: V
Y
:
V: Type u₁
V
}, (
X: V
X
⟶
Y: V
Y
) → (
obj: V → W
obj
X: V
X
⟶
obj: V → W
obj
Y: V
Y
) #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 → W
Prefunctor.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 = G
ext
{
V: Type u
V
:
Type u: Type (u+1)
Type u
} [
Quiver: Type ?u.22889 → Type (max?u.22889v₁)
Quiver
.{v₁}
V: Type u
V
] {
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 W
F
G: Prefunctor V W
G
:
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 u
V
W: Type u₂
W
} (
h_obj: ∀ (X : V), F.obj X = G.obj X
h_obj
: ∀
X: ?m.22928
X
,
F: Prefunctor V W
F
.
obj: {V : Type ?u.22933} → [inst : Quiver V] → {W : Type ?u.22932} → [inst_1 : Quiver W] → Prefunctor V W → V → W
obj
X: ?m.22928
X
=
G: Prefunctor V W
G
.
obj: {V : Type ?u.22951} → [inst : Quiver V] → {W : Type ?u.22950} → [inst_1 : Quiver W] → Prefunctor V W → V → W
obj
X: ?m.22928
X
) (
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: V
X
Y: V
Y
:
V: Type u
V
) (
f: X ⟶ Y
f
:
X: V
X
⟶
Y: V
Y
),
F: Prefunctor V W
F
.
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 ⟶ Y
f
=
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 t
Eq.recOn
(
h_obj: ∀ (X : V), F.obj X = G.obj X
h_obj
Y: V
Y
).
symm: ∀ {α : Sort ?u.23058} {a b : α}, a = b → b = a
symm
(
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 t
Eq.recOn
(
h_obj: ∀ (X : V), F.obj X = G.obj X
h_obj
X: V
X
).
symm: ∀ {α : Sort ?u.23104} {a b : α}, a = b → b = a
symm
(
G: Prefunctor V W
G
.
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 ⟶ Y
f
))) :
F: Prefunctor V W
F
=
G: Prefunctor V W
G
:=

Goals accomplished! 🐙
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

G: Prefunctor V W

F_obj: V → W

map✝: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

h_obj: ∀ (X : V), { obj := F_obj, map := map✝ }.obj X = G.obj X

h_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 u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

G_obj: V → W

map✝: {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 X

h_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 u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

G_obj: V → W

map✝: {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 X

h_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✝ }

Goals accomplished! 🐙
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

G_obj: V → W

map✝: {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 X

h_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_obj
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

G_obj: V → W

map✝: {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 X

h_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: V


h
F_obj X = G_obj X
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹: {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)

G_obj: V → W

map✝: {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 X

h_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_obj

Goals accomplished! 🐙
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹, 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 X

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


mk.mk.e_map
map✝¹ = map✝
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F_obj: V → W

map✝¹, 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 X

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

X, Y: V

f: X ⟶ Y


mk.mk.e_map.h.h.h
map✝¹ f = map✝ f
V: Type u

inst✝¹: Quiver V

W: Type u₂

inst✝: Quiver W

F, G: Prefunctor V W

h_obj: ∀ (X : V), F.obj X = G.obj X

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


F = G

Goals 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 = G
Prefunctor.ext
/-- The identity morphism between quivers. -/ @[
simps: ∀ (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X ⟶ Y), (id V).map f = f
simps
] def
id: (V : Type u_1) → [inst : Quiver V] → Prefunctor V V
id
(
V: Type ?u.23954
V
:
Type _: Type (?u.23954+1)
Type _
) [
Quiver: Type ?u.23957 → Type (max?u.23957?u.23958)
Quiver
V: Type ?u.23954
V
] :
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.23954
V
V: Type ?u.23954
V
where obj := fun
X: ?m.23993
X
=>
X: ?m.23993
X
map
f: ?m.24000
f
:=
f: ?m.24000
f
#align prefunctor.id
Prefunctor.id: (V : Type u_1) → [inst : Quiver V] → Prefunctor V V
Prefunctor.id
#align prefunctor.id_obj
Prefunctor.id_obj: ∀ (V : Type u_1) [inst : Quiver V] (X : V), (id V).obj X = X
Prefunctor.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 = f
Prefunctor.id_map
instance: (V : Type u_1) → [inst : Quiver V] → Inhabited (Prefunctor V V)
instance
(
V: Type ?u.24133
V
:
Type _: Type (?u.24133+1)
Type _
) [
Quiver: Type ?u.24136 → Type (max?u.24136?u.24137)
Quiver
V: Type ?u.24133
V
] :
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.24133
V
V: Type ?u.24133
V
) := ⟨
id: (V : Type ?u.24163) → [inst : Quiver V] → Prefunctor V V
id
V: Type ?u.24133
V
⟩ /-- 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 W
comp
{
U: Type ?u.24207
U
:
Type _: Type (?u.24207+1)
Type _
} [
Quiver: Type ?u.24210 → Type (max?u.24210?u.24211)
Quiver
U: Type ?u.24207
U
] {
V: Type ?u.24214
V
:
Type _: Type (?u.24214+1)
Type _
} [
Quiver: Type ?u.24217 → Type (max?u.24217?u.24218)
Quiver
V: Type ?u.24214
V
] {
W: Type ?u.24221
W
:
Type _: Type (?u.24221+1)
Type _
} [
Quiver: Type ?u.24224 → Type (max?u.24224?u.24225)
Quiver
W: Type ?u.24221
W
] (
F: Prefunctor U V
F
:
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.24207
U
V: Type ?u.24214
V
) (
G: Prefunctor V W
G
:
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.24214
V
W: Type ?u.24221
W
) :
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.24207
U
W: Type ?u.24221
W
where obj
X: ?m.24298
X
:=
G: Prefunctor V W
G
.
obj: {V : Type ?u.24301} → [inst : Quiver V] → {W : Type ?u.24300} → [inst_1 : Quiver W] → Prefunctor V W → V → W
obj
(
F: Prefunctor U V
F
.
obj: {V : Type ?u.24317} → [inst : Quiver V] → {W : Type ?u.24316} → [inst_1 : Quiver W] → Prefunctor V W → V → W
obj
X: ?m.24298
X
) map
f: ?m.24335
f
:=
G: Prefunctor V W
G
.
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 V
F
.
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.24335
f
) #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 W
Prefunctor.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 W
Prefunctor.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) = F
comp_id
{
U: Type ?u.31803
U
V: Type ?u.31806
V
:
Type _: Type (?u.31806+1)
Type _
} [
Quiver: Type ?u.31809 → Type (max?u.31809?u.31810)
Quiver
U: Type ?u.31803
U
] [
Quiver: Type ?u.31813 → Type (max?u.31813?u.31814)
Quiver
V: Type ?u.31806
V
] (
F: Prefunctor U V
F
:
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.31803
U
V: Type ?u.31806
V
) :
F: Prefunctor U V
F
.
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 W
comp
(
id: (V : Type ?u.31861) → [inst : Quiver V] → Prefunctor V V
id
_: Type ?u.31861
_
) =
F: Prefunctor U V
F
:=
rfl: ∀ {α : Sort ?u.31887} {a : α}, a = a
rfl
#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) = F
Prefunctor.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 = F
id_comp
{
U: Type u_1
U
V: Type ?u.31930
V
:
Type _: Type (?u.31930+1)
Type _
} [
Quiver: Type ?u.31933 → Type (max?u.31933?u.31934)
Quiver
U: Type ?u.31927
U
] [
Quiver: Type ?u.31937 → Type (max?u.31937?u.31938)
Quiver
V: Type ?u.31930
V
] (
F: Prefunctor U V
F
:
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.31927
U
V: Type ?u.31930
V
) : (
id: (V : Type ?u.31959) → [inst : Quiver V] → Prefunctor V V
id
_: 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 W
comp
F: Prefunctor U V
F
=
F: Prefunctor U V
F
:=
rfl: ∀ {α : Sort ?u.32011} {a : α}, a = a
rfl
#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 = F
Prefunctor.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.32055
U
V: Type ?u.32058
V
W: Type ?u.32061
W
Z: Type ?u.32064
Z
:
Type _: Type (?u.32055+1)
Type _
} [
Quiver: Type ?u.32067 → Type (max?u.32067?u.32068)
Quiver
U: Type ?u.32055
U
] [
Quiver: Type ?u.32071 → Type (max?u.32071?u.32072)
Quiver
V: Type ?u.32058
V
] [
Quiver: Type ?u.32075 → Type (max?u.32075?u.32076)
Quiver
W: Type ?u.32061
W
] [
Quiver: Type ?u.32079 → Type (max?u.32079?u.32080)
Quiver
Z: Type ?u.32064
Z
] (
F: Prefunctor U V
F
:
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.32055
U
V: Type ?u.32058
V
) (
G: Prefunctor V W
G
:
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.32058
V
W: Type ?u.32061
W
) (
H: Prefunctor W Z
H
:
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.32061
W
Z: Type ?u.32064
Z
) : (
F: Prefunctor U V
F
.
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 W
comp
G: Prefunctor V W
G
).
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 W
comp
H: Prefunctor W Z
H
=
F: Prefunctor U V
F
.
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 W
comp
(
G: Prefunctor V W
G
.
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 W
comp
H: Prefunctor W Z
H
) :=
rfl: ∀ {α : Sort ?u.32285} {a : α}, a = a
rfl
#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 W
Prefunctor.comp
/-- Notation for the identity prefunctor on a quiver. -/ notation "𝟭q" =>
id: (V : Type u_1) → [inst : Quiver V] → V ⥤q V
id
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.54163
V
} [
Quiver: Type ?u.54166 → Type (max?u.54166?u.54167)
Quiver
V: ?m.54163
V
] :
Quiver: Type ?u.54170 → Type (max?u.54170?u.54171)
Quiver
V: ?m.54163
V
ᵒᵖ := ⟨fun
a: ?m.54183
a
b: ?m.54186
b
=> (
unop: {α : Sort ?u.54195} → αᵒᵖ → α
unop
b: ?m.54186
b
⟶
unop: {α : Sort ?u.54199} → αᵒᵖ → α
unop
a: ?m.54183
a
)ᵒᵖ⟩ #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.54255
V
} [
Quiver: Type ?u.54258 → Type (max?u.54258?u.54259)
Quiver
V: ?m.54255
V
] {
X: V
X
Y: V
Y
:
V: ?m.54255
V
} (
f: X ⟶ Y
f
:
X: V
X
⟶
Y: V
Y
) :
op: {α : Sort ?u.54288} → α → αᵒᵖ
op
Y: V
Y
⟶
op: {α : Sort ?u.54291} → α → αᵒᵖ
op
X: V
X
:= ⟨
f: X ⟶ Y
f
⟩ #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.57901
V
} [
Quiver: Type ?u.57904 → Type (max?u.57904?u.57905)
Quiver
V: ?m.57901
V
] {X Y :
V: ?m.57901
V
ᵒᵖ} (
f: X ⟶ Y
f
: X ⟶ Y) :
unop: {α : Sort ?u.57946} → αᵒᵖ → α
unop
Y ⟶
unop: {α : Sort ?u.57949} → αᵒᵖ → α
unop
X :=
Opposite.unop: {α : Sort ?u.57965} → αᵒᵖ → α
Opposite.unop
f: X ⟶ Y
f
#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 u
Empty
(
V: Type u
V
:
Type u: Type (u+1)
Type u
) :
Type u: Type (u+1)
Type u
:=
V: Type u
V
#align quiver.empty
Quiver.Empty: Type u → Type u
Quiver.Empty
instance
emptyQuiver: (V : Type u) → Quiver (Empty V)
emptyQuiver
(
V: Type u
V
:
Type u: Type (u+1)
Type u
) :
Quiver: Type ?u.61563 → Type (max?u.61563u)
Quiver
.{u} (
Empty: Type ?u.61564 → Type ?u.61564
Empty
V: Type u
V
) := ⟨fun
_: ?m.61574
_
_: ?m.61577
_
=>
PEmpty: Sort ?u.61579
PEmpty
⟩ #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) = PEmpty
empty_arrow
{
V: Type u
V
:
Type u: Type (u+1)
Type u
} (
a: Empty V
a
b: Empty V
b
:
Empty: Type ?u.61630 → Type ?u.61630
Empty
V: Type u
V
) : (
a: Empty V
a
⟶
b: Empty V
b
) =
PEmpty: Sort ?u.61646
PEmpty
:=
rfl: ∀ {α : Sort ?u.61670} {a : α}, a = a
rfl
#align quiver.empty_arrow
Quiver.empty_arrow: ∀ {V : Type u} (a b : Empty V), (a ⟶ b) = PEmpty
Quiver.empty_arrow
/-- A quiver is thin if it has no parallel arrows. -/ @[reducible] def
IsThin: (V : Type u) → [inst : Quiver V] → Prop
IsThin
(
V: Type u
V
:
Type u: Type (u+1)
Type u
) [
Quiver: Type ?u.61693 → Type (max?u.61693?u.61694)
Quiver
V: Type u
V
] :
Prop: Type
Prop
:= ∀
a: V
a
b: V
b
:
V: Type u
V
,
Subsingleton: Sort ?u.61705 → Prop
Subsingleton
(
a: V
a
⟶
b: V
b
) #align quiver.is_thin
Quiver.IsThin: (V : Type u) → [inst : Quiver V] → Prop
Quiver.IsThin
end Quiver