The graded preprojective Koszul resolution

The right vertex projectives of a preprojective algebra inherit the path-length grading. The Koszul differentials multiply by arrows and therefore raise path degree by one. Shifting the middle projective by one and the left projective by two makes the differentials homogeneous of degree zero. For quivers without sinks these terms give a linear graded projective resolution of the vertex augmentation module.

Right modules are left modules over the ordinary opposite algebra, without a Koszul sign. The internal shifts are implemented by InternalGrading.shift (-n), so generators of the term in homological degree n have internal degree n.

References

• P. Etingof and C.-H. Eu, Koszulity and the Hilbert series of preprojective algebras, Math. Res. Lett. 14 (2007), Sections 2 and 3.

theorem TauCeti.isHomogeneous_preprojectiveRightProjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : DirectSum.SetLike.IsHomogeneous (preprojectiveIntegerGrade k) (Submodule.restrictScalars k (preprojectiveRightProjective k i))

The right vertex ideal is homogeneous: projection commutes with left multiplication by its degree-zero idempotent.

noncomputable def TauCeti.preprojectiveRightProjectiveGrading (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : InternalGrading k ↥(preprojectiveRightProjective k i) ℤ

The internal grading on e_i Π, restricted from the actual preprojective algebra.

@[simp]

theorem TauCeti.mem_preprojectiveRightProjectiveGrading_piece_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) (p : ℤ) (x : ↥(preprojectiveRightProjective k i)) : x ∈ (preprojectiveRightProjectiveGrading k i).piece ℤ p ↔ ↑x ∈ preprojectiveIntegerGrade k p

Homogeneity in the right vertex ideal is homogeneity of its underlying path class.

