Projective resolutions of preprojective vertex modules

For a finite quiver Q, write Π = Π_k(Q). The right vertex projective e_v Π consists of path classes ending at v. Right modules are represented as left modules over Πᵐᵒᵖ. This file bundles the two maps of the preprojective Koszul complex as right-module maps:

e_v Π → ⨁_{b : i → v} e_i Π → e_v Π,

with formulas y ↦ (ε_b b* y)_b and (z_b) ↦ ∑_b b z_b. Multiplication is later-factor-first. The finite direct sum is implemented as a dependent function space. The cokernel is the vertex augmentation module: the kernel of its quotient map is precisely the positive path-degree part of e_v Π.

The middle exactness is valid over every commutative ring and for every finite quiver. When every vertex of Q has an outgoing arrow, the first map is injective and the augmented complex is a length-two projective resolution. The construction uses the exactness theorems in TauCeti.RepresentationTheory.Quiver.Preprojective.Koszul.Complex and the injectivity theorem in TauCeti.RepresentationTheory.Quiver.Preprojective.Sinkless. This is an ungraded resolution; internal shifts and linearity are not asserted here.

References

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

noncomputable def TauCeti.preprojectiveRightProjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : Submodule (preprojectiveAlgebra k Q)ᵐᵒᵖ (preprojectiveAlgebra k Q)

The right vertex projective e_i Π, realized inside Π with opposite scalars.

@[simp]

theorem TauCeti.mem_preprojectiveRightProjective_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) (x : preprojectiveAlgebra k Q) : x ∈ preprojectiveRightProjective k i ↔ (fun (i : Quiver.Symmetrify Q) => (preprojectiveMk k Q) (PathAlgebra.vertexIdempotent k i)) i * x = x

A path class belongs to e_i Π exactly when left multiplication by e_i fixes it.

instance TauCeti.instProjectiveMulOppositePreprojectiveAlgebraSubtypeMemSubmodulePreprojectiveRightProjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (i : Quiver.Symmetrify Q) : Module.Projective (preprojectiveAlgebra k Q)ᵐᵒᵖ ↥(preprojectiveRightProjective k i)

Each right vertex ideal is projective, since multiplication by its idempotent splits its inclusion in the regular right module.

@[reducible, inline]

abbrev TauCeti.preprojectiveKoszulMiddle (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : Type (max (max (max (max u v) w) u) v)

The middle projective of the Koszul complex at v, indexed by doubled arrows into v.

instance TauCeti.instProjectiveMulOppositePreprojectiveAlgebraPreprojectiveKoszulMiddle (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : Module.Projective (preprojectiveAlgebra k Q)ᵐᵒᵖ (preprojectiveKoszulMiddle k v)

The middle Koszul term is projective as a finite direct sum of right vertex projectives, represented by a dependent function space.

noncomputable def TauCeti.preprojectiveKoszulLeft (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v)) →ₗ[(preprojectiveAlgebra k Q)ᵐᵒᵖ] preprojectiveKoszulMiddle k v

The first Koszul differential, y ↦ (ε_b b* y)_b.

noncomputable def TauCeti.preprojectiveKoszulRight (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveKoszulMiddle k v →ₗ[(preprojectiveAlgebra k Q)ᵐᵒᵖ] ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v))

The second Koszul differential, (z_b) ↦ ∑_b b z_b.

@[simp]

theorem TauCeti.coe_preprojectiveKoszulLeft_apply (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (y : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v))) (i : Quiver.Symmetrify Q) (b : i ⟶ Quiver.Symmetrify.of.obj v) : ↑((preprojectiveKoszulLeft k v) y i b) = doubledArrowSign k b • ((preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.reverse b)) * ↑y)

@[simp]

