class LeanPool.Polylean.Quiver (V : Sort u) : Sort (max u (v + 1))

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.

It is a common generalisation of multigraphs and categories. This definition is taken from mathlib: https://leanprover-community.github.io/mathlib_docs/combinatorics/quiver/basic.html#quiver.

• hom : V → V → Sort v

  The type of arrows from one vertex to another.

def LeanPool.Polylean.«term_⟶_» : Lean.TrailingParserDescr

Arrow notation for the hom type of a quiver.

Equations

• LeanPool.Polylean.«term_⟶_» = Lean.ParserDescr.trailingNode `LeanPool.Polylean.«term_⟶_» 10 11 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶ ") (Lean.ParserDescr.cat `term 10))

structure LeanPool.Polylean.Quiver.PreFunctor {V : Sort u_1} {V' : Sort u_2} (Q : Quiver V) (Q' : Quiver V') : Sort (max (max (max (max 1 u_1) u_2) u_3) u_4)

A pre-functor is a morphism of quivers.

• obj : V → V'

  The map on vertices.

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

  The map on arrows.

def LeanPool.Polylean.Quiver.PreFunctor.id (V : Sort u_1) [Q : Quiver V] : Q.PreFunctor Q

The identity morphism between quivers.

Equations

• LeanPool.Polylean.Quiver.PreFunctor.id V = { obj := id, map := fun {X Y : V} => id }

@[implicit_reducible]

instance LeanPool.Polylean.Quiver.PreFunctor.instInhabited (V : Sort u_1) [Q : Quiver V] : Inhabited (Q.PreFunctor Q)

Equations

• LeanPool.Polylean.Quiver.PreFunctor.instInhabited V = { default := LeanPool.Polylean.Quiver.PreFunctor.id V }

def LeanPool.Polylean.Quiver.PreFunctor.comp {U : Sort u_1} {V : Sort u_2} {W : Sort u_3} {QU : Quiver U} {QV : Quiver V} {QW : Quiver W} (F : QU.PreFunctor QV) (G : QV.PreFunctor QW) : QU.PreFunctor QW

Composition of morphisms between quivers.

Equations

• F.comp G = { obj := G.obj ∘ F.obj, map := fun {X Y : U} => G.map ∘ F.map }

inductive LeanPool.Polylean.Path {V : Sort u_1} [Quiver V] : V → V → Sort (max (max 1 u_1) u_2)

Paths in a quiver.

• nil {V : Sort u_1} [Quiver V] {A : V} : Path A A
• cons {V : Sort u_1} [Quiver V] {A B C : V} : (A ⟶ B) → Path B C → Path A C

def LeanPool.Polylean.Quiver.toPath {V : Sort u_1} [Quiver V] {A B : V} (e : A ⟶ B) : Path A B

Convert a single quiver arrow to a path.

Equations

• LeanPool.Polylean.Quiver.toPath e = LeanPool.Polylean.Path.cons e LeanPool.Polylean.Path.nil

@[reducible, match_pattern, inline]

abbrev LeanPool.Polylean.Path.nil' {V : Sort u_1} [Quiver V] (A : V) : Path A A

The empty path at a vertex, with its vertex explicit for pattern matching.

Equations

• LeanPool.Polylean.Path.nil' A = LeanPool.Polylean.Path.nil

@[reducible, match_pattern, inline]

abbrev LeanPool.Polylean.Path.cons' {V : Sort u_1} [Quiver V] (A B C : V) : (A ⟶ B) → Path B C → Path A C

A path formed by adding an edge to the front, with endpoints explicit for matching.

Equations

• LeanPool.Polylean.Path.cons' A B C = LeanPool.Polylean.Path.cons

@[reducible, match_pattern, inline]

abbrev LeanPool.Polylean.Path.snoc {V : Sort u_1} [Quiver V] {A B C : V} : Path A B → (B ⟶ C) → Path A C

Concatenate an edge to the end of a path.

Equations

• LeanPool.Polylean.Path.nil.snoc x✝ = LeanPool.Polylean.Path.cons x✝ LeanPool.Polylean.Path.nil
• (LeanPool.Polylean.Path.cons e p').snoc x✝ = LeanPool.Polylean.Path.cons e (p'.snoc x✝)

@[reducible, match_pattern, inline]

abbrev LeanPool.Polylean.Path.snoc' {V : Sort u_1} [Quiver V] (A B C : V) : Path A B → (B ⟶ C) → Path A C

Append an edge to the end of a path, with endpoints explicit for matching.

Equations

• LeanPool.Polylean.Path.snoc' A B C = LeanPool.Polylean.Path.snoc

def LeanPool.Polylean.Path.append {V : Sort u_1} [Quiver V] {A B C : V} : Path A B → Path B C → Path A C

Concatenation of paths.

Equations

• LeanPool.Polylean.Path.nil.append x✝ = x✝
• (LeanPool.Polylean.Path.cons e p').append x✝ = LeanPool.Polylean.Path.cons e (p'.append x✝)

def LeanPool.Polylean.Path.length {V : Sort u_1} [Quiver V] {A B : V} : Path A B → Nat

The length of a path.

Equations

• LeanPool.Polylean.Path.nil.length = Nat.zero
• (LeanPool.Polylean.Path.cons a p).length = p.length.succ

@[simp]

theorem LeanPool.Polylean.Path.nil_append {V : Sort u_1} [Quiver V] {A B : V} (p : Path A B) : nil.append p = p

@[simp]

theorem LeanPool.Polylean.Path.append_nil {V : Sort u_1} [Quiver V] {A B : V} (p : Path A B) : p.append nil = p

theorem LeanPool.Polylean.Path.snoc_cons {V : Sort u_1} [Quiver V] {A B C D : V} (e : A ⟶ B) (p : Path B C) (e' : C ⟶ D) : (cons e p).snoc e' = cons e (p.snoc e')

theorem LeanPool.Polylean.Path.append_snoc {V : Sort u_1} [Quiver V] {A B C D : V} (p : Path A B) (p' : Path B C) (e : C ⟶ D) : p.append (p'.snoc e) = (p.append p').snoc e

theorem LeanPool.Polylean.Path.append_cons {V : Sort u_1} [Quiver V] {A B C D : V} (p : Path A B) (e : B ⟶ C) (p' : Path C D) : p.append (cons e p') = (p.snoc e).append p'

theorem LeanPool.Polylean.Path.append_assoc {V : Sort u_1} [Quiver V] {A B C D : V} (p : Path A B) (q : Path B C) (r : Path C D) : (p.append q).append r = p.append (q.append r)

theorem LeanPool.Polylean.Path.nil_length {V : Sort u_1} [Quiver V] {A : V} (p : Path A A) : p.length = Nat.zero ↔ p = nil' A

theorem LeanPool.Polylean.Path.snoc_length {V : Sort u_1} [Quiver V] {A B C : V} (p : Path A B) (e : B ⟶ C) : (p.snoc e).length = p.length.succ

theorem LeanPool.Polylean.Path.length_append {V : Sort u_1} [Quiver V] {A B C : V} (p : Path A B) (q : Path B C) : (p.append q).length = p.length + q.length

def LeanPool.Polylean.Path.first {V : Sort u_1} [Quiver V] {A B : V} : Path A B → V

The end-point of the first edge in the path.

Equations

• LeanPool.Polylean.Path.nil.first = B
• (LeanPool.Polylean.Path.cons a a_1).first = v

def LeanPool.Polylean.Path.last {V : Sort u_1} [Quiver V] {A B : V} : Path A B → V

The source of the last end in the path.

Equations

• LeanPool.Polylean.Path.nil.last = x✝
• (LeanPool.Polylean.Path.cons a LeanPool.Polylean.Path.nil).last = x✝¹
• (LeanPool.Polylean.Path.cons a (LeanPool.Polylean.Path.cons e p)).last = (LeanPool.Polylean.Path.cons e p).last

theorem LeanPool.Polylean.Path.first_cons {V : Sort u_1} [Quiver V] (A B C : V) (e : A ⟶ B) (p : Path B C) : (cons e p).first = B

theorem LeanPool.Polylean.Path.last_snoc {V : Sort u_1} [Quiver V] (A B C : V) (p : Path A B) (e : B ⟶ C) : (p.snoc e).last = B

@[reducible, inline]

abbrev LeanPool.Polylean.Loop {V : Sort u_1} [Quiver V] (A : V) : Sort (max (max 1 u_1) u_2)

A loop is a path whose source and target are the same vertex.

Equations

• LeanPool.Polylean.Loop A = LeanPool.Polylean.Path A A

def LeanPool.Polylean.Loop.toPath {V : Sort u_1} [Quiver V] (A : V) : Loop A → Path A A

Regard a loop as a path.

Equations

• LeanPool.Polylean.Loop.toPath A = id

@[reducible, inline]

abbrev LeanPool.Polylean.Loop.nil {V : Sort u_1} [Quiver V] (A : V) : Loop A

The empty loop.

Equations

• LeanPool.Polylean.Loop.nil A = LeanPool.Polylean.Path.nil

@[reducible, inline]

abbrev LeanPool.Polylean.Loop.next {V : Sort u_1} [Quiver V] (A : V) : Loop A → V

The next vertex reached by the first edge of a loop.

Equations

• LeanPool.Polylean.Loop.next A = LeanPool.Polylean.Path.first

@[reducible, inline]

abbrev LeanPool.Polylean.Loop.concat {V : Sort u_1} [Quiver V] (A : V) : Loop A → Loop A → Loop A

Concatenate two loops.

Equations

• LeanPool.Polylean.Loop.concat A = LeanPool.Polylean.Path.append