Wide subquivers

A wide subquiver H of a quiver H consists of a subset of the edge set a ⟶ b⟶ b for every pair of vertices a b : V. We include 'wide' in the name to emphasize that these subquivers by definition contain all vertices.

ink

def WideSubquiver (V : Type u_1) [inst : Quiver V] : Type (maxu_1v)

A wide subquiver H of G picks out a set H a b of arrows from a to b for every pair of vertices a b.

NB: this does not work for Prop-valued quivers. It requires G : Quiver.{v+1} V.

Equations

• WideSubquiver V = ((a b : V) → Set (a ⟶ b))

ink

def WideSubquiver.toType (V : Type u) [inst : Quiver V] : WideSubquiver V → Type u

A type synonym for V, when thought of as a quiver having only the arrows from some WideSubquiver.

Equations

• WideSubquiver.toType V x = V

ink

instance wideSubquiverHasCoeToSort {V : Type u} [inst : Quiver V] : CoeSort (WideSubquiver V) (Type u)

Equations

• wideSubquiverHasCoeToSort = { coe := fun H => WideSubquiver.toType V H }

ink

instance WideSubquiver.quiver {V : Type u_1} [inst : Quiver V] (H : WideSubquiver V) : Quiver (WideSubquiver.toType V H)

A wide subquiver viewed as a quiver on its own.

Equations

• WideSubquiver.quiver H = { Hom := fun a b => { f // f ∈ H a b } }

ink

instance Quiver.instBotWideSubquiver {V : Type u_1} [inst : Quiver V] : Bot (WideSubquiver V)

Equations

• Quiver.instBotWideSubquiver = { bot := fun x x_1 => ∅ }

ink

instance Quiver.instTopWideSubquiver {V : Type u_1} [inst : Quiver V] : Top (WideSubquiver V)

Equations

• Quiver.instTopWideSubquiver = { top := fun x x_1 => Set.univ }

ink

noncomputable instance Quiver.instInhabitedWideSubquiver {V : Type u_1} [inst : Quiver V] : Inhabited (WideSubquiver V)

Equations

• Quiver.instInhabitedWideSubquiver = { default := ⊤ }

ink

theorem Quiver.Total.ext {V : Type u} : ∀ {inst : Quiver V} (x y : Quiver.Total V), x.left = y.left → x.right = y.right → HEq x.hom y.hom → x = y

ink

theorem Quiver.Total.ext_iff {V : Type u} : ∀ {inst : Quiver V} (x y : Quiver.Total V), x = y ↔ x.left = y.left ∧ x.right = y.right ∧ HEq x.hom y.hom

ink

structure Quiver.Total (V : Type u) [inst : Quiver V] : Sort (max(u+1)v)

• the source vertex of an arrow

  left : V

• the target vertex of an arrow

  right : V

• an arrow

  hom : left ⟶ right

Total V is the type of all arrows of V.

ink

def Quiver.wideSubquiverEquivSetTotal {V : Type u_1} [inst : Quiver V] : WideSubquiver V ≃ Set (Quiver.Total V)

A wide subquiver of G can equivalently be viewed as a total set of arrows.

Equations

• One or more equations did not get rendered due to their size.

ink

def Quiver.Labelling (V : Type u) [inst : Quiver V] (L : Sort u_2) : Sort (imax(u+1)(u+1)u_1u_2)

An L-labelling of a quiver assigns to every arrow an element of L.

Equations

• Quiver.Labelling V L = (⦃a b : V⦄ → (a ⟶ b) → L)

ink

instance Quiver.instInhabitedLabelling {V : Type u} [inst : Quiver V] (L : Sort u_2) [inst : Inhabited L] : Inhabited (Quiver.Labelling V L)

Equations

• Quiver.instInhabitedLabelling L = { default := fun x x_1 x => default }