mathlib3 documentation

combinatorics.quiver.subquiver

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.

source
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
source
@[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
source
@[protected, instance]
def wide_subquiver_has_coe_to_sort {V : Type u} [quiver V] :
has_coe_to_sort (wide_subquiver V) (Type u)
Equations
source
@[protected, instance]
def wide_subquiver.quiver {V : Type u_1} [quiver V] (H : wide_subquiver V) :
quiver ↥H

A wide subquiver viewed as a quiver on its own.

Equations
source
@[protected, instance]
def quiver.wide_subquiver.has_bot {V : Type u_1} [quiver V] :
has_bot (wide_subquiver V)
Equations
source
@[protected, instance]
def quiver.wide_subquiver.has_top {V : Type u_1} [quiver V] :
has_top (wide_subquiver V)
Equations
source
@[protected, instance]
def quiver.wide_subquiver.inhabited {V : Type u_1} [quiver V] :
inhabited (wide_subquiver V)
Equations
source
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
source
@[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
source
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
source
def quiver.wide_subquiver_equiv_set_total {V : Type u_1} [quiver V] :
wide_subquiver V ≃ set (quiver.total V)

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

Equations
source
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
Instances for quiver.labelling
source
@[protected, instance]
def quiver.labelling.inhabited {V : Type u} [quiver V] (L : Sort u_2) [inhabited L] :
inhabited (quiver.labelling V L)
Equations