Mathlib.Combinatorics.Quiver.Basic

Module docstring

{"# 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 Hom : 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. "}

Quiver structure

(V : Type u)

Full source

/-- 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) where
  /-- The type of edges/arrows/morphisms between a given source and target. -/
  Hom : V → V → Sort v

Quiver (Directed Graph Structure)

Informal description

A quiver on a type $V$ of vertices assigns to every pair $a, b \in V$ a type $a \longrightarrow b$ of arrows from $a$ to $b$. This structure generalizes the notion of directed graphs, allowing for different levels of arrow multiplicity depending on the chosen universe level (e.g., `Prop` for no repeated edges or `Type` for multigraphs).

term_⟶_ definition

: Lean.TrailingParserDescr✝

Full source

/--
Notation for the type of edges/arrows/morphisms between a given source and target
in a quiver or category.
-/
infixr:10 " ⟶ " => Quiver.Hom

Arrow type in a quiver or category

Informal description

The notation `a ⟶ b` represents the type of edges (or arrows/morphisms) from vertex `a` to vertex `b` in a quiver or category.

Quiver.opposite instance

{V} [Quiver V] : Quiver Vᵒᵖ

Full source

/-- `Vᵒᵖ` reverses the direction of all arrows of `V`. -/
instance opposite {V} [Quiver V] : Quiver Vᵒᵖ :=
  ⟨fun a b => (unop b ⟶ unop a)ᵒᵖ⟩

Opposite Quiver Construction

Informal description

For any quiver $V$, the opposite quiver $V^{\mathrm{op}}$ is defined by reversing the direction of all arrows. Specifically, for any vertices $a, b \in V$, an arrow $a \longrightarrow b$ in $V$ corresponds to an arrow $\mathrm{op}\,b \longrightarrow \mathrm{op}\,a$ in $V^{\mathrm{op}}$.

Quiver.Hom.op definition

{V} [Quiver V] {X Y : V} (f : X ⟶ Y) : op Y ⟶ op X

Full source

/-- The opposite of an arrow in `V`. -/
def Hom.op {V} [Quiver V] {X Y : V} (f : X ⟶ Y) : opop Y ⟶ op X := ⟨f⟩

Opposite of a quiver arrow

Informal description

Given an arrow $f : X \longrightarrow Y$ in a quiver $V$, the function returns the corresponding arrow $\mathrm{op}\, Y \longrightarrow \mathrm{op}\, X$ in the opposite quiver $V^{\mathrm{op}}$.

Quiver.Hom.unop definition

