An orientation of a forest has no oriented cycle #
A quiver none of whose arrows has a reverse, in particular one without loops, and whose underlying
graph TauCeti.Quiver.underlyingGraph is acyclic, has no oriented cycle
(TauCeti.Quiver.isAcyclic_of_isAcyclic_underlyingGraph). An oriented cycle would be a closed walk
in the underlying graph which never turns straight back, since turning back would need an arrow and
its reverse; in a forest such a walk is a path, and a closed path is trivial.
Main results #
TauCeti.Quiver.isAcyclic_of_isAcyclic_underlyingGraph: an orientation of a forest is an acyclic quiver.
theorem
TauCeti.Quiver.isAcyclic_of_isAcyclic_underlyingGraph
{V : Type u}
[Quiver V]
(hrev : ∀ (a b : V) (a_1 : a ⟶ b), IsEmpty (b ⟶ a))
(hG : (underlyingGraph V).IsAcyclic)
:
An orientation of a forest has no oriented cycle. If no arrow of a quiver has a reverse, so that in particular there is no loop, and the underlying graph is acyclic, then every closed path is trivial.