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 generalization of Digraph V, which can be thought of as "a proposition a ⟶ b of arrows".

class Quiver (V : Type u) : Type (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. This is hence a form of directed multigraphs.

For graphs with no repeated edges, one can either use Quiver.IsThin to demand that the hom sets are subsingletons, or Digraph V (where the hom sets are Prop-valued).

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.

• Hom : V → V → Type v

  The type of edges/arrows/morphisms between a given source and target.

def «term_⟶_» : Lean.TrailingParserDescr

Notation for the type of edges/arrows/morphisms between a given source and target in a quiver or category.

Equations

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

instance Quiver.opposite {V : Type u_1} [Quiver V] : Quiver Vᵒᵖ

Vᵒᵖ reverses the direction of all arrows of V.

Equations

• Quiver.opposite = { Hom := fun (a b : Vᵒᵖ) => (Opposite.unop b ⟶ Opposite.unop a)ᵒᵖ }

def Quiver.Hom.op {V : Type u_1} [Quiver V] {X Y : V} (f : X ⟶ Y) : Opposite.op Y ⟶ Opposite.op X

The opposite of an arrow in V.

Equations

• f.op = Opposite.op f

def Quiver.Hom.unop {V : Type u_1} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : Opposite.unop Y ⟶ Opposite.unop X

Given an arrow in Vᵒᵖ, we can take the "unopposite" back in V.

Equations

• f.unop = Opposite.unop f

def Quiver.Hom.opEquiv {V : Type u_1} [Quiver V] {X Y : V} : (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X)

The bijection (X ⟶ Y) ≃ (op Y ⟶ op X).

Equations

• Quiver.Hom.opEquiv = { toFun := Opposite.op, invFun := Opposite.unop, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Quiver.Hom.opEquiv_apply {V : Type u_1} [Quiver V] {X Y : V} (unop : X ⟶ Y) : opEquiv unop = Opposite.op unop

@[simp]

theorem Quiver.Hom.opEquiv_symm_apply {V : Type u_1} [Quiver V] {X Y : V} (self : (Opposite.unop (Opposite.op X) ⟶ Opposite.unop (Opposite.op Y))ᵒᵖ) : opEquiv.symm self = Opposite.unop self

def Quiver.Empty (V : Type u) : Type u

A type synonym for a quiver with no arrows.

Equations

• Quiver.Empty V = V

instance Quiver.emptyQuiver (V : Type u) : Quiver (Empty V)

Equations

• Quiver.emptyQuiver V = { Hom := fun (x x_1 : Quiver.Empty V) => PEmpty.{?u.9 + 1} }

@[simp]

theorem Quiver.empty_arrow {V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty.{u + 1}

@[reducible, inline]

abbrev Quiver.IsThin (V : Type u) [Quiver V] : Prop

A quiver is thin if it has no parallel arrows.

Equations

• Quiver.IsThin V = ∀ (a b : V), Subsingleton (a ⟶ b)

@[reducible, inline]

abbrev Quiver.IsThin' (V : Type u) [Quiver V] : Prop

isThin' is equivalent to IsThin. It is used by @[to_dual] to be able to translate IsThin.

Equations

• Quiver.IsThin' V = ∀ (a b : V), Subsingleton (b ⟶ a)

def Quiver.homOfEq {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') : X' ⟶ Y'

An arrow in a quiver can be transported across equalities between the source and target objects.

Equations

• Quiver.homOfEq f hX hY = hX ▸ hY ▸ f

@[simp]

theorem Quiver.homOfEq_trans {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (hX : X = X') (hY : Y = Y') {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') : homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f ⋯ ⋯

theorem Quiver.homOfEq_injective {V : Type u_1} [Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f g : X ⟶ Y} (h : homOfEq f hX hY = homOfEq g hX hY) : f = g

@[simp]

theorem Quiver.homOfEq_rfl {V : Type u_1} [Quiver V] {X Y : V} (f : X ⟶ Y) : homOfEq f ⋯ ⋯ = f

theorem Quiver.heq_of_homOfEq_ext {V : Type u_1} [Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (e : homOfEq f hX hY = f') : f ≍ f'

theorem Quiver.homOfEq_eq_iff {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') : homOfEq f hX hY = g ↔ f = homOfEq g ⋯ ⋯

theorem Quiver.eq_homOfEq_iff {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y) : f = homOfEq g hX hY ↔ homOfEq f ⋯ ⋯ = g

theorem Quiver.homOfEq_heq {V : Type u_1} [Quiver V] {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') (f : X ⟶ Y) : homOfEq f hX hY ≍ f

theorem Quiver.homOfEq_heq_left_iff {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X = X') (hY : Y = Y') : homOfEq f hX hY ≍ g ↔ f ≍ g

theorem Quiver.homOfEq_heq_right_iff {V : Type u_1} [Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y) : f ≍ homOfEq g hX hY ↔ f ≍ g