Documentation

TauCeti.RepresentationTheory.Quiver.Preprojective.Koszul.NonDynkin

Koszulity of the preprojective algebras of non-Dynkin quivers #

Let Π = Π_k(Q) be the preprojective algebra of a finite quiver over a field k. The Koszul complex of the vertex module S_v,

0 ⟶ e_v Π ⟶ ⨁_{b : w ⟶ v} e_w Π ⟶ e_v Π ⟶ S_v ⟶ 0,

is exact except possibly at its left end, whose defect consists of the y ∈ e_v Π killed by every arrow b* of the doubled quiver leaving v. A connected simple graph which is not a Dynkin diagram carries, in every orientation, a positive superadditive weight: a weight δ on the vertices of the oriented quiver with δ_i > 0 and 2 δ_i ≤ ∑_j (#(i ⟶ j) + #(j ⟶ i)) δ_j at every vertex (TauCeti.exists_pos_two_mul_le_sum_orientedQuiver_of_not_exists_dynkinType_iso). Such a weight makes the quiver-level Koszul machinery of TauCeti.forall_preprojectiveMk_ofArrow_reverse_mul_eq_zero_iff_of_two_mul_le_sum (Koszul/Superadditive.lean) exact, so for every orientation of a connected non-Dynkin graph, trees such as D~ₙ, E₆~, E₇~ and E₈~ included, the Koszul complexes are projective resolutions and the matrix Hilbert series of Π is ((1 + t²) I - t A)⁻¹. This is the theorem of Etingof and Eu; for orientations of graphs which are not trees it is already TauCeti.forall_preprojectiveMk_ofArrow_reverse_mul_eq_zero_iff_of_not_isAcyclic.

Main results #

References #

source
theorem TauCeti.exists_pos_two_mul_le_sum_orientedQuiver_of_not_exists_dynkinType_iso {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) :
∃ (δ : DoubledQuiver.OrientedQuiver G o → ℝ), (∀ (i : DoubledQuiver.OrientedQuiver G o), 0 < δ i) ∧ ∀ (i : DoubledQuiver.OrientedQuiver G o), 2 * δ i ≤ ∑ j : DoubledQuiver.OrientedQuiver G o, ↑(Fintype.card (i ⟶ j) + Fintype.card (j ⟶ i)) * δ j

Every orientation of a connected non-Dynkin graph carries a positive weight on its oriented quiver which is positive at every vertex and superadditive on its underlying multigraph.

source
theorem TauCeti.forall_preprojectiveMk_ofArrow_reverse_mul_eq_zero_iff_of_not_exists_dynkinType_iso (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) (v : DoubledQuiver.OrientedQuiver G o) {y : preprojectiveAlgebra k (DoubledQuiver.OrientedQuiver G o)} (hy : (preprojectiveMk k (DoubledQuiver.OrientedQuiver G o)) (doubledVertexIdempotent k v) * y = y) :
(∀ (w : Quiver.Symmetrify (DoubledQuiver.OrientedQuiver G o)) (b : w ⟶ Quiver.Symmetrify.of.obj v), (preprojectiveMk k (DoubledQuiver.OrientedQuiver G o)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) ↔ y = 0

Exactness of the Koszul complex at its left end, for a connected non-Dynkin graph. Let G be a connected finite simple graph which is not isomorphic to the diagram of any valid Dynkin type, and o any orientation of G. If y = e_v y in the preprojective algebra of o over a field k, then b* y = 0 for every arrow b of the doubled quiver into v exactly when y = 0. This covers the non-Dynkin trees, such as the affine diagrams D~ₙ, E₆~, E₇~ and E₈~.

source
theorem TauCeti.preprojectiveKoszulLeft_injective_of_not_exists_dynkinType_iso (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) (v : DoubledQuiver.OrientedQuiver G o) :
Function.Injective ⇑(preprojectiveKoszulLeft k v)

For every orientation of a connected non-Dynkin graph, the left Koszul differential at each vertex is injective.

source
theorem TauCeti.isLinear_preprojectiveGradedKoszulResolution_of_not_exists_dynkinType_iso (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) (v : DoubledQuiver.OrientedQuiver G o) :
(preprojectiveGradedKoszulResolution k v ⋯).IsLinear

The right vertex module of every orientation of a connected non-Dynkin graph has a linear graded Koszul resolution. Its projective terms are generated in internal degrees zero, one and two, respectively, and all later terms vanish.

source
theorem TauCeti.mul_preprojectiveHilbertSeries_eq_one_of_not_exists_dynkinType_iso (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) [DecidableEq (DoubledQuiver.OrientedQuiver G o)] :
((1 + PowerSeries.X ^ 2) • 1 - PowerSeries.X • Matrix.of fun (v w : DoubledQuiver.OrientedQuiver G o) => ↑(Fintype.card (Quiver.Symmetrify.of.obj w ⟶ Quiver.Symmetrify.of.obj v))) * preprojectiveHilbertSeries k (DoubledQuiver.OrientedQuiver G o) = 1

For every orientation of a connected non-Dynkin graph, ((1 + X²) I - X A) H = I, where A counts doubled arrows and H is the matrix Hilbert series of the preprojective algebra.

source
theorem TauCeti.preprojectiveHilbertSeries_eq_inv_of_not_exists_dynkinType_iso (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (hD : ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)) (o : DoubledQuiver.Orientation G) [DecidableEq (DoubledQuiver.OrientedQuiver G o)] :
preprojectiveHilbertSeries k (DoubledQuiver.OrientedQuiver G o) = ((1 + PowerSeries.X ^ 2) • 1 - PowerSeries.X • Matrix.of fun (v w : DoubledQuiver.OrientedQuiver G o) => ↑(Fintype.card (Quiver.Symmetrify.of.obj w ⟶ Quiver.Symmetrify.of.obj v)))⁻¹

The Hilbert series of the preprojective algebra of a connected non-Dynkin graph. For every orientation of a connected finite simple graph which is not a Dynkin diagram, the matrix Hilbert series of its preprojective algebra over any field is ((1 + X²) I - X A)⁻¹.

source
theorem TauCeti.exists_not_preprojectiveKoszulLeft_injective_of_finiteDimensional (k : Type w) [Field k] {Q : Type u_1} [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] [Nonempty Q] [FiniteDimensional k (preprojectiveAlgebra k Q)] :
∃ (v : Q), ¬Function.Injective ⇑(preprojectiveKoszulLeft k v)

For a nonempty finite quiver whose preprojective algebra is finite-dimensional, the left Koszul differential fails to be injective at some vertex.

source
theorem TauCeti.forall_preprojectiveKoszulLeft_injective_iff (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (o : DoubledQuiver.Orientation G) :
(∀ (v : DoubledQuiver.OrientedQuiver G o), Function.Injective ⇑(preprojectiveKoszulLeft k v)) ↔ ¬∃ (t : DynkinType), t.Valid ∧ Nonempty (G ≃g diagramGraph t.cartanMatrix)

The Koszulity dichotomy for preprojective algebras of oriented graphs: for a connected finite simple graph G and any orientation o of G, the left Koszul differential of Π_k(OrientedQuiver G o) is injective at every vertex if and only if G is not isomorphic to the diagram of any valid Dynkin type.

source
theorem TauCeti.forall_preprojectiveKoszulLeft_injective_iff_not_finiteDimensional (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Connected) (o : DoubledQuiver.Orientation G) :
(∀ (v : DoubledQuiver.OrientedQuiver G o), Function.Injective ⇑(preprojectiveKoszulLeft k v)) ↔ ¬FiniteDimensional k (preprojectiveAlgebra k (DoubledQuiver.OrientedQuiver G o))

For a connected finite simple graph G and any orientation o of G, the left Koszul differential of Π_k(OrientedQuiver G o) is injective at every vertex if and only if Π_k(OrientedQuiver G o) is infinite-dimensional.