Graded corners of the signless preprojective algebra

For vertices i and j of a finite quiver R with involutive reversal, the graded corner e_j Π_n e_i of the signless preprojective algebra Π = Π^s_k(R) is the span of the classes of the paths of length n from i to j; equivalently, it is the intersection of the degree-n piece with the corner of the two vertex idempotents. Over a field it is finite-dimensional.

Left multiplication by an arrow b : j ⟶ l maps e_j Π_n e_i to e_l Π_{n+1} e_i, and every element of e_l Π_{n+1} e_i is a sum of such products. The graded form of the middle exactness of the Koszul complex 0 → e_v Π → ⨁_{b : j ⟶ v} e_j Π → e_v Π also holds corner by corner: if ∑_b b z_b = 0 with z_b ∈ e_j Π_n e_i, then z_b = b* y for one y ∈ e_v Π_{n-1} e_i. These are the graded inputs to the Koszul complexes of zigzag simple modules, whose generators are dual to these corners.

Main definitions

• TauCeti.signlessPreprojectiveCorner: the graded corner e_j Π_n e_i.

Main results

• TauCeti.mem_signlessPreprojectiveCorner_iff: the graded corner is the degree-n part of the corner e_j Π e_i.
• TauCeti.signlessPreprojectiveCorner_zero_self_eq_span and TauCeti.signlessPreprojectiveCorner_zero_eq_bot_of_ne: the corners in degree zero.
• TauCeti.signlessPreprojectiveMk_ofArrow_mul_mem_signlessPreprojectiveCorner: arrows act on the graded corners.
• TauCeti.exists_eq_sum_signlessPreprojectiveMk_ofArrow_mul: last-arrow decomposition in a graded corner of positive degree.
• TauCeti.exists_mem_signlessPreprojectiveCorner_of_sum_ofArrow_mul_eq_zero: graded middle exactness of the Koszul complex.

References

• 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 graded corners of the vertex Koszul complex.
• TauCeti.RepresentationTheory.Quiver.Preprojective.HilbertSeries.Basic, whose TauCeti.preprojectiveCorner and associated corner lemmas are adapted here to the signless preprojective algebra.

noncomputable def TauCeti.signlessPreprojectiveCorner (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] (n : ℕ) (i j : R) : Submodule k (signlessPreprojectiveAlgebra k R)

The graded corner e_j Π_n e_i of the signless preprojective algebra: the span of the classes of the paths of length n from i to j.

