mathlib3 documentation


Wide subquivers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

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

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

@[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.

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

total V is the type of all arrows of V.

Instances for
theorem {V : Type u} {_inst_1 : quiver V} (x y : V) :
x = y x.left = y.left x.right = y.right x.hom == y.hom

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_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.

Instances for quiver.labelling
@[protected, instance]