theorem TauCeti.coe_preprojectiveKoszulRight_apply (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (z : preprojectiveKoszulMiddle k v) : ↑((preprojectiveKoszulRight k v) z) = ∑ i : Quiver.Symmetrify Q, ∑ b : i ⟶ Quiver.Symmetrify.of.obj v, (preprojectiveMk k Q) (PathAlgebra.ofArrow b) * ↑(z i b)

@[simp]

theorem TauCeti.preprojectiveKoszulRight_comp_left (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveKoszulRight k v ∘ₗ preprojectiveKoszulLeft k v = 0

The Koszul differentials compose to zero by the local preprojective relation.

theorem TauCeti.range_preprojectiveKoszulLeft_eq_ker_right (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveKoszulLeft k v).range = (preprojectiveKoszulRight k v).ker

Exactness at the middle projective, with no restriction on the quiver.

@[reducible, inline]

abbrev TauCeti.preprojectiveVertexModule (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : Type (max (max u v) w)

The vertex augmentation module, the cokernel of the incoming-arrow map on e_v Π. Its quotient kernel is precisely the positive path-degree part.

noncomputable def TauCeti.preprojectiveVertexAugmentation (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v)) →ₗ[(preprojectiveAlgebra k Q)ᵐᵒᵖ] preprojectiveVertexModule k v

The augmentation from the vertex projective to its vertex module.

theorem TauCeti.preprojectiveVertexAugmentation_apply (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (x : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v))) : (preprojectiveVertexAugmentation k v) x = Submodule.Quotient.mk x

The vertex augmentation sends each element to its quotient class.

@[simp]

theorem TauCeti.preprojectiveVertexAugmentation_eq_zero_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) (x : ↥(preprojectiveRightProjective k (Quiver.Symmetrify.of.obj v))) : (preprojectiveVertexAugmentation k v) x = 0 ↔ ↑x ∈ ⨆ (n : ℕ), preprojectiveGrade k Q (n + 1)

The augmentation kills exactly the elements of positive path degree.

@[simp]

theorem TauCeti.ker_preprojectiveVertexAugmentation (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : (preprojectiveVertexAugmentation k v).ker = (preprojectiveKoszulRight k v).range

The vertex augmentation kernel is the range of the incoming-arrow differential.

theorem TauCeti.preprojectiveVertexAugmentation_surjective (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : Function.Surjective ⇑(preprojectiveVertexAugmentation k v)

The vertex augmentation is surjective.

theorem TauCeti.preprojectiveKoszulLeft_injective_iff (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : Function.Injective ⇑(preprojectiveKoszulLeft k v) ↔ ∀ (y : preprojectiveAlgebra k Q), (preprojectiveMk k Q) (doubledVertexIdempotent k v) * y = y → (∀ (i : Quiver.Symmetrify Q) (b : i ⟶ Quiver.Symmetrify.of.obj v), (preprojectiveMk k Q) (PathAlgebra.ofArrow (Quiver.reverse b)) * y = 0) → y = 0

The left Koszul differential is injective exactly when no nonzero element of e_v Π is annihilated by every doubled arrow leaving v. The signs in the differential are units, including in characteristic two.

theorem TauCeti.preprojectiveKoszulLeft_injective (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) : Function.Injective ⇑(preprojectiveKoszulLeft k v)

For a quiver without sinks, the left Koszul differential is injective.

The augmented chain complex

noncomputable def TauCeti.preprojectiveKoszulComplex (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : ChainComplex (ModuleCat (preprojectiveAlgebra k Q)ᵐᵒᵖ) ℕ

The right-module Koszul chain complex, supported in degrees zero, one and two. Its term identifications and differential formulas are those of ModuleCatLengthTwo.complex.

@[simp]

theorem TauCeti.preprojectiveKoszulComplex_def (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : preprojectiveKoszulComplex k v = ModuleCatLengthTwo.complex (preprojectiveKoszulLeft k v) (preprojectiveKoszulRight k v) ⋯

The Koszul complex is the common three-term construction on the Koszul maps.

noncomputable def TauCeti.preprojectiveKoszulProjectiveResolution (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) : CategoryTheory.ProjectiveResolution ↧(preprojectiveVertexModule k v)

The vertex module of a quiver without sinks has a projective resolution supported in homological degrees zero, one and two, with the Koszul maps as differentials. This is a resolution over the opposite algebra, hence of right preprojective modules. The term identifications and augmentation formula are supplied by ModuleCatLengthTwo.projectiveResolutionXIso and ModuleCatLengthTwo.projectiveResolution_π_f_zero.

@[simp]

theorem TauCeti.preprojectiveKoszulProjectiveResolution_def (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) : preprojectiveKoszulProjectiveResolution k hQ v = ModuleCatLengthTwo.projectiveResolution (preprojectiveKoszulLeft k v) (preprojectiveKoszulRight k v) ⋯ ⋯

The vertex resolution is the common length-two construction on the Koszul maps.