theorem TauCeti.mem_signlessPreprojectiveCorner_iff {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {n : ℕ} {i j : R} {x : signlessPreprojectiveAlgebra k R} : x ∈ signlessPreprojectiveCorner k R n i j ↔ x ∈ signlessPreprojectiveGrade k R n ∧ (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k j) * x * (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) = x

The graded corner e_j Π_n e_i is the degree-n part of the corner e_j Π e_i.

theorem TauCeti.signlessPreprojectiveMk_vertexIdempotent_mul_of_mem_signlessPreprojectiveCorner {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {n : ℕ} {i j : R} {x : signlessPreprojectiveAlgebra k R} (hx : x ∈ signlessPreprojectiveCorner k R n i j) : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k j) * x = x

An element of e_j Π_n e_i is fixed by left multiplication by e_j.

theorem TauCeti.mul_signlessPreprojectiveMk_vertexIdempotent_of_mem_signlessPreprojectiveCorner {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {n : ℕ} {i j : R} {x : signlessPreprojectiveAlgebra k R} (hx : x ∈ signlessPreprojectiveCorner k R n i j) : x * (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) = x

An element of e_j Π_n e_i is fixed by right multiplication by e_i.

theorem TauCeti.signlessPreprojectiveCorner_zero_self_eq_span (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] (i : R) : signlessPreprojectiveCorner k R 0 i i = k ∙ (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i)

The graded corner e_i Π_0 e_i is the line of the vertex idempotent e_i, the class of the only path of length zero from i to i.

theorem TauCeti.signlessPreprojectiveCorner_zero_eq_bot_of_ne (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {i j : R} (h : i ≠ j) : signlessPreprojectiveCorner k R 0 i j = ⊥

The graded corner e_j Π_0 e_i vanishes for i ≠ j: there is no path of length zero between distinct vertices.

theorem TauCeti.signlessPreprojectiveMk_vertexIdempotent_mem_signlessPreprojectiveCorner_zero (k : Type w) {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] (i : R) : (signlessPreprojectiveMk k R) (PathAlgebra.vertexIdempotent k i) ∈ signlessPreprojectiveCorner k R 0 i i

The vertex idempotent e_i lies in the graded corner e_i Π_0 e_i.

theorem TauCeti.signlessPreprojectiveMk_ofArrow_mul_mem_signlessPreprojectiveCorner {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {n : ℕ} {i j l : R} (b : j ⟶ l) {x : signlessPreprojectiveAlgebra k R} (hx : x ∈ signlessPreprojectiveCorner k R n i j) : (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) * x ∈ signlessPreprojectiveCorner k R (n + 1) i l

Left multiplication by an arrow b : j ⟶ l maps e_j Π_n e_i into e_l Π_{n+1} e_i.

theorem TauCeti.disjoint_signlessPreprojectiveCorner {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Finite R] {m n : ℕ} {i i' j j' : R} (h : m ≠ n ∨ i ≠ i' ∨ j ≠ j') : Disjoint (signlessPreprojectiveCorner k R m i j) (signlessPreprojectiveCorner k R n i' j')

Distinct graded corners of the signless preprojective algebra meet only in zero.

theorem TauCeti.exists_eq_sum_signlessPreprojectiveMk_ofArrow_mul {k : Type w} {R : Type u} [CommRing k] [Quiver R] [Quiver.HasReverse R] [(x : R) → Fintype (Quiver.Star x)] [Fintype R] [(i j : R) → Fintype (i ⟶ j)] {n : ℕ} {i v : R} {x : signlessPreprojectiveAlgebra k R} (hx : x ∈ signlessPreprojectiveCorner k R (n + 1) i v) : ∃ (z : (j : R) → (j ⟶ v) → signlessPreprojectiveAlgebra k R), (∀ (j : R) (b : j ⟶ v), z j b ∈ signlessPreprojectiveCorner k R n i j) ∧ x = ∑ j : R, ∑ b : j ⟶ v, (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) * z j b

Last-arrow decomposition in a graded corner. Every element of e_v Π_{n+1} e_i is a sum ∑_{b : j ⟶ v} b z_b with z_b ∈ e_j Π_n e_i.

theorem TauCeti.exists_mem_signlessPreprojectiveCorner_of_sum_ofArrow_mul_eq_zero {k : Type w} [CommRing k] {R : Type u} [Quiver R] [Quiver.HasInvolutiveReverse R] [Fintype R] [(x : R) → Fintype (Quiver.Star x)] [(i j : R) → Fintype (i ⟶ j)] {n : ℕ} {i v : R} {z : (j : R) → (j ⟶ v) → signlessPreprojectiveAlgebra k R} (hz : ∀ (j : R) (b : j ⟶ v), z j b ∈ signlessPreprojectiveCorner k R n i j) (h : ∑ j : R, ∑ b : j ⟶ v, (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow b) * z j b = 0) : ∃ y ∈ signlessPreprojectiveCorner k R (n - 1) i v, ∀ (j : R) (b : j ⟶ v), z j b = (signlessPreprojectiveMk k R) (PathAlgebra.ofArrow (Quiver.reverse b)) * y

Graded middle exactness of the Koszul complex. Let z_b ∈ e_j Π_n e_i for the arrows b : j ⟶ v. If ∑_b b z_b = 0, then there is y ∈ e_v Π_{n-1} e_i with z_b = b* y for every b; for n = 0 every z_b vanishes and y = 0.

instance TauCeti.instFiniteDimensionalSubtypeSignlessPreprojectiveAlgebraMemSubmoduleSignlessPreprojectiveCorner (k : Type w) {R : Type u} [Field k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] [∀ (i j : R), Finite (i ⟶ j)] (n : ℕ) (i j : R) : FiniteDimensional k ↥(signlessPreprojectiveCorner k R n i j)

The graded corners of the signless preprojective algebra of a finite quiver are finite-dimensional: there are finitely many paths of each length between two vertices.