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