# Documentation

Mathlib.Combinatorics.Quiver.Subquiver

## 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) [] :
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.

Equations
Instances For
def WideSubquiver.toType (V : Type u) [] :

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

Equations
Instances For
instance wideSubquiverHasCoeToSort {V : Type u} [] :
Equations
• wideSubquiverHasCoeToSort = { coe := fun (H : ) => }
instance WideSubquiver.quiver {V : Type u_1} [] (H : ) :

A wide subquiver viewed as a quiver on its own.

Equations
• = { Hom := fun (a b : ) => { f : a b // f H a b } }
instance Quiver.instBotWideSubquiver {V : Type u_1} [] :
Bot ()
Equations
• Quiver.instBotWideSubquiver = { bot := fun (x x_1 : V) => }
instance Quiver.instTopWideSubquiver {V : Type u_1} [] :
Top ()
Equations
• Quiver.instTopWideSubquiver = { top := fun (x x_1 : V) => Set.univ }
noncomputable instance Quiver.instInhabitedWideSubquiver {V : Type u_1} [] :
Equations
• Quiver.instInhabitedWideSubquiver = { default := }
theorem Quiver.Total.ext {V : Type u} :
∀ {inst : } (x y : ), x.left = y.leftx.right = y.rightHEq x.hom y.homx = y
theorem Quiver.Total.ext_iff {V : Type u} :
∀ {inst : } (x y : ), x = y x.left = y.left x.right = y.right HEq x.hom y.hom
structure Quiver.Total (V : Type u) [] :
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 : s.left s.right

an arrow

Instances For

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.
Instances For
def Quiver.Labelling (V : Type u) [] (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.

Equations
• = (a b : V⦄ → (a b)L)
Instances For
instance Quiver.instInhabitedLabelling {V : Type u} [] (L : Sort u_2) [] :
Equations
• = { default := fun (x x_1 : V) (x : x x_1) => default }