# mathlibdocumentation

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 wide_subquiver (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.

Equations
Instances for wide_subquiver
@[nolint]
def wide_subquiver.to_Type (V : Type u) [quiver V] (H : wide_subquiver V) :
Type u

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

Equations
@[protected, instance]
def wide_subquiver_has_coe_to_sort {V : Type u} [quiver V] :
(Type u)
Equations
@[protected, instance]
def wide_subquiver.quiver {V : Type u_1} [quiver V] (H : wide_subquiver V) :

A wide subquiver viewed as a quiver on its own.

Equations
@[protected, instance]
def quiver.wide_subquiver.has_bot {V : Type u_1} [quiver V] :
Equations
@[protected, instance]
def quiver.wide_subquiver.has_top {V : Type u_1} [quiver V] :
Equations
@[protected, instance]
def quiver.wide_subquiver.inhabited {V : Type u_1} [quiver V] :
Equations
theorem quiver.total.ext {V : Type u} {_inst_1 : quiver V} (x y : quiver.total V) (h : x.left = y.left) (h_1 : x.right = y.right) (h_2 : x.hom == y.hom) :
x = y
@[nolint, ext]
structure quiver.total (V : Type u) [quiver V] :
Sort (max (u+1) v)

total V is the type of all arrows of V.

Instances for quiver.total
• quiver.total.has_sizeof_inst
theorem quiver.total.ext_iff {V : Type u} {_inst_1 : quiver V} (x y : quiver.total V) :
x = y x.left = y.left x.right = y.right x.hom == y.hom
def quiver.wide_subquiver_equiv_set_total {V : Type u_1} [quiver V] :

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

Equations
def quiver.labelling (V : Type u) [quiver V] (L : Sort u_2) :
Sort (imax (u+1) (u+1) u_1 u_2)

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

Equations
• = Π ⦃a b : V⦄, (a b) → L
Instances for quiver.labelling
@[protected, instance]
def quiver.labelling.inhabited {V : Type u} [quiver V] (L : Sort u_2) [inhabited L] :
Equations