Euler and Tits forms of a finite quiver #
The Euler form records the oriented incidence data of a finite quiver. Its diagonal, the Tits form, is the numerical form used by reflection functors and Gabriel's theorem.
TauCeti.eulerForm_card_path_left evaluates the Euler form against the vector counting the paths
out of a vertex i: it is evaluation at i, the last-arrow recursion for path counts cancelling
the arrow sum. TauCeti.eulerForm_card_path_right is the mirror statement on the right-hand
argument, for the vector counting the paths into a vertex, and rests on the first-arrow recursion
instead.
The last section evaluates both forms on the simple dimension vectors αᵢ = Pi.single i 1;
in particular TauCeti.titsPolarForm_single_single computes the Gram matrix of the polarized
Tits form as 2·I - (A + Aᵀ), for A the matrix of arrow counts, and
TauCeti.titsForm_posDef_iff_posDef_toMatrix says that the Tits form is positive definite exactly
when this matrix is. When there is no loop and at most one arrow between any two vertices, counting
both directions, A + Aᵀ is the adjacency matrix of the underlying graph, so the Gram matrix is
the matrix 2I - A of that graph (TauCeti.toMatrix_titsPolarForm_eq_graphCartanMatrix), and
positive definiteness of the Tits form is a property of the underlying graph alone
(TauCeti.titsForm_posDef_iff_posDef_graphCartanMatrix). A positive definite Tits form forces this
arrow condition (TauCeti.card_hom_add_card_hom_le_one_of_titsForm_posDef).
The definitions follow the Layer 4 signatures in
TauCetiRoadmap/TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/Suggested.lean.
See Derksen--Weyman, An Introduction to Quiver Representations.
The Euler (or Ringel) form of a finite quiver. Arrows are counted with multiplicity.
Equations
- TauCeti.eulerForm Q = LinearMap.mk₂ ℤ (fun (d e : Q → ℤ) => ∑ v : Q, d v * e v - ∑ a : Q, ∑ b : Q, ∑ x : a ⟶ b, d a * e b) ⋯ ⋯ ⋯ ⋯
Instances For
The Tits form of a finite quiver, the diagonal of its Euler form.
Equations
Instances For
The symmetric bilinear form obtained by polarizing the Tits form.
Equations
Instances For
The Euler form against a path-count vector #
The Euler form against a path-count vector is evaluation. Pairing the vector counting the
paths out of i against any e : Q → ℤ returns eᵢ: at each vertex b the path count #(i → b)
cancels the arrow-weighted sum ∑ₐ #(a ⟶ b) · #(i → a) up to the trivial path, by the last-arrow
recursion TauCeti.card_path_eq_ite_add_sum.
The Euler form against a path-count vector on the right is evaluation. Pairing any
d : Q → ℤ against the vector counting the paths into i returns dᵢ: at each vertex a the path
count #(a → i) cancels the arrow-weighted sum ∑_b #(a ⟶ b) · #(b → i) up to the trivial path, by
the first-arrow recursion TauCeti.card_path_eq_ite_add_sum_firstArrow. This is the mirror image of
TauCeti.eulerForm_card_path_left, and the Euler form is not symmetric, so neither statement
follows from the other.
The Euler and Tits forms in the simple dimension vectors #
The Euler form with a simple dimension vector on the left counts the arrows out of i.
The Euler form with a simple dimension vector on the right counts the arrows into j.
The Euler form in the simple dimension vectors: ⟨αᵢ, αⱼ⟩ = δᵢⱼ - #(i ⟶ j).
The Tits form of a simple dimension vector is one minus the number of loops at that vertex.
The polarized Tits form against a simple dimension vector, in coordinates.
The polarized Tits form against a simple dimension vector on the right, in coordinates.
The Gram matrix of the polarized Tits form in the simple dimension vectors is
2·I - (A + Aᵀ), for A the matrix of arrow counts: the symmetrized Cartan matrix of Q.
A loopless vertex has ⟨αᵢ, αᵢ⟩ = 2 for the polarized Tits form: the normalization that
makes the simple reflection at i an involution.
The Tits form is positive definite exactly when the Gram matrix 2·I - (A + Aᵀ) of its
polarization is, the matrix being taken in the simple dimension vectors, as computed by
TauCeti.titsPolarForm_single_single. The polarized form takes the value 2 q(d) at (d, d).
A positive definite Tits form allows at most one arrow between two vertices, counting both
directions, and no loop: q(αᵢ + αⱼ) = 2 - #(i ⟶ j) - #(j ⟶ i) for distinct i and j, and
q(αᵢ) = 1 - #(i ⟶ i).
The Gram matrix of the Tits form of a simple quiver is 2I - A of its underlying graph. If
there is no loop and at most one arrow between any two vertices, counting both directions, then the
matrix 2·I - (A + Aᵀ) of the polarized Tits form in the simple dimension vectors is the matrix
2I - A of the underlying graph.
For a simple quiver the Tits form is positive definite exactly when 2I - A of the
underlying graph is. If there is no loop and at most one arrow between any two vertices, counting
both directions, then twice the Tits form is the form of the matrix 2I - A of the underlying
graph (TauCeti.toMatrix_titsPolarForm_eq_graphCartanMatrix).