Finite quiver stars

The arrows from a fixed source to a fixed target inject into the star at the source. Thus a finite source star makes each of these arrow types finite, without requiring finite vertices or a chosen enumeration of the arrows.

Main results

• Quiver.finiteHomOfFiniteStar: finite source stars give finite arrow types.

instance Quiver.finiteHomOfFiniteStar {V : Type u} [Quiver V] (i j : V) [Finite (Star i)] : Finite (i ⟶ j)

The arrows from i to j form a finite type when the star at i is finite.