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⟶ 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) [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
def WideSubquiver.toType (V : Type u) [inst : Quiver V] :

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

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

A wide subquiver viewed as a quiver on its own.

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

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.
    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
    instance Quiver.instInhabitedLabelling {V : Type u} [inst : Quiver V] (L : Sort u_2) [inst : Inhabited L] :
    Equations