Finite representation type does not depend on reflecting at a sink or a source

Reflecting a quiver at a sink or at a source reverses the arrows meeting that vertex, and the Bernstein-Gelfand-Ponomarev reflection functors carry its representations along. This file proves that the change of orientation does not affect finite representation type: for a sink i of a finite quiver Q, the reflected quiver TauCeti.Quiver.Reflect Q i has finite representation type exactly when Q does (TauCeti.isFiniteRepType_reflect_iff_of_isSink), and likewise for a source (TauCeti.isFiniteRepType_reflect_iff_of_isSource). Iterating, the same holds along every sink-admissible list of vertices (TauCeti.isFiniteRepType_reflectList_iff).

The argument is the same at a sink and at a source. A finite-dimensional indecomposable representation M of Q either vanishes away from i, or the reflection functor at i is injective on its morphisms in the appropriate sense, so that it carries M to a finite-dimensional indecomposable representation of the reflected quiver and reflects isomorphisms among such representations. The representations of the first kind form a single isomorphism class, by TauCeti.nonempty_iso_of_forall_subsingleton: that of the vertex simple at i. So the isomorphism classes of finite-dimensional indecomposables of Q are, up to that one class, embedded in those of the reflected quiver; and reflecting the reflected quiver at i once more returns Q (TauCeti.Quiver.reflectAt_reflectAt), which gives the converse.

This is how Gabriel's dichotomy is freed from the choice of orientation: whether a quiver has finite representation type depends only on its underlying graph as soon as any two orientations are related by reflections at sinks, which is the case for a tree.

Main results

• TauCeti.IsFiniteRepType.of_reflect_of_isSink and TauCeti.IsFiniteRepType.of_reflect_of_isSource: if the quiver reflected at a sink, respectively a source, has finite representation type, then so does the original one.
• TauCeti.isFiniteRepType_reflect_iff_of_isSink and TauCeti.isFiniteRepType_reflect_iff_of_isSource: finite representation type is invariant under reflection at a sink or at a source.
• TauCeti.isFiniteRepType_reflectList_iff: it is invariant under reflection along every sink-admissible list of vertices.

Implementation notes

The representations of Q are taken with vertex spaces in max v w x, the universe in which the reflection functors produce them, and those of the reflected quiver in the same universe. The iterated statement carries the quiver structure explicitly, as TauCeti.Quiver.reflectList does, because it is the structure that the recursion along the list changes.

References

• I. N. Bernstein, I. M. Gelfand, V. A. Ponomarev, Coxeter functors and Gabriel's theorem, Russian Math. Surveys 28 (1973), 17--32.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.

theorem TauCeti.IsFiniteRepType.of_reflect_of_isSource {k : Type u} {Q : Type v} [Field k] [Quiver Q] {i : Q} [Finite ((b : Q) × (i ⟶ b))] (hi : Quiver.IsSource i) (h : IsFiniteRepType k (Quiver.Reflect Q i)) : IsFiniteRepType k Q

Finite representation type ascends along the reflection at a source. If i is a source of Q and the quiver obtained by reflecting Q at i has finite representation type, then so does Q: a finite-dimensional indecomposable representation of Q is either the vertex simple at i, or its source reflection is a finite-dimensional indecomposable representation of the reflected quiver, from which it is recovered up to isomorphism.

theorem TauCeti.IsFiniteRepType.of_reflect_of_isSink {k : Type u} {Q : Type v} [Field k] [Quiver Q] {i : Q} [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (hi : Quiver.IsSink i) (h : IsFiniteRepType k (Quiver.Reflect Q i)) : IsFiniteRepType k Q

Finite representation type ascends along the reflection at a sink. If i is a sink of Q and the quiver obtained by reflecting Q at i has finite representation type, then so does Q: a finite-dimensional indecomposable representation of Q is either the vertex simple at i, or its reflection is a finite-dimensional indecomposable representation of the reflected quiver, from which it is recovered up to isomorphism.

theorem TauCeti.isFiniteRepType_reflect_iff_of_isSink {k : Type u} {Q : Type v} [Field k] [Quiver Q] {i : Q} [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (hi : Quiver.IsSink i) : IsFiniteRepType k (Quiver.Reflect Q i) ↔ IsFiniteRepType k Q

Finite representation type is invariant under reflection at a sink. The quiver obtained by reversing the arrows into a sink i of a finite quiver Q has finite representation type exactly when Q does.

theorem TauCeti.isFiniteRepType_reflect_iff_of_isSource {k : Type u} {Q : Type v} [Field k] [Quiver Q] {i : Q} [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] (hi : Quiver.IsSource i) : IsFiniteRepType k (Quiver.Reflect Q i) ↔ IsFiniteRepType k Q

Finite representation type is invariant under reflection at a source. The quiver obtained by reversing the arrows out of a source i of a finite quiver Q has finite representation type exactly when Q does.

theorem TauCeti.isFiniteRepType_reflectList_iff {k : Type u} [Field k] {V : Type v} [Finite V] (l : List V) (q : Quiver V) (_hq : ∀ (a b : V), Finite (a ⟶ b)) : Quiver.IsSinkAdmissible q l → (IsFiniteRepType k V ↔ IsFiniteRepType k V)

Finite representation type is invariant under reflection along a sink-admissible list. Reflecting a finite quiver successively at the entries of a list, each a sink of the quiver its predecessors produce, does not change whether it has finite representation type.