The Koszul resolution of a zigzag simple module

Let Z be the zigzag relation quotient TauCeti.nonisolatedZigzagQuotient of a finite graph G, graded by path length, and let Π be the signless preprojective algebra of the doubled quiver, the quadratic dual of the quadratic zigzag presentation. The Koszul complex K of the simple Z-module at a vertex v, with terms K_n = ⨁_u Hom_k(e_u Π_n e_v, Z e_u), is exact in every positive homological degree when every signless vertex Koszul complex 0 → e_w Π → ⨁_{j ∼ w} e_j Π is exact at its left end (TauCeti.range_zigzagKoszulDifferential_eq_ker). This file completes K to a linear graded projective resolution of the graded simple module S_v (TauCeti.zigzagGradedSimple).

• Grading. A map f ∈ K_n has degree p when its values have degree p - n. Evaluation on bases of the finite-dimensional corners e_u Π_n e_v identifies K_n with a finite direct sum of vertex projectives Z e_u, which makes this an internal grading and K_n a projective module. The term K_n is generated in degree n, by the maps with values in the lines of the vertex idempotents, and the differential preserves degrees because arrows have degree one.
• Augmentation. Since e_v Π_0 e_v is the line of e_v and e_u Π_0 e_v = 0 for u ≠ v, an element f ∈ K_0 is determined by f_v(e_v) ∈ Z e_v, and the augmentation sends f to the class of f_v(e_v) in the head S_v of Z e_v. Every arrow out of v, and the volume class at v, is the value (d g)_v(e_v) of a boundary, because the arrows of Π are nonzero; so the boundaries account for the whole radical of Z e_v, which is the kernel of the augmentation.

Hence S_v has a linear resolution whenever the signless Koszul complexes are exact at their left ends; a non-backtracking choice of neighbours provides this for every connected graph which is not a tree. For such graphs every vertex simple module S_v, concentrated in degree zero, has a linear resolution, and its grading shifts have the correspondingly shifted resolutions; this is Koszulity in the sense of Beilinson--Ginzburg--Soergel. Through TauCeti.coeff_inv_zigzagGradedCartanMatrix_map_aeval_neg_X_eq, the multiplicities of these resolutions are the coefficients of the inverse graded Cartan matrix C_G(-X)⁻¹.

Main definitions

• TauCeti.zigzagKoszulTermGrading: the internal grading of K_n.
• TauCeti.zigzagKoszulAugmentation: the augmentation K_0 → S_v.
• TauCeti.zigzagKoszulResolution: the graded projective resolution of S_v by K.

Main results

• TauCeti.mem_zigzagKoszulTermGrading_piece_iff: the homogeneous pieces of K_n.
• TauCeti.isHomogeneous_zigzagKoszulDifferential and TauCeti.isHomogeneous_zigzagKoszulAugmentation: the maps preserve internal degree.
• TauCeti.isGeneratedInDegree_zigzagKoszulTermGrading: K_n is generated in degree n.
• TauCeti.exact_zigzagKoszulDifferential_zigzagKoszulAugmentation: exactness at K_0.
• TauCeti.isLinear_zigzagKoszulResolution: the Koszul resolution is linear.
• TauCeti.exists_isLinear_gradedProjectiveResolution_zigzagGradedSimple_of_not_isAcyclic: the vertex simple modules, concentrated in degree zero, of the zigzag algebra of a connected graph which is not a tree have linear resolutions.

References

• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, J. Amer. Math. Soc. 9 (1996), Sections 1.2 and 2, for linear resolutions and the Koszul complex.
• R. S. Huerfano and M. Khovanov, A category for the adjoint representation, J. Algebra 246 (2001), Section 3, for the zigzag algebra and its quadratic dual.
• P. Etingof and C.-H. Eu, Koszulity and the Hilbert series of preprojective algebras, Math. Res. Lett. 14 (2007), Sections 2 and 3, for the vertex Koszul complexes of Π.

The terms as direct sums of vertex projectives

The internal grading

