The Coxeter transformation on the dimension vectors of a quiver

Composing the simple reflections of a finite quiver Q at the successive vertices of a word l = [i₁, …, iₙ] gives the endomorphism sᵢₙ ∘ ⋯ ∘ sᵢ₁ of the dimension-vector lattice Q → ℤ. The Coxeter transformation is the case of a word listing every vertex exactly once, taken in a sink-admissible order; it is the numerical shadow of the Coxeter functor, the composite of the Bernstein-Gelfand-Ponomarev reflection functors at i₁, …, iₙ. On an indecomposable representation other than the vertex simple at the current sink, and when the source spaces of the incoming arrows are finite-dimensional, each reflection functor acts on dimension vectors by the simple reflection at its vertex (TauCeti.dimVector_reflectRep_of_indecomposable); the excluded vertex simple is annihilated instead. Reflecting the quiver itself changes neither the polarized Tits form nor the simple reflections built from it (TauCeti.vertexPreReflection_reflect_apply), so the successive reflections may all be read in the original quiver.

Following TauCeti.vertexPreReflection, the composite is defined for an arbitrary word, and the results that need the Coxeter case say so through explicit List.Nodup and vertex-exhaustion hypotheses.

The main result is that this composite has no nonzero fixed vector once the word runs over every vertex without repetition and the polarized Tits form has trivial radical, in particular whenever the Tits form is anisotropic, and so for a quiver of ADE type, where the Tits form is positive definite and QuadraticMap.PosDef.anisotropic applies. This is the engine of the Bernstein-Gelfand-Ponomarev proof of Gabriel's theorem that forbids a nonzero dimension vector from being carried to itself after a full pass of the Coxeter functor. The finite-orbit argument in TauCeti.exists_vertexPreReflectionList_pow_apply_neg supplies the descent to a vertex simple without first passing through root-system combinatorics.

Main definitions and results

• TauCeti.vertexPreReflectionList: the composite of the simple reflections along a word in the vertices, as a ℤ-linear endomorphism of the dimension-vector lattice. As with TauCeti.vertexPreReflection, no hypothesis on the vertices is imposed.
• TauCeti.vertexReflectionList: the same map as a linear automorphism, over a word in loopless vertices, with TauCeti.vertexReflectionList_symm identifying its inverse as the automorphism along the reversed word.
• TauCeti.vertexPreReflectionList_flatten_replicate: repeating a word raises its reflection product to the corresponding power, so a run of Coxeter passes is itself a reflection product.
• TauCeti.vertexPreReflectionList_reflectList: the reflection product along a word does not depend on the orientation of the quiver, so it is unchanged by reflecting the quiver along another word.
• TauCeti.nonneg_vertexPreReflectionList_take_append and TauCeti.nonneg_vertexPreReflectionList_take_flatten_replicate: nonnegativity of the intermediate vectors along a word is inherited by a concatenation and by a repetition.
• TauCeti.nonneg_vertexPreReflectionList_take_reverse: reading a word with nonnegative intermediate vectors backwards from its endpoint stays nonnegative.
• TauCeti.titsForm_vertexPreReflectionList and TauCeti.bijOn_vertexPreReflectionList: along a word in loopless vertices, the composite preserves the Tits form, and hence permutes each of its level sets, in particular the roots q(d) = 1.
• TauCeti.titsPolarForm_eq_zero_of_vertexPreReflectionList_eq_self: a vector fixed by the composite along a repetition-free word in all the vertices lies in the radical of the polarized Tits form.
• TauCeti.vertexPreReflectionList_eq_self_iff: consequently, once that radical is trivial the only fixed vector is 0; TauCeti.vertexPreReflectionList_eq_self_iff_of_anisotropic is the same statement for an anisotropic Tits form.

References

See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations.

noncomputable def TauCeti.vertexPreReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (l : List Q) : Module.End ℤ (Q → ℤ)

The composite of the simple reflections at the vertices of a word, applied in the order in which they are listed, so that l = [i₁, …, iₙ] gives sᵢₙ ∘ ⋯ ∘ sᵢ₁. Over a repetition-free word running through all the vertices this is the Coxeter transformation.

No hypothesis on the vertices is imposed here, following TauCeti.vertexPreReflection; over a word in loopless vertices TauCeti.vertexReflectionList packages this map as an automorphism.

@[simp]

theorem TauCeti.vertexPreReflectionList_nil (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] : vertexPreReflectionList Q [] = 1

@[simp]

