The Euler and Tits forms of the generalized Kronecker quiver

This file evaluates the Euler and Tits forms of the generalized Kronecker quiver in the coordinates of its two vertices. The arithmetic of the Tits form pins down exactly where the boundary of Gabriel's theorem lies: writing n for the number of arrows,

• titsForm d = d src ^ 2 + d tgt ^ 2 - n * (d src * d tgt);
• it is positive definite iff n ≤ 1;
• it is positive semidefinite iff n ≤ 2, and for n = 2 it is the perfect square (d src - d tgt) ^ 2, whose radical is the line spanned by the constant vector (1, 1) -- the null root of the affine root system Ã₁.

Since reflecting a quiver changes its orientation but not its underlying graph, the quiver reflected at tgt has the same Tits form, and hence the same thresholds.

Main results

• TauCeti.Quiver.Kronecker.eulerForm_apply and TauCeti.Quiver.Kronecker.titsForm_apply: the Euler and Tits forms in coordinates.
• TauCeti.Quiver.Kronecker.titsForm_posDef_iff and TauCeti.Quiver.Kronecker.titsForm_nonneg_iff: the two thresholds n ≤ 1 and n ≤ 2.
• TauCeti.Quiver.Kronecker.titsForm_reflect_posDef: the quiver reflected at tgt has positive definite Tits form under the same threshold n ≤ 1.
• TauCeti.Quiver.Kronecker.titsForm_eq_zero_iff_exists_smul and TauCeti.Quiver.Kronecker.titsForm_eq_one_iff: for the Kronecker quiver the radical of the Tits form is the line spanned by (1, 1), and the vectors of Tits norm one are those whose two coordinates differ by one.

References

This file supplies the positive semidefinite Tits form (a - b) ^ 2 with radical (1, 1) asked for by the “Kronecker quiver” worked example of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Derksen--Weyman, An Introduction to Quiver Representations, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.

theorem TauCeti.Quiver.Kronecker.eulerForm_apply {A : Type v} [Fintype A] (d e : Kronecker A → ℤ) : ((eulerForm (Kronecker A)) d) e = d src * e src + d tgt * e tgt - ↑(Fintype.card A) * (d src * e tgt)

The Euler form of the generalized Kronecker quiver, in the coordinates of its two vertices.

theorem TauCeti.Quiver.Kronecker.titsForm_apply {A : Type v} [Fintype A] (d : Kronecker A → ℤ) : (titsForm (Kronecker A)) d = d src ^ 2 + d tgt ^ 2 - ↑(Fintype.card A) * (d src * d tgt)

The Tits form of the generalized Kronecker quiver on n arrows is q(d) = d₁ ^ 2 + d₂ ^ 2 - n * d₁ * d₂.

theorem TauCeti.Quiver.Kronecker.titsForm_one {A : Type v} [Fintype A] : (titsForm (Kronecker A)) 1 = 2 - ↑(Fintype.card A)

The Tits form on the constant dimension vector (1, 1) is 2 - n. This single value decides both thresholds below.

theorem TauCeti.Quiver.Kronecker.titsForm_nonneg {A : Type v} [Fintype A] (h : Fintype.card A ≤ 2) (d : Kronecker A → ℤ) : 0 ≤ (titsForm (Kronecker A)) d

With at most two arrows the Tits form is positive semidefinite.

theorem TauCeti.Quiver.Kronecker.titsForm_nonneg_iff {A : Type v} [Fintype A] : (∀ (d : Kronecker A → ℤ), 0 ≤ (titsForm (Kronecker A)) d) ↔ Fintype.card A ≤ 2

The Tits form of the generalized Kronecker quiver is positive semidefinite exactly when there are at most two arrows. Two arrows is the Kronecker quiver • ⇉ •, of affine type Ã₁, the boundary case of Gabriel's theorem; three or more arrows makes the form indefinite.

theorem TauCeti.Quiver.Kronecker.titsForm_posDef {A : Type v} [Fintype A] (h : Fintype.card A ≤ 1) : (titsForm (Kronecker A)).PosDef

With at most one arrow the Tits form is positive definite: these are the quivers of type A₁ ⊔ A₁ (no arrow) and A₂ (one arrow).

theorem TauCeti.Quiver.Kronecker.titsForm_posDef_iff {A : Type v} [Fintype A] : (titsForm (Kronecker A)).PosDef ↔ Fintype.card A ≤ 1

The Tits form of the generalized Kronecker quiver is positive definite exactly when there is at most one arrow: no arrow gives the disconnected Dynkin quiver A₁ ⊔ A₁, and one arrow gives A₂. Every other generalized Kronecker quiver falls outside the Dynkin classification.

theorem TauCeti.Quiver.Kronecker.titsForm_reflect_posDef {A : Type v} [Fintype A] (h : Fintype.card A ≤ 1) : (titsForm (Reflect (Kronecker A) tgt)).PosDef

With at most one arrow the quiver reflected at tgt has positive definite Tits form: reflecting changes the orientation of a quiver, not its underlying graph, and TauCeti.Quiver.Kronecker.titsForm_posDef covers the underlying graph.

The Kronecker quiver itself

theorem TauCeti.Quiver.Kronecker.titsForm_eq_sq {A : Type v} [Fintype A] (h : Fintype.card A = 2) (d : Kronecker A → ℤ) : (titsForm (Kronecker A)) d = (d src - d tgt) ^ 2

The Tits form of the Kronecker quiver is the perfect square (d₁ - d₂) ^ 2.

theorem TauCeti.Quiver.Kronecker.titsForm_eq_zero_iff {A : Type v} [Fintype A] (h : Fintype.card A = 2) (d : Kronecker A → ℤ) : (titsForm (Kronecker A)) d = 0 ↔ d src = d tgt

The Tits form of the Kronecker quiver vanishes exactly on the diagonal.

theorem TauCeti.Quiver.Kronecker.titsForm_eq_zero_iff_exists_smul {A : Type v} [Fintype A] (h : Fintype.card A = 2) (d : Kronecker A → ℤ) : (titsForm (Kronecker A)) d = 0 ↔ ∃ (c : ℤ), d = c • 1

The radical of the Tits form of the Kronecker quiver is the line spanned by the constant vector (1, 1): the null root of the affine root system Ã₁.

theorem TauCeti.Quiver.Kronecker.titsForm_eq_one_iff {A : Type v} [Fintype A] (h : Fintype.card A = 2) (d : Kronecker A → ℤ) : (titsForm (Kronecker A)) d = 1 ↔ d src = d tgt + 1 ∨ d tgt = d src + 1

For the Kronecker quiver the integer vectors of Tits norm one -- the real roots of the affine root system Ã₁, positive and negative alike -- are exactly those whose two coordinates differ by one, that is (m, m + 1) and (m + 1, m).

theorem TauCeti.Quiver.Kronecker.not_titsForm_posDef {A : Type v} [Fintype A] (h : Fintype.card A = 2) : ¬(titsForm (Kronecker A)).PosDef

The Tits form of the Kronecker quiver is not positive definite: it is isotropic on the nonzero vector (1, 1). Together with TauCeti.Quiver.Kronecker.titsForm_nonneg this says it is positive semidefinite but degenerate, which is what places the Kronecker quiver on the boundary of Gabriel's dichotomy.