noncomputable def TauCeti.zigzagKoszulTermGrading (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : InternalGrading k (ZigzagKoszulTerm k G v n) ℤ

The internal grading of the Koszul term K_n = ⨁_u Hom_k(e_u Π_n e_v, Z e_u): a map has degree p when it takes values in degree p - n of the vertex projectives, so that K_n is the direct sum of the shifted projectives Z e_u{n} tensored with the dual corners.

@[simp]

theorem TauCeti.mem_zigzagKoszulTermGrading_piece_iff (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {v : V} {n : ℕ} {p : ℤ} {f : ZigzagKoszulTerm k G v n} : f ∈ (zigzagKoszulTermGrading k G v n).piece ℤ p ↔ ∀ (u : V) (y : ↥(signlessPreprojectiveCorner k (DoubledQuiver G) n (DoubledQuiver.vertex G v) (DoubledQuiver.vertex G u))), (f u) y ∈ zigzagProjectiveGrade k G u (p - ↑n)

A map in K_n has degree p exactly when all its values have degree p - n.

@[instance_reducible]

noncomputable def TauCeti.instSMulNonisolatedZigzagQuotientZigzagKoszulTerm (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : SMul (nonisolatedZigzagQuotient k G) (ZigzagKoszulTerm k G v n)

The scalar action of the zigzag algebra on the Koszul terms, read off from their module structure. Synthesizing it directly, through the actions on Pi types and on linear maps, exceeds the default instance-search budget.

instance TauCeti.instGradedSMulIntSubmoduleNonisolatedZigzagQuotientZigzagKoszulTermZigzagIntegerGradePieceZigzagKoszulTermGrading (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : SetLike.GradedSMul (zigzagIntegerGrade k G) ((zigzagKoszulTermGrading k G v n).piece ℤ)

The Koszul terms are graded modules over the path-length graded zigzag algebra.

instance TauCeti.instProjectiveNonisolatedZigzagQuotientZigzagKoszulTerm (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : Module.Projective (nonisolatedZigzagQuotient k G) (ZigzagKoszulTerm k G v n)

The Koszul terms are projective modules over the zigzag algebra.

theorem TauCeti.isHomogeneous_zigzagKoszulDifferential (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : LinearMap.IsHomogeneous (zigzagKoszulDifferential k G v n) ((zigzagKoszulTermGrading k G v (n + 1)).piece ℤ) ((zigzagKoszulTermGrading k G v n).piece ℤ) 0

The Koszul differential preserves internal degree.

theorem TauCeti.isGeneratedInDegree_zigzagKoszulTermGrading (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (n : ℕ) : (zigzagKoszulTermGrading k G v n).IsGeneratedInDegree (nonisolatedZigzagQuotient k G) ↑n

The Koszul term K_n is generated in degree n: it is a direct sum of shifted vertex projectives Z e_u{n}, each generated by its vertex idempotent e_u.

The augmentation

noncomputable def TauCeti.zigzagKoszulAugmentation (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : ZigzagKoszulTerm k G v 0 →ₗ[nonisolatedZigzagQuotient k G] (zigzagGradedSimple k G v).carrier

The augmentation K_0 → S_v of the Koszul complex onto the graded simple module at v: the class in the head of Z e_v of the value at the vertex idempotent e_v ∈ e_v Π_0 e_v.

theorem TauCeti.zigzagKoszulAugmentation_apply (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) (f : ZigzagKoszulTerm k G v 0) : (zigzagKoszulAugmentation k G v) f = (zigzagGradedSimpleMk k G v) ⟨↑((f v) ⟨(signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G v)), ⋯⟩), ⋯⟩

The augmentation sends f to the class of f_v (e_v).

theorem TauCeti.isHomogeneous_zigzagKoszulAugmentation (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : LinearMap.IsHomogeneous (zigzagKoszulAugmentation k G v) ((zigzagKoszulTermGrading k G v 0).piece ℤ) ((zigzagGradedSimple k G v).grading.piece ℤ) 0

The augmentation preserves internal degree.

@[simp]

theorem TauCeti.zigzagKoszulAugmentation_comp_zigzagKoszulDifferential (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : zigzagKoszulAugmentation k G v ∘ₗ zigzagKoszulDifferential k G v 0 = 0

The augmentation kills the boundaries: K_1 → K_0 → S_v composes to zero.

theorem TauCeti.exact_zigzagKoszulDifferential_zigzagKoszulAugmentation (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : Function.Exact ⇑(zigzagKoszulDifferential k G v 0) ⇑(zigzagKoszulAugmentation k G v)

Exactness of the Koszul complex at K_0: the kernel of the augmentation is the image of the first differential.

theorem TauCeti.zigzagKoszulAugmentation_surjective (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : Function.Surjective ⇑(zigzagKoszulAugmentation k G v)

The augmentation is onto the graded simple module.

The linear Koszul resolution

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagKoszulResolution (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) : GradedProjectiveResolution (zigzagIntegerGrade k G) (zigzagGradedSimple k G v).grading

The Koszul resolution of a graded simple zigzag module. Let G be a finite graph such that the Koszul complex 0 → e_w Π → ⨁_{j ∼ w} e_j Π of the signless preprojective algebra Π is exact at its left end at every vertex w. Then the Koszul complex K of the graded simple module S_v of the zigzag algebra, with its augmentation K_0 → S_v, is a graded projective resolution of S_v.

This is an abbreviation so that the types and module instances of its terms are those of TauCeti.ZigzagKoszulTerm; its data are computed by the [simp] lemmas below.

@[simp]

theorem TauCeti.zigzagKoszulResolution_X (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) (n : ℕ) : (zigzagKoszulResolution k G hinj v).X n = ZigzagKoszulTerm k G v n

The terms of the Koszul resolution are the Koszul terms.

@[simp]

theorem TauCeti.zigzagKoszulResolution_grading (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) (n : ℕ) : (zigzagKoszulResolution k G hinj v).grading n = zigzagKoszulTermGrading k G v n

The terms of the Koszul resolution carry the gradings TauCeti.zigzagKoszulTermGrading.

@[simp]

theorem TauCeti.zigzagKoszulResolution_d (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) (n : ℕ) : (zigzagKoszulResolution k G hinj v).d n = zigzagKoszulDifferential k G v n

The differentials of the Koszul resolution are the Koszul differentials.

@[simp]

theorem TauCeti.zigzagKoszulResolution_π (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) : (zigzagKoszulResolution k G hinj v).π = zigzagKoszulAugmentation k G v

The augmentation of the Koszul resolution is TauCeti.zigzagKoszulAugmentation.

theorem TauCeti.isLinear_zigzagKoszulResolution (k : Type w) [Field k] {V : Type u} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hinj : ∀ (w : V) (y : signlessPreprojectiveAlgebra k (DoubledQuiver G)), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G w)) * y = y → (∀ (i : DoubledQuiver G) (b : i ⟶ DoubledQuiver.vertex G w), (signlessPreprojectiveMk k (DoubledQuiver G)) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0) (v : V) : (zigzagKoszulResolution k G hinj v).IsLinear

The Koszul resolution is linear: its term in homological degree n is generated in internal degree n.

theorem TauCeti.exists_isLinear_gradedProjectiveResolution_zigzagGradedSimple_of_not_isAcyclic (k : Type w) [Field k] {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.Preconnected) (hc : ¬G.IsAcyclic) (v : V) : ∃ (r : GradedProjectiveResolution (zigzagIntegerGrade k G) (zigzagGradedSimple k G v).grading), r.IsLinear

The vertex simple modules of the zigzag algebra of a connected graph which is not a tree have linear resolutions: the simple module S_v, concentrated in degree zero, has the linear resolution TauCeti.zigzagKoszulResolution, since a non-backtracking choice of neighbours makes the signless Koszul complexes exact at their left ends. Its grading shifts have the correspondingly shifted resolutions. Such a graph is never a finite ADE Dynkin diagram.