theorem TauCeti.vertexPreReflectionList_cons (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (i : Q) (l : List Q) : vertexPreReflectionList Q (i :: l) = vertexPreReflectionList Q l * vertexPreReflection Q i

The vertex at the head of the word is reflected first.

theorem TauCeti.vertexPreReflectionList_apply_cons (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (i : Q) (l : List Q) (d : Q → ℤ) : (vertexPreReflectionList Q (i :: l)) d = (vertexPreReflectionList Q l) ((vertexPreReflection Q i) d)

The vertex at the head of the word is reflected first, in applied form.

theorem TauCeti.vertexPreReflectionList_reflectAt (Q : Type u) [Fintype Q] [DecidableEq Q] (q : Quiver Q) (hq : (a b : Q) → Fintype (a ⟶ b)) (i : Q) (l : List Q) : vertexPreReflectionList Q l = vertexPreReflectionList Q l

The composite of the simple reflections along a word is unchanged by reflecting the quiver structure at a vertex.

theorem TauCeti.vertexPreReflectionList_reflectList (Q : Type u) [Fintype Q] [DecidableEq Q] (l' : List Q) (q : Quiver Q) (hq : (a b : Q) → Fintype (a ⟶ b)) (l : List Q) : vertexPreReflectionList Q l = vertexPreReflectionList Q l

The composite of the simple reflections along a word is unchanged by reflecting the quiver structure along another word: the word-level form of TauCeti.vertexPreReflectionList_reflectAt.

theorem TauCeti.vertexPreReflectionList_append (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (l₁ l₂ : List Q) : vertexPreReflectionList Q (l₁ ++ l₂) = vertexPreReflectionList Q l₂ * vertexPreReflectionList Q l₁

Concatenating two words composes their reflection products, the first word acting first.

@[simp]

theorem TauCeti.vertexPreReflectionList_flatten_replicate (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (l : List Q) (N : ℕ) : vertexPreReflectionList Q (List.replicate N l).flatten = vertexPreReflectionList Q l ^ N

Repeating a word N times raises its reflection product to the N-th power.

theorem TauCeti.nonneg_vertexPreReflectionList_take_append (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {d : Q → ℤ} {l₁ l₂ : List Q} (h₁ : ∀ r ≤ l₁.length, 0 ≤ (vertexPreReflectionList Q (List.take r l₁)) d) (h₂ : ∀ r ≤ l₂.length, 0 ≤ (vertexPreReflectionList Q (List.take r l₂)) ((vertexPreReflectionList Q l₁) d)) (r : ℕ) : r ≤ (l₁ ++ l₂).length → 0 ≤ (vertexPreReflectionList Q (List.take r (l₁ ++ l₂))) d

Nonnegativity of every intermediate vector along a concatenation follows from nonnegativity along each of the two segments.

theorem TauCeti.nonneg_vertexPreReflectionList_take_flatten_replicate (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {d : Q → ℤ} (hd : 0 ≤ d) {l : List Q} (N : ℕ) : (∀ p < N, ∀ r ≤ l.length, 0 ≤ (vertexPreReflectionList Q (List.take r l)) ((vertexPreReflectionList Q l ^ p) d)) → ∀ r ≤ (List.replicate N l).flatten.length, 0 ≤ (vertexPreReflectionList Q (List.take r (List.replicate N l).flatten)) d

Nonnegativity of every intermediate vector along a repeated word follows from nonnegativity along each of its passes.

@[simp]

theorem TauCeti.vertexPreReflectionList_apply_of_notMem (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} {i : Q} (hi : i ∉ l) (d : Q → ℤ) : (vertexPreReflectionList Q l) d i = d i

Off the word, the reflection product changes no coordinate: each simple reflection in the composite alters only the coordinate at its own vertex.

Invariance of the Tits form

theorem TauCeti.titsForm_vertexPreReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) (d : Q → ℤ) : (titsForm Q) ((vertexPreReflectionList Q l) d) = (titsForm Q) d

The reflection product along a word in loopless vertices preserves the Tits form.

theorem TauCeti.titsPolarForm_vertexPreReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) (d e : Q → ℤ) : ((titsPolarForm Q) ((vertexPreReflectionList Q l) d)) ((vertexPreReflectionList Q l) e) = ((titsPolarForm Q) d) e

The reflection product along a word in loopless vertices preserves the polarized Tits form.

The Coxeter transformation as an automorphism

noncomputable def TauCeti.vertexReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : (Q → ℤ) ≃ₗ[ℤ] Q → ℤ

The reflection product along a word in loopless vertices, as a linear automorphism of the dimension-vector lattice; over a repetition-free word running through all the vertices this is the Coxeter transformation.

@[simp]

theorem TauCeti.coe_vertexReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : ⇑(vertexReflectionList Q hl) = ⇑(vertexPreReflectionList Q l)

Coercing the reflection automorphism along a word to a function gives the corresponding pre-reflection product.

theorem TauCeti.vertexPreReflectionList_bijective (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : Function.Bijective ⇑(vertexPreReflectionList Q l)

The reflection product along a word in loopless vertices is bijective.

theorem TauCeti.coe_vertexReflectionList_symm (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : ⇑(vertexReflectionList Q hl).symm = ⇑(vertexPreReflectionList Q l.reverse)

The inverse automorphism is the reflection product along the reversed word.

@[simp]

theorem TauCeti.vertexReflectionList_symm (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : (vertexReflectionList Q hl).symm = vertexReflectionList Q ⋯

The inverse reflection automorphism along a word is the reflection automorphism along the reversed word.

theorem TauCeti.vertexPreReflectionList_reverse_mul (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : vertexPreReflectionList Q l.reverse * vertexPreReflectionList Q l = 1

Composing the pre-reflection lists for a word and its reverse gives the identity.

theorem TauCeti.vertexPreReflectionList_mul_reverse (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) : vertexPreReflectionList Q l * vertexPreReflectionList Q l.reverse = 1

Composing the pre-reflection lists for a word and its reverse in the other order also gives the identity.

theorem TauCeti.vertexPreReflectionList_reverse_apply_append (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l₂ : List Q} (hl₂ : ∀ i ∈ l₂, IsEmpty (i ⟶ i)) (l₁ : List Q) (d : Q → ℤ) : (vertexPreReflectionList Q l₂.reverse) ((vertexPreReflectionList Q (l₁ ++ l₂)) d) = (vertexPreReflectionList Q l₁) d

Undoing the reflections of a word in reverse order returns the vector the word started from.

theorem TauCeti.nonneg_vertexPreReflectionList_take_reverse (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) {d : Q → ℤ} (h : ∀ r ≤ l.length, 0 ≤ (vertexPreReflectionList Q (List.take r l)) d) (s : ℕ) : s ≤ l.length → 0 ≤ (vertexPreReflectionList Q (List.take s l.reverse)) ((vertexPreReflectionList Q l) d)

Reading a nonnegative reflection word backwards stays nonnegative. If every intermediate vector of the word l applied to d is nonnegative, then every intermediate vector of the reversed word applied to the endpoint sˡ d is nonnegative, being one of the vectors of the forward chain. This is the hypothesis the source-reflection composite of TauCeti.indecomposable_and_dimVector_sourceReflectionFunctorList asks for.

theorem TauCeti.bijOn_vertexPreReflectionList (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hl : ∀ i ∈ l, IsEmpty (i ⟶ i)) (n : ℤ) : Set.BijOn ⇑(vertexPreReflectionList Q l) {d : Q → ℤ | (titsForm Q) d = n} {d : Q → ℤ | (titsForm Q) d = n}

The reflection product along a word in loopless vertices permutes every level set of the Tits form; at the level 1 this says that it permutes the roots of Q.

Fixed vectors

theorem TauCeti.titsPolarForm_single_eq_zero_of_vertexPreReflectionList_eq_self (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hnd : l.Nodup) {v : Q → ℤ} (hv : (vertexPreReflectionList Q l) v = v) {i : Q} (hi : i ∈ l) : ((titsPolarForm Q) (Pi.single i 1)) v = 0

A vector fixed by the reflection product along a repetition-free word is orthogonal, for the polarized Tits form, to the simple dimension vector at every vertex of that word.

theorem TauCeti.titsPolarForm_eq_zero_of_vertexPreReflectionList_eq_self (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] {l : List Q} (hnd : l.Nodup) (hmem : ∀ (i : Q), i ∈ l) {v : Q → ℤ} (hv : (vertexPreReflectionList Q l) v = v) (d : Q → ℤ) : ((titsPolarForm Q) d) v = 0

A vector fixed by the reflection product along a repetition-free word in all the vertices lies in the radical of the polarized Tits form.

theorem TauCeti.vertexPreReflectionList_eq_self_iff (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hsep : LinearMap.SeparatingRight (titsPolarForm Q)) {l : List Q} (hnd : l.Nodup) (hmem : ∀ (i : Q), i ∈ l) (v : Q → ℤ) : (vertexPreReflectionList Q l) v = v ↔ v = 0

The Coxeter transformation of a quiver whose polarized Tits form has trivial radical fixes only the zero vector, as soon as the word of vertices it is taken along is repetition-free and exhausts the vertices.

This fixed-point obstruction is one input to the reflection induction behind Gabriel's theorem: no nonzero dimension vector survives a full pass of the Coxeter functor unchanged. For a positive definite Tits form, TauCeti.exists_vertexPreReflectionList_pow_apply_neg combines this obstruction with a finite-orbit argument to supply the descent without a separate root-height argument. An anisotropic Tits form has trivial radical, which is the form the hypothesis takes in TauCeti.vertexPreReflectionList_eq_self_iff_of_anisotropic.

theorem TauCeti.vertexPreReflectionList_eq_self_iff_of_anisotropic (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hani : (titsForm Q).Anisotropic) {l : List Q} (hnd : l.Nodup) (hmem : ∀ (i : Q), i ∈ l) (v : Q → ℤ) : (vertexPreReflectionList Q l) v = v ↔ v = 0

The Coxeter transformation of a quiver with anisotropic Tits form fixes only the zero vector: a vector in the radical of the polarized form is isotropic, since ⟨v, v⟩ = 2 q(v).

For a quiver of ADE type the Tits form is positive definite, and QuadraticMap.PosDef.anisotropic supplies the hypothesis.