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

wide_subquiver V = Π (a b : V), set (a ⟶ b)

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

wide_subquiver.to_Type V H = V

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

wide_subquiver_has_coe_to_sort = {coe := λ (H : wide_subquiver V), wide_subquiver.to_Type V H}

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

H.quiver = {hom := λ (a b : ↥H), {f // f ∈ H a b}}

source

@[protected, instance]

def quiver.wide_subquiver.has_bot {V : Type u_1} [quiver V] :

has_bot (wide_subquiver V)

Equations

quiver.wide_subquiver.has_bot = {bot := λ (a b : V), ∅}

source

@[protected, instance]

def quiver.wide_subquiver.has_top {V : Type u_1} [quiver V] :

has_top (wide_subquiver V)

Equations

quiver.wide_subquiver.has_top = {top := λ (a b : V), set.univ}

source

@[protected, instance]

def quiver.wide_subquiver.inhabited {V : Type u_1} [quiver V] :

inhabited (wide_subquiver V)

Equations

quiver.wide_subquiver.inhabited = {default := ⊤}

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)