The Euler and Tits forms of the D₄ quiver

This file evaluates the Euler and Tits forms of the D₄ quiver in the coordinates of its four vertices and reads off their positive roots. Writing c for the value at the centre and aᵢ for the values at the three outer vertices,

• titsForm d = c ^ 2 + ∑ᵢ aᵢ ^ 2 - c * ∑ᵢ aᵢ, and four times it is the sum of squares c ^ 2 + ∑ᵢ (2 aᵢ - c) ^ 2, so the form is positive definite: D₄ is a Dynkin quiver;
• consequently a dimension vector d ≥ 0 of Tits norm one has c ≤ 2, and the nonnegative vectors of Tits norm one are exactly twelve in number -- the three outer simple roots, the eight vectors with a 1 at the centre and an arbitrary 0/1 pattern outside (s = ∅ being the central simple root), and the highest root (1,1,1;2).

Twelve is the number of positive roots of the root system D₄, so this is the standard check that the positive-root count of a quiver is correct beyond type A, where TauCeti.Quiver.Kronecker.EulerForm already tests it.

Main definitions

• TauCeti.Quiver.D4.rootVector: the dimension vector with a given value at the centre and a 1 at each outer vertex of a given set. Every positive root has this shape.
• TauCeti.Quiver.D4.posRoot: the twelve positive roots, indexed by Fin 3 ⊕ Finset (Fin 3) ⊕ Unit.

Main results

• TauCeti.Quiver.D4.eulerForm_apply and TauCeti.Quiver.D4.titsForm_apply: the two forms in coordinates, and TauCeti.Quiver.D4.four_mul_titsForm the sum-of-squares identity behind everything else.
• TauCeti.Quiver.D4.titsForm_posDef: the Tits form of D₄ is positive definite.
• TauCeti.Quiver.D4.titsForm_eq_one_iff_of_nonneg: a nonnegative dimension vector has Tits norm one exactly when it is one of the listed positive roots.
• TauCeti.Quiver.D4.card_positiveRoots: there are exactly twelve of them.

References

This file supplies the “D₄ quiver” worked example of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md, which asks for the twelve positive roots of D₄ -- the four simple roots, those with a 1 at the centre and a 1 on a subset of the outer vertices, and the highest root with coefficient 2 at the centre. See Derksen--Weyman, An Introduction to Quiver Representations, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. VII.

The two forms in coordinates

theorem TauCeti.Quiver.D4.eulerForm_apply (d e : D4 → ℤ) : ((eulerForm D4) d) e = d center * e center + ∑ i : Fin 3, d (outer i) * e (outer i) - (∑ i : Fin 3, d (outer i)) * e center

The Euler form of the D₄ quiver in the coordinates of its four vertices: the three arrows contribute the single term (∑ᵢ dᵢ) · e_center.

theorem TauCeti.Quiver.D4.titsForm_apply (d : D4 → ℤ) : (titsForm D4) d = d center ^ 2 + ∑ i : Fin 3, d (outer i) ^ 2 - d center * ∑ i : Fin 3, d (outer i)

The Tits form of the D₄ quiver: q(d) = c ^ 2 + ∑ᵢ aᵢ ^ 2 - c * ∑ᵢ aᵢ for c the value at the centre and aᵢ the values at the outer vertices.

theorem TauCeti.Quiver.D4.four_mul_titsForm (d : D4 → ℤ) : 4 * (titsForm D4) d = d center ^ 2 + ∑ i : Fin 3, (2 * d (outer i) - d center) ^ 2

Four times the Tits form of D₄ is a sum of four squares. This single identity carries the positive definiteness of the form and the bound c ≤ 2 on the central coordinate of a root.

theorem TauCeti.Quiver.D4.titsForm_nonneg (d : D4 → ℤ) : 0 ≤ (titsForm D4) d

The Tits form of D₄ is positive semidefinite.

theorem TauCeti.Quiver.D4.titsForm_posDef : (titsForm D4).PosDef

The Tits form of D₄ is positive definite, so D₄ is a Dynkin quiver and, by Gabriel's dichotomy, of finite representation type.

The shape of a positive root

def TauCeti.Quiver.D4.rootVector (c : ℤ) (s : Finset (Fin 3)) : D4 → ℤ

The dimension vector of D₄ with the value c at the centre and a 1 at each outer vertex lying in s. Every nonnegative dimension vector of Tits norm one has this shape.

@[simp]

theorem TauCeti.Quiver.D4.rootVector_center (c : ℤ) (s : Finset (Fin 3)) : rootVector c s center = c

@[simp]

theorem TauCeti.Quiver.D4.rootVector_outer (c : ℤ) (s : Finset (Fin 3)) (j : Fin 3) : rootVector c s (outer j) = if j ∈ s then 1 else 0

theorem TauCeti.Quiver.D4.rootVector_nonneg {c : ℤ} (hc : 0 ≤ c) (s : Finset (Fin 3)) : 0 ≤ rootVector c s

A root vector with a nonnegative central coordinate is a nonnegative dimension vector.

theorem TauCeti.Quiver.D4.sum_rootVector_outer (c : ℤ) (s : Finset (Fin 3)) : ∑ j : Fin 3, rootVector c s (outer j) = ↑s.card

The sum of a root vector over the outer vertices is the size of its defining set.

theorem TauCeti.Quiver.D4.titsForm_rootVector (c : ℤ) (s : Finset (Fin 3)) : (titsForm D4) (rootVector c s) = c ^ 2 + (1 - c) * ↑s.card

