Any two orientations of a forest are related by reflections at sinks

Reflecting a quiver at a sink reverses the arrows meeting that vertex and keeps its underlying multigraph (Quiver.nonempty_reflectList_sum_hom_equiv). This file proves the converse for a forest: if a quiver q on a finite vertex type has at most one arrow between any two vertices and an acyclic underlying graph, then every quiver q' with the same underlying multigraph is reached from q by reflecting along a sink-admissible list of vertices (Quiver.exists_isSinkAdmissible_reflectList_equiv).

The arrows are turned around one at a time. Removing an arrow u ⟶ w from a forest disconnects w from u; let B be the set of vertices still connected to w. The arrow u ⟶ w is the only one joining B to its complement, and it points into B, so no arrow leaves B. Reflecting at the vertices of B, listed so that no arrow runs from an earlier entry to a later one, is then sink-admissible, and it reverses exactly the arrows joining B to its complement: the single arrow u ⟶ w. The orientation of a forest is acyclic (TauCeti.Quiver.isAcyclic_of_isAcyclic_underlyingGraph), which provides such a listing.

Main results

• Quiver.exists_isSinkAdmissible_reflectList_equiv: two orientations of the same finite forest are related by a sequence of reflections at sinks.

References

• I. N. Bernstein, I. M. Gelfand, V. A. Ponomarev, Coxeter functors and Gabriel's theorem, Russian Math. Surveys 28 (1973), 17--32.
• H. Derksen, J. Weyman, An Introduction to Quiver Representations, Chapter 4.

theorem Quiver.exists_isSinkAdmissible_reflectList_equiv {V : Type u} [Finite V] (q q' : Quiver V) (hsub : ∀ (a b : V), Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))) (hG : (TauCeti.Quiver.underlyingGraph V).IsAcyclic) (h : ∀ (a b : V), Nonempty ((a ⟶ b) ⊕ (b ⟶ a) ≃ (a ⟶ b) ⊕ (b ⟶ a))) : ∃ (l : List V), TauCeti.Quiver.IsSinkAdmissible q l ∧ ∀ (a b : V), Nonempty ((a ⟶ b) ≃ (a ⟶ b))

Any two orientations of a finite forest are related by reflections at sinks. Let q be a quiver on a finite vertex type with at most one arrow between any two vertices, counted in both directions, whose underlying graph is acyclic. If a second quiver q' has the same arrows joining any two vertices, in either direction, then reflecting q along some sink-admissible list of vertices produces a quiver whose arrows are those of q'.