Acyclic reflected quivers

This file develops the interaction between acyclicity and reflection at a sink or source. A nonempty finite acyclic quiver has a sink and a source, and reflecting at either one preserves acyclicity.

Main results

• TauCeti.Quiver.IsAcyclic.exists_isSink: a nonempty finite acyclic quiver has a sink.
• TauCeti.Quiver.IsAcyclic.exists_isSource: a nonempty finite acyclic quiver has a source.
• TauCeti.Quiver.IsAcyclic.reflect_of_isSink: reflecting an acyclic quiver at a sink leaves it acyclic.
• TauCeti.Quiver.IsAcyclic.reflect_of_isSource: reflecting an acyclic quiver at a source leaves it acyclic.

References

These results support the sink-admissible reflection-functor constructions in Layers 4 and 5 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

theorem TauCeti.Quiver.IsAcyclic.exists_isSink {V : Type u} [Quiver V] [Finite V] [Nonempty V] (h : IsAcyclic V) : ∃ (i : V), IsSink i

A nonempty finite acyclic quiver has a sink: were every vertex to carry an outgoing arrow, paths could be extended indefinitely, past the bound of TauCeti.Quiver.IsAcyclic.length_lt_card.

theorem TauCeti.Quiver.IsAcyclic.exists_isSource {V : Type u} [Quiver V] [Finite V] [Nonempty V] (h : IsAcyclic V) : ∃ (i : V), IsSource i

A nonempty finite acyclic quiver has a source.

theorem TauCeti.Quiver.IsAcyclic.reflect_of_isSink {V : Type u} [Quiver V] {i : V} (hV : IsAcyclic V) (h : IsSink i) : IsAcyclic (Reflect V i)

Reflecting an acyclic quiver at a sink leaves it acyclic.

theorem TauCeti.Quiver.IsAcyclic.reflect_of_isSource {V : Type u} [Quiver V] {i : V} (hV : IsAcyclic V) (h : IsSource i) : IsAcyclic (Reflect V i)

Reflecting an acyclic quiver at a source leaves it acyclic.