Wide subquivers

A wide subquiver H of a quiver H consists of a subset of the edge set a ⟶ 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.

def WideSubquiver (V : Type u_1) [Quiver V] : Type (max u_1 v)

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.

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

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

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

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

A wide subquiver viewed as a quiver on its own.

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

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

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

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

Total V is the type of all arrows of V.

• left : V

  the source vertex of an arrow

• right : V

  the target vertex of an arrow

• hom : self.left ⟶ self.right

  an arrow

theorem Quiver.Total.ext_iff {V : Type u} {inst✝ : Quiver V} {x y : Total V} : x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.hom ≍ y.hom

theorem Quiver.Total.ext {V : Type u} {inst✝ : Quiver V} {x y : Total V} (left : x.left = y.left) (right : x.right = y.right) (hom : x.hom ≍ y.hom) : x = y

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

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

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

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

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