Documentation

TauCeti.RepresentationTheory.Quiver.FiniteRepType.Orientation

Finite representation type of a forest does not depend on the orientation #

Whether a quiver has finite representation type is unchanged by reflecting it at a sink (TauCeti.isFiniteRepType_reflectList_iff), and any two orientations of a finite forest are related by such reflections (Quiver.exists_isSinkAdmissible_reflectList_equiv). So for a quiver whose underlying graph is a forest, with at most one arrow between any two vertices, finite representation type is a property of the underlying graph alone: every quiver with the same underlying multigraph has finite representation type exactly when the original one does (TauCeti.isFiniteRepType_iff_of_isAcyclic_underlyingGraph), and in particular so does every reorientation TauCeti.Reorient Q σ (TauCeti.isFiniteRepType_reorient_iff).

Combined with the passage of finite representation type to subquivers, this frees the forest from the arrows of the ambient quiver as well: if the underlying graph of a forest quiver P has a copy in the underlying graph of a quiver Q of finite representation type, then P has finite representation type (TauCeti.IsFiniteRepType.of_copy_underlyingGraph). The arrows of Q over the edges of the copy orient the forest in some way, giving a subquiver of Q, and that orientation has finite representation type together with P.

This is how Gabriel's dichotomy is reduced to the underlying graph: for a tree, such as a Dynkin or an extended Dynkin diagram other than a cycle, it suffices to treat a single orientation.

Main results #

References #

theorem TauCeti.isFiniteRepType_iff_of_isAcyclic_underlyingGraph {k : Type u} [Field k] {V : Type v} [Finite V] (q q' : Quiver V) (hsub : ∀ (a b : V), Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))) (hG : (Quiver.underlyingGraph V).IsAcyclic) (h : ∀ (a b : V), Nonempty ((a ⟶ b) ⊕ (b ⟶ a) ≃ (a ⟶ b) ⊕ (b ⟶ a))) :

Finite representation type of a forest does not depend on the orientation. 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. A quiver q' with the same arrows joining any two vertices, in either direction, has finite representation type exactly when q does.

theorem TauCeti.isFiniteRepType_reorient_iff {k : Type u} [Field k] {Q : Type v} [q : Quiver Q] [Finite Q] (hsub : ∀ (a b : Q), Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))) (hG : (Quiver.underlyingGraph Q).IsAcyclic) (σ : ⦃i j : Q⦄ → (i ⟶ j) → Bool) :

Reorienting a forest does not change whether it has finite representation type. If a finite quiver Q has at most one arrow between any two vertices, counted in both directions, and its underlying graph is acyclic, then turning around any of its arrows gives a quiver TauCeti.Reorient Q σ with finite representation type exactly when Q has it.

theorem TauCeti.IsFiniteRepType.of_copy_underlyingGraph {k : Type u} [Field k] {Q : Type v} [Quiver Q] {W : Type v'} [Finite W] [p : Quiver W] (h : IsFiniteRepType k Q) (hsub : ∀ (a b : W), Subsingleton ((a ⟶ b) ⊕ (b ⟶ a))) (hG : (Quiver.underlyingGraph W).IsAcyclic) (f : (Quiver.underlyingGraph W).Copy (Quiver.underlyingGraph Q)) :

Finite representation type passes to forests in the underlying graph. Let W be a finite quiver with at most one arrow between any two vertices, counted in both directions, whose underlying graph is acyclic. If the underlying graph of W has a copy in the underlying graph of a quiver Q of finite representation type, then W has finite representation type, whatever the directions of the arrows of Q along the copy.

The copy need not be induced, and Q may have several arrows, in either direction, over an edge of the copy: choosing one of them over each edge orients the forest as a subquiver of Q, and that orientation has finite representation type together with W.