The Tits form on a root vector. Because the outer coordinates are 0 or 1, they are their own squares, and q(rootVector c s) = c ^ 2 + (1 - c) * #s.

theorem TauCeti.Quiver.D4.rootVector_eq_iff {c c' : ℤ} {s s' : Finset (Fin 3)} : rootVector c s = rootVector c' s' ↔ c = c' ∧ s = s'

Two root vectors agree exactly when both of their data do: the central coordinate is read off at the centre, and the defining set from the outer coordinates.

The twelve positive roots

theorem TauCeti.Quiver.D4.abs_center_le_two_of_titsForm_eq_one {d : D4 → ℤ} (h : (titsForm D4) d = 1) : |d center| ≤ 2

The central coordinate of a root of D₄ has absolute value at most 2: a dimension vector of Tits norm one, not necessarily nonnegative, has |d center| ≤ 2.

theorem TauCeti.Quiver.D4.exists_eq_rootVector_zero_of_titsForm_eq_one {d : D4 → ℤ} (hd : 0 ≤ d) (h : (titsForm D4) d = 1) (hc : d center = 0) : ∃ (s : Finset (Fin 3)), d = rootVector 0 s ∧ s.card = 1

The positive roots of D₄ with central coordinate 0 are the three outer simple roots: a nonnegative dimension vector of Tits norm one vanishing at the centre is a root vector with a single 1 outside.

theorem TauCeti.Quiver.D4.exists_eq_rootVector_one_of_titsForm_eq_one {d : D4 → ℤ} (h : (titsForm D4) d = 1) (hc : d center = 1) : ∃ (s : Finset (Fin 3)), d = rootVector 1 s

The positive roots of D₄ with central coordinate 1: a dimension vector of Tits norm one with a 1 at the centre, not necessarily nonnegative, is a root vector, that is, has an arbitrary 0/1 pattern outside.

theorem TauCeti.Quiver.D4.eq_rootVector_two_of_titsForm_eq_one {d : D4 → ℤ} (h : (titsForm D4) d = 1) (hc : d center = 2) : d = rootVector 2 Finset.univ

The positive root of D₄ with central coordinate 2 is the highest root: a dimension vector of Tits norm one with a 2 at the centre, not necessarily nonnegative, has a 1 at every outer vertex.

theorem TauCeti.Quiver.D4.titsForm_eq_one_iff_of_nonneg {d : D4 → ℤ} (hd : 0 ≤ d) : (titsForm D4) d = 1 ↔ ∃ (c : ℤ) (s : Finset (Fin 3)), d = rootVector c s ∧ (c = 0 ∧ s.card = 1 ∨ c = 1 ∨ c = 2 ∧ s = Finset.univ)

The positive roots of the D₄ Tits form. A nonnegative dimension vector has Tits norm one exactly when it is a root vector of one of three kinds: an outer simple root (0 at the centre and a single outer 1), a vector with a 1 at the centre and an arbitrary 0/1 pattern outside, or the highest root (2 at the centre and a 1 at every outer vertex).

def TauCeti.Quiver.D4.posRoot : Fin 3 ⊕ Finset (Fin 3) ⊕ Unit → D4 → ℤ

The twelve positive roots of D₄, indexed: inl i is the simple root at the i-th outer vertex, inr (inl s) carries a 1 at the centre and a 1 at each outer vertex of s (so s = ∅ gives the simple root at the centre), and inr (inr ()) is the highest root.

@[simp]

theorem TauCeti.Quiver.D4.posRoot_inl (i : Fin 3) : posRoot (Sum.inl i) = rootVector 0 {i}

@[simp]

theorem TauCeti.Quiver.D4.posRoot_inr_inl (s : Finset (Fin 3)) : posRoot (Sum.inr (Sum.inl s)) = rootVector 1 s

@[simp]

theorem TauCeti.Quiver.D4.posRoot_inr_inr (u : Unit) : posRoot (Sum.inr (Sum.inr u)) = rootVector 2 Finset.univ

theorem TauCeti.Quiver.D4.posRoot_nonneg (x : Fin 3 ⊕ Finset (Fin 3) ⊕ Unit) : 0 ≤ posRoot x

Each of the twelve listed vectors is nonnegative.

theorem TauCeti.Quiver.D4.titsForm_posRoot (x : Fin 3 ⊕ Finset (Fin 3) ⊕ Unit) : (titsForm D4) (posRoot x) = 1

Each of the twelve listed vectors has Tits norm one.

theorem TauCeti.Quiver.D4.posRoot_injective : Function.Injective posRoot

The twelve listed vectors are pairwise distinct.

theorem TauCeti.Quiver.D4.titsForm_eq_one_iff_exists_posRoot {d : D4 → ℤ} (hd : 0 ≤ d) : (titsForm D4) d = 1 ↔ ∃ (x : Fin 3 ⊕ Finset (Fin 3) ⊕ Unit), posRoot x = d

The positive roots of D₄, as the range of the indexing map.

theorem TauCeti.Quiver.D4.card_positiveRoots : Nat.card { d : D4 → ℤ // 0 ≤ d ∧ (titsForm D4) d = 1 } = 12

The D₄ quiver has exactly twelve positive roots, matching the twelve positive roots of the root system D₄: the four simple roots, the six further vectors with a 1 at the centre and a 1 at one or two outer vertices, the vector (1,1,1;1), and the highest root (1,1,1;2).