instance TauCeti.preprojectiveRightProjective_gradedSMul (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : SetLike.GradedSMul ((preprojectiveInternalGrading k).opposite.piece ℤ) ((preprojectiveRightProjectiveGrading k i).piece ℤ)

Right multiplication respects the restricted path-length grading.

theorem TauCeti.isGeneratedInDegree_preprojectiveRightProjectiveGrading (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : (preprojectiveRightProjectiveGrading k i).IsGeneratedInDegree (preprojectiveAlgebra k Q)ᵐᵒᵖ 0

Every right vertex projective is generated by its degree-zero idempotent.

noncomputable def TauCeti.preprojectiveKoszulMiddleGrading (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : InternalGrading k (preprojectiveKoszulMiddle k v) ℤ

The middle Koszul term with the componentwise path grading.

@[simp]

theorem TauCeti.mem_preprojectiveKoszulMiddleGrading_piece_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (p : ℤ) (x : preprojectiveKoszulMiddle k v) : x ∈ (preprojectiveKoszulMiddleGrading k v).piece ℤ p ↔ ∀ (i : Quiver.Symmetrify Q) (b : i ⟶ Quiver.Symmetrify.of.obj v), ↑(x i b) ∈ preprojectiveIntegerGrade k p

The path degree in the middle Koszul term is tested in each arrow-indexed component.

theorem TauCeti.isHomogeneous_preprojectiveKoszulLeft (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : LinearMap.IsHomogeneous (preprojectiveKoszulLeft k v) ((preprojectiveRightProjectiveGrading k (Quiver.Symmetrify.of.obj v)).piece ℤ) ((preprojectiveKoszulMiddleGrading k v).piece ℤ) 1

The left Koszul differential raises path degree by one.

theorem TauCeti.isHomogeneous_preprojectiveKoszulRight (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : LinearMap.IsHomogeneous (preprojectiveKoszulRight k v) ((preprojectiveKoszulMiddleGrading k v).piece ℤ) ((preprojectiveRightProjectiveGrading k (Quiver.Symmetrify.of.obj v)).piece ℤ) 1

The right Koszul differential raises path degree by one.

instance TauCeti.preprojectiveKoszulMiddle_gradedSMul (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : SetLike.GradedSMul ((preprojectiveInternalGrading k).opposite.piece ℤ) ((preprojectiveKoszulMiddleGrading k v).piece ℤ)

Right multiplication respects the arrow-indexed grading of the middle Koszul term.

theorem TauCeti.isGeneratedInDegree_preprojectiveKoszulMiddleGrading (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveKoszulMiddleGrading k v).IsGeneratedInDegree (preprojectiveAlgebra k Q)ᵐᵒᵖ 0

The unshifted middle Koszul term is generated in path degree zero.

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedRightProjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : GradedModuleCat ((preprojectiveInternalGrading k).opposite.piece ℤ)

The graded right vertex projective, with its unshifted path-length grading.

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedKoszulMiddle (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : GradedModuleCat ((preprojectiveInternalGrading k).opposite.piece ℤ)

The middle projective shifted so its vertex generators have internal degree one.

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedKoszulRight (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveGradedKoszulMiddle k v ⟶ preprojectiveGradedRightProjective k (Quiver.Symmetrify.of.obj v)

The incoming-arrow differential, as a degree-zero map from the shifted middle term. This is an abbreviation so its cokernel has the carrier of the existing vertex module without transporting along an equality of ranges.

noncomputable def TauCeti.preprojectiveGradedKoszulLeft (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveGradedRightProjective k (Quiver.Symmetrify.of.obj v)).shiftObj 2 ⟶ preprojectiveGradedKoszulMiddle k v

The reverse-arrow differential, as a degree-zero map from the twice-shifted vertex term.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulRight_hom (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveGradedKoszulRight k v).hom = preprojectiveKoszulRight k v

@[simp]

theorem TauCeti.preprojectiveGradedKoszulLeft_hom (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveGradedKoszulLeft k v).hom = preprojectiveKoszulLeft k v

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedVertexModule (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : GradedModuleCat ((preprojectiveInternalGrading k).opposite.piece ℤ)

The vertex augmentation module with the quotient grading of the incoming-arrow map.

noncomputable def TauCeti.preprojectiveGradedVertexAugmentation (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveGradedRightProjective k (Quiver.Symmetrify.of.obj v) ⟶ preprojectiveGradedVertexModule k v

The graded augmentation onto the vertex module.

@[simp]

theorem TauCeti.preprojectiveGradedVertexAugmentation_hom (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveGradedVertexAugmentation k v).hom = preprojectiveVertexAugmentation k v

@[simp]

theorem TauCeti.mem_preprojectiveGradedVertexModule_piece_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (p : ℤ) (x : (preprojectiveGradedVertexModule k v).carrier) : x ∈ (preprojectiveGradedVertexModule k v).grading.piece ℤ p ↔ ∃ (y : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v))), ↑y ∈ preprojectiveIntegerGrade k p ∧ (preprojectiveVertexAugmentation k v) y = x

The homogeneous vectors of the vertex module are precisely the classes of homogeneous vectors of its vertex projective.

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedKoszulTerm (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : ℕ → GradedModuleCat ((preprojectiveInternalGrading k).opposite.piece ℤ)

The graded Koszul terms: the vertex projective in degrees zero and two, with internal shifts zero and two, the arrow-indexed projective shifted by one, and zero thereafter.

noncomputable def TauCeti.preprojectiveGradedKoszulDifferential (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (n : ℕ) : preprojectiveGradedKoszulTerm k v (n + 1) ⟶ preprojectiveGradedKoszulTerm k v n

The degree-zero graded Koszul differentials.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulDifferential_zero (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveGradedKoszulDifferential k v 0 = preprojectiveGradedKoszulRight k v

@[simp]

theorem TauCeti.preprojectiveGradedKoszulDifferential_one (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveGradedKoszulDifferential k v 1 = preprojectiveGradedKoszulLeft k v

@[simp]

theorem TauCeti.preprojectiveGradedKoszulDifferential_add_two (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (n : ℕ) : preprojectiveGradedKoszulDifferential k v (n + 2) = 0

theorem TauCeti.preprojectiveGradedKoszulDifferential_exact (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) (n : ℕ) : Function.Exact ⇑(preprojectiveGradedKoszulDifferential k v (n + 1)).hom ⇑(preprojectiveGradedKoszulDifferential k v n).hom

If the left Koszul map is injective at the chosen vertex, the graded Koszul sequence is exact at every positive homological degree.

@[reducible, inline]

noncomputable abbrev TauCeti.preprojectiveGradedKoszulResolution (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) : GradedProjectiveResolution ((preprojectiveInternalGrading k).opposite.piece ℤ) (preprojectiveGradedVertexModule k v).grading

If the left Koszul map is injective at the chosen vertex, the shifted Koszul complex is a graded projective resolution of its vertex augmentation module, over the ordinary opposite algebra. This is an abbreviation so the types and module instances of its explicit terms can be used without transporting along equalities. Its augmentation is computed by preprojectiveGradedKoszulResolution_π.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulResolution_grading (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) (n : ℕ) : (preprojectiveGradedKoszulResolution k v hinj).grading n = (preprojectiveGradedKoszulTerm k v n).grading

Each resolution term carries the grading of the corresponding shifted Koszul term.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulResolution_d (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) (n : ℕ) : (preprojectiveGradedKoszulResolution k v hinj).d n = (preprojectiveGradedKoszulDifferential k v n).hom

The differentials of the resolution are the explicit graded Koszul maps.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulResolution_π (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) : (preprojectiveGradedKoszulResolution k v hinj).π = preprojectiveVertexAugmentation k v

The augmentation of the resolution is the vertex augmentation.

@[simp]

theorem TauCeti.preprojectiveGradedKoszulResolution_X (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) (n : ℕ) : (preprojectiveGradedKoszulResolution k v hinj).X n = (preprojectiveGradedKoszulTerm k v n).carrier

The terms of the resolution are the shifted graded Koszul terms.

theorem TauCeti.isLinear_preprojectiveGradedKoszulResolution (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (hinj : Function.Injective ⇑(preprojectiveKoszulLeft k v)) : (preprojectiveGradedKoszulResolution k v hinj).IsLinear

The graded Koszul resolution is linear: its term in homological degree n is generated in internal degree n. The terms beyond degree two are zero.

theorem TauCeti.isLinear_preprojectiveGradedKoszulResolution_of_no_sinks (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (hQ : ∀ (u : Q), ∃ (w : Q), Nonempty (u ⟶ w)) (v : Q) : (preprojectiveGradedKoszulResolution k v ⋯).IsLinear

For a finite quiver without sinks, the graded Koszul resolution at every vertex is linear.