{V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unop Y ⟶ unop X

Full source

/-- Given an arrow in `Vᵒᵖ`, we can take the "unopposite" back in `V`. -/
def Hom.unop {V} [Quiver V] {X Y : Vᵒᵖ} (f : X ⟶ Y) : unopunop Y ⟶ unop X := Opposite.unop f

Unopposite of a quiver arrow

Informal description

Given an arrow $f : X \longrightarrow Y$ in the opposite quiver $V^{\mathrm{op}}$, the function returns the corresponding arrow $\mathrm{unop}\, Y \longrightarrow \mathrm{unop}\, X$ in the original quiver $V$.

Quiver.Hom.opEquiv definition

{V} [Quiver V] {X Y : V} : (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X)

Full source

/-- The bijection `(X ⟶ Y) ≃ (op Y ⟶ op X)`. -/
@[simps]
def Hom.opEquiv {V} [Quiver V] {X Y : V} :
    (X ⟶ Y) ≃ (Opposite.op Y ⟶ Opposite.op X) where
  toFun := Opposite.op
  invFun := Opposite.unop
  left_inv _ := rfl
  right_inv _ := rfl

Bijection between arrows and their opposites in a quiver

Informal description

The bijection between arrows $X \longrightarrow Y$ in a quiver $V$ and arrows $\mathrm{op}\, Y \longrightarrow \mathrm{op}\, X$ in the opposite quiver $V^{\mathrm{op}}$. Specifically, the function maps an arrow $f : X \longrightarrow Y$ to its opposite $\mathrm{op}\, f : \mathrm{op}\, Y \longrightarrow \mathrm{op}\, X$, and the inverse function maps an arrow $g : \mathrm{op}\, Y \longrightarrow \mathrm{op}\, X$ back to $\mathrm{unop}\, g : X \longrightarrow Y$.

Quiver.Empty definition

(V : Type u) : Type u

Full source

/-- A type synonym for a quiver with no arrows. -/
def Empty (V : Type u) : Type u := V

Empty quiver

Informal description

The type synonym `Quiver.Empty V` represents a quiver (directed graph) with vertex set `V` and no arrows between any pair of vertices. For any two vertices `a, b : V`, the type of arrows `a ⟶ b` is empty.

Quiver.emptyQuiver instance

(V : Type u) : Quiver.{u} (Empty V)

Full source

instance emptyQuiver (V : Type u) : Quiver.{u} (Empty V) := ⟨fun _ _ => PEmpty⟩

Empty Quiver Structure

Informal description

For any type $V$, the empty quiver structure on $V$ is a quiver where there are no arrows between any two vertices. That is, for any $a, b \in V$, the type of arrows $a \longrightarrow b$ is empty.

Quiver.empty_arrow theorem

{V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty

Full source

@[simp]
theorem empty_arrow {V : Type u} (a b : Empty V) : (a ⟶ b) = PEmpty := rfl

No Arrows in Empty Quiver: $a \longrightarrow b \cong \mathrm{PEmpty}$

Informal description

For any two vertices $a$ and $b$ in an empty quiver $V$, the type of arrows from $a$ to $b$ is equivalent to the empty type $\mathrm{PEmpty}$ (i.e., there are no arrows between any two vertices).

Quiver.IsThin abbrev

(V : Type u) [Quiver V] : Prop

Full source

/-- A quiver is thin if it has no parallel arrows. -/
abbrev IsThin (V : Type u) [Quiver V] : Prop := ∀ a b : V, Subsingleton (a ⟶ b)

Definition of a Thin Quiver

Informal description

A quiver $V$ is called *thin* if for every pair of vertices $a, b \in V$, the type of arrows $a \longrightarrow b$ is a subsingleton (i.e., there is at most one arrow between any two vertices).

Quiver.homOfEq definition

{X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') : X' ⟶ Y'

Full source

/-- An arrow in a quiver can be transported across equalities between the source and target
objects. -/
def homOfEq {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') : X' ⟶ Y' := by
  subst hX hY
  exact f

Transport of quiver arrows along vertex equalities

Informal description

Given an arrow $f : X \longrightarrow Y$ in a quiver $V$ and equalities $h_X : X = X'$ and $h_Y : Y = Y'$, the function constructs an arrow $X' \longrightarrow Y'$ by transporting $f$ along the equalities $h_X$ and $h_Y$.

Quiver.homOfEq_trans theorem

 {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y') {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') :
  homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f (hX.trans hX') (hY.trans hY')

Full source

@[simp]
lemma homOfEq_trans {X Y : V} (f : X ⟶ Y) {X' Y' : V} (hX : X = X') (hY : Y = Y')
    {X'' Y'' : V} (hX' : X' = X'') (hY' : Y' = Y'') :
    homOfEq (homOfEq f hX hY) hX' hY' = homOfEq f (hX.trans hX') (hY.trans hY') := by
  subst hX hY hX' hY'
  rfl

Transitivity of Arrow Transport in Quivers

Informal description

Given an arrow $f : X \longrightarrow Y$ in a quiver $V$, and vertex equalities $h_X : X = X'$, $h_Y : Y = Y'$, $h_{X'} : X' = X''$, $h_{Y'} : Y' = Y''$, the transport of $f$ along the composite equalities $h_X \cdot h_{X'}$ and $h_Y \cdot h_{Y'}$ is equal to the composition of the transports along $h_X, h_Y$ and $h_{X'}, h_{Y'}$.

Quiver.homOfEq_injective theorem

 {X X' Y Y' : V} (hX : X = X') (hY : Y = Y') {f g : X ⟶ Y} (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g

Full source

lemma homOfEq_injective {X X' Y Y' : V} (hX : X = X') (hY : Y = Y')
    {f g : X ⟶ Y} (h : Quiver.homOfEq f hX hY = Quiver.homOfEq g hX hY) : f = g := by
  subst hX hY
  exact h

Injectivity of Arrow Transport in Quivers

Informal description

For any vertices $X, X', Y, Y'$ in a quiver $V$, given equalities $h_X : X = X'$ and $h_Y : Y = Y'$, if the transported arrows $\text{homOfEq}(f, h_X, h_Y)$ and $\text{homOfEq}(g, h_X, h_Y)$ are equal, then the original arrows $f$ and $g$ from $X$ to $Y$ are equal.

Quiver.homOfEq_rfl theorem

{X Y : V} (f : X ⟶ Y) : Quiver.homOfEq f rfl rfl = f

Full source

@[simp]
lemma homOfEq_rfl {X Y : V} (f : X ⟶ Y) : Quiver.homOfEq f rfl rfl = f := rfl

Identity Transport of Quiver Arrows

Informal description

For any arrow $f : X \longrightarrow Y$ in a quiver, transporting $f$ along the reflexivity equalities $\text{rfl} : X = X$ and $\text{rfl} : Y = Y$ yields $f$ itself, i.e., $\text{homOfEq}\, f\, \text{rfl}\, \text{rfl} = f$.

Quiver.heq_of_homOfEq_ext theorem

{X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'} (e : Quiver.homOfEq f hX hY = f') : HEq f f'

Full source

lemma heq_of_homOfEq_ext {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (e : Quiver.homOfEq f hX hY = f') : HEq f f' := by
  subst hX hY
  rw [Quiver.homOfEq_rfl] at e
  rw [e]

Heterogeneous Equality of Quiver Arrows via Transport

Informal description

For any vertices $X, Y, X', Y'$ in a quiver $V$, given equalities $h_X : X = X'$ and $h_Y : Y = Y'$, and arrows $f : X \longrightarrow Y$ and $f' : X' \longrightarrow Y'$, if the transported arrow $\text{homOfEq}(f, h_X, h_Y)$ equals $f'$, then $f$ and $f'$ are heterogeneously equal (i.e., equal up to the vertex equalities $h_X$ and $h_Y$).