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.
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
- wide_subquiver V = Π (a b : V), set (a ⟶ b)
@[nolint]
A type synonym for V
, when thought of as a quiver having only the arrows from
some wide_subquiver
.
Equations
- wide_subquiver.to_Type V H = V
@[protected, instance]
def
wide_subquiver_has_coe_to_sort
{V : Type u}
[quiver V] :
has_coe_to_sort (wide_subquiver V) (Type u)
Equations
- wide_subquiver_has_coe_to_sort = {coe := λ (H : wide_subquiver V), wide_subquiver.to_Type V H}
@[protected, instance]
Equations
- quiver.wide_subquiver.has_bot = {bot := λ (a b : V), ∅}
@[protected, instance]
Equations
- quiver.wide_subquiver.has_top = {top := λ (a b : V), set.univ}
@[protected, instance]
Equations
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.
An L
-labelling of a quiver assigns to every arrow an element of L
.
Equations
- quiver.labelling V L = Π ⦃a b : V⦄, (a ⟶ b) → L
@[protected, instance]
def
quiver.labelling.inhabited
{V : Type u}
[quiver V]
(L : Sort u_2)
[inhabited L] :
inhabited (quiver.labelling V L)