Topological sorting of an acyclic quiver

Every finite set of vertices of an acyclic quiver can be listed without repetition so that no arrow runs from an earlier entry to a later one.

Main results

• TauCeti.Quiver.IsAcyclic.exists_pairwise_isEmpty_hom: every finite set of vertices of an acyclic quiver has a topological ordering, along which no arrow runs forwards.

Applications

This ordering is the input to the sink-admissible orderings of TauCeti.RepresentationTheory.Quiver.Reflection.Admissible.

theorem TauCeti.Quiver.IsAcyclic.exists_pairwise_isEmpty_hom {V : Type u} [Quiver V] (h : IsAcyclic V) (s : Finset V) : ∃ (l : List V), l.Nodup ∧ (∀ (v : V), v ∈ l ↔ v ∈ s) ∧ List.Pairwise (fun (x y : V) => IsEmpty (x ⟶ y)) l

Topological sorting. Every finite set of vertices of an acyclic quiver can be listed without repetition so that no arrow runs from an earlier entry to a later one.