Finite representation type of a tree quiver forces a positive definite Tits form

This file proves the converse half of Gabriel's dichotomy for quivers whose underlying graph is a tree: such a quiver of finite representation type has a positive definite Tits form.

The argument is the graph-theoretic half of Gabriel's theorem. The extended Dynkin trees D~ₘ₊₄, E₆~, E₇~ and E₈~ obstruct finite representation type wherever they occur in the underlying graph (TauCeti.not_isFiniteRepType_of_copy_affineD and its siblings), so it is enough to show that a finite tree containing none of them has a positive definite matrix 2I - A:

• a vertex of degree at least four is the centre of a copy of D~₄;
• two vertices of degree at least three, joined by the path between them, carry a copy of D~ₘ₊₄;
• a tree with no vertex of degree three is a path, the diagram of type Aₙ;
• a tree with a unique vertex of degree three is a star with three arms (TauCeti.exists_equiv_forall_eq_starCartanMatrix_of_isTree_of_isSimplyLaced), and its arms are either those of Dₙ, E₆, E₇ or E₈, or long enough to contain E₆~, E₇~ or E₈~.

The Cartan matrices of the simply-laced Dynkin types are positive definite (TauCeti.DynkinType.IsSimplyLaced.posDef_map_intCast_cartanMatrix), and the Tits form of a quiver with no loops and at most one arrow in total, counting both directions, between any two distinct vertices is half the form of 2I - A for its underlying graph (TauCeti.titsForm_posDef_iff_posDef_graphCartanMatrix).

Main results

• SimpleGraph.IsTree.posDef_graphCartanMatrix: a finite tree containing no copy of D~ₘ₊₄, E₆~, E₇~ or E₈~ has a positive definite matrix 2I - A.
• TauCeti.IsFiniteRepType.posDef_titsForm_of_isTree: a quiver of finite representation type whose underlying graph is a tree has a positive definite Tits form.

Implementation notes

The extended Dynkin trees are the underlying graphs of the quivers TauCeti.Quiver.AffineD m, TauCeti.Quiver.AffineE6, TauCeti.Quiver.AffineE7 and TauCeti.Quiver.AffineE8, on which their infinite families of indecomposables are built, so the copies are stated for those graphs.

Loops, parallel arrows and opposite arrows are excluded by the obstruction theorems in TauCeti.RepresentationTheory.Quiver.FiniteRepType.Obstructions.

References

• P. Gabriel, Unzerlegbare Darstellungen I, Manuscripta Math. 6 (1972), 71--103.
• 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 SimpleGraph.IsTree.posDef_graphCartanMatrix {V : Type u_1} {G : SimpleGraph V} [Finite V] [DecidableEq V] [DecidableRel G.Adj] (hG : G.IsTree) (hD : ∀ (m : ℕ), ¬(TauCeti.Quiver.underlyingGraph (TauCeti.Quiver.AffineD m)).IsContained G) (hE₆ : ¬(TauCeti.Quiver.underlyingGraph TauCeti.Quiver.AffineE6).IsContained G) (hE₇ : ¬(TauCeti.Quiver.underlyingGraph TauCeti.Quiver.AffineE7).IsContained G) (hE₈ : ¬(TauCeti.Quiver.underlyingGraph TauCeti.Quiver.AffineE8).IsContained G) : (G.graphCartanMatrix ℚ).PosDef

A finite tree containing no extended Dynkin tree has a positive definite matrix 2I - A. If a finite tree G contains no copy of D~ₘ₊₄, E₆~, E₇~ or E₈~, given as the underlying graphs of the quivers TauCeti.Quiver.AffineD m, TauCeti.Quiver.AffineE6, TauCeti.Quiver.AffineE7 and TauCeti.Quiver.AffineE8, then 2I - A is positive definite over ℚ: G is a Dynkin diagram of type A, D or E.

theorem TauCeti.IsFiniteRepType.posDef_titsForm_of_isTree {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (h : IsFiniteRepType k Q) (htree : (Quiver.underlyingGraph Q).IsTree) : (titsForm Q).PosDef

Finite representation type of a tree quiver forces a positive definite Tits form. A finite quiver of finite representation type whose underlying graph is a tree has a positive definite Tits form.

This is the converse of TauCeti.isFiniteRepType_of_titsForm_posDef for such quivers. The underlying graph contains none of the extended Dynkin trees, which obstruct finite representation type, so it is a Dynkin diagram (SimpleGraph.IsTree.posDef_graphCartanMatrix), and twice the Tits form is the form of the matrix 2I - A of the underlying graph (TauCeti.titsForm_posDef_iff_posDef_graphCartanMatrix).