The path-length grading of the preprojective algebra

Every preprojective relator of a quiver is homogeneous for the path-length grading of the path algebra of the doubled quiver: the head backtrack and the tail backtrack of an arrow are the basis elements of single length-two paths, so the local relator at a vertex and the global relator are differences of sums of degree-two elements. Consequently the preprojective relation ideal is homogeneous.

Because the relation ideal is homogeneous, the generic descent TauCeti.GradedAlgebra.quotientPiece applies to it: the preprojective algebra Pi_k(Q) carries the induced path-length grading TauCeti.preprojectiveGrade, in which the vertex idempotents have degree 0, the doubled arrows degree 1, and the relator degree 2. This file packages the graded-algebra structure and computes the concrete pieces.

Main definitions

• TauCeti.preprojectiveGrade: the induced degree-n piece on the preprojective algebra, the descent of TauCeti.PathAlgebra.grade along the quotient map TauCeti.preprojectiveMk.
• TauCeti.preprojectiveGradedAlgebra: the preprojective algebra is a graded algebra for the induced path-length grading.

Main results

• TauCeti.headBacktrackElem_mem_grade_two and TauCeti.tailBacktrackElem_mem_grade_two: the two backtracks of an arrow have degree two.
• TauCeti.localPreprojectiveRelator_mem_grade_two and TauCeti.preprojectiveRelator_mem_grade_two: the local and global relators have degree two.
• TauCeti.signlessPreprojectiveRelator_mem_grade_two: so does the signless local relator.
• TauCeti.isHomogeneous_preprojectiveIdeal: the preprojective relation ideal is homogeneous.
• TauCeti.preprojectiveMk_ofArrow_mul_mem_iSup: left multiplication by an arrow lands in positive degree.
• TauCeti.isInternal_preprojectiveGrade: the preprojective algebra is the internal direct sum of its graded pieces, the comparison of the direct-sum graded algebra with the ungraded quotient rather than with a separate graded copy.
• TauCeti.preprojectiveGrade_zero_eq_span_range_vertexIdempotent and TauCeti.preprojectiveGrade_one_eq_span_range_ofArrow: degree 0 is spanned by the vertex idempotent classes and degree 1 by the doubled arrow classes.
• TauCeti.preprojectiveGrade_eq_span_range_ofPath: every piece is spanned by the classes of the paths of its degree.

References

See Crawley-Boevey, Quiver algebras, weighted projective lines, and the Deligne--Simpson problem, Section 1.

The generators of the doubled path algebra are homogeneous

theorem TauCeti.headBacktrackElem_mem_grade_two (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : headBacktrackElem k a ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) 2

The head backtrack of an arrow has degree two: it is the basis element of a single length-two path of the doubled quiver.

theorem TauCeti.tailBacktrackElem_mem_grade_two (k : Type w) {Q : Type u} [Semiring k] [Quiver Q] {i j : Q} (a : i ⟶ j) : tailBacktrackElem k a ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) 2

The tail backtrack of an arrow has degree two: it is the basis element of a single length-two path of the doubled quiver.

The relators have degree two

theorem TauCeti.localPreprojectiveRelator_mem_grade_two (k : Type w) {Q : Type u} [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (v : Q) : localPreprojectiveRelator k v ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) 2

The local preprojective relator has degree two: it is a difference of sums of head and tail backtracks, each of degree two.

theorem TauCeti.preprojectiveRelator_mem_grade_two (k : Type w) (Q : Type u) [Ring k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveRelator k Q ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) 2

The global preprojective relator has degree two.

theorem TauCeti.signlessPreprojectiveRelator_mem_grade_two (k : Type w) {R : Type u} [Semiring k] [Quiver R] [Quiver.HasReverse R] (v : R) [Fintype (Quiver.Star v)] : signlessPreprojectiveRelator k v ∈ PathAlgebra.grade k R 2

The signless local relator has degree two: it is a sum of backtracks, each of them the basis element of a single length-two path.

The relation ideal is homogeneous

theorem TauCeti.isHomogeneous_preprojectiveIdeal (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : Ideal.IsHomogeneous (PathAlgebra.grade k (Quiver.Symmetrify Q)) (TwoSidedIdeal.asIdeal (preprojectiveIdeal k Q))

The preprojective relation ideal is homogeneous for the path-length grading. This is the condition needed to descend the grading to the preprojective algebra.

The induced grading on the preprojective algebra

noncomputable def TauCeti.preprojectiveGrade (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (n : ℕ) : Submodule k (preprojectiveAlgebra k Q)

The induced path-length grading on the preprojective algebra: the degree-n piece is the image of the degree-n piece of the doubled path algebra under the quotient map. Multiplication adds degrees for any relation ideal (TauCeti.GradedAlgebra.mul_mem_quotientPiece); because the relation ideal is homogeneous (TauCeti.isHomogeneous_preprojectiveIdeal), TauCeti.isInternal_preprojectiveGrade also holds, comparing the direct sum of the pieces with the preprojective algebra itself rather than with a separate graded copy.

Equations

• TauCeti.preprojectiveGrade k Q n = TauCeti.GradedAlgebra.quotientPiece (TauCeti.PathAlgebra.grade k (Quiver.Symmetrify Q)) (TwoSidedIdeal.asIdeal (TauCeti.preprojectiveIdeal k Q)) n

theorem TauCeti.preprojectiveMk_mem_preprojectiveGrade (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {n : ℕ} {y : pathAlgebra k (Quiver.Symmetrify Q)} (hy : y ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) n) : (preprojectiveMk k Q) y ∈ preprojectiveGrade k Q n

A homogeneous element lands in the piece its degree names.

@[simp]

theorem TauCeti.mem_preprojectiveGrade_iff (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {n : ℕ} {x : preprojectiveAlgebra k Q} : x ∈ preprojectiveGrade k Q n ↔ ∃ y ∈ PathAlgebra.grade k (Quiver.Symmetrify Q) n, (preprojectiveMk k Q) y = x

Membership in the induced degree-n piece is being the class of a degree-n element of the doubled path algebra.

theorem TauCeti.isInternal_preprojectiveGrade (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : DirectSum.IsInternal (preprojectiveGrade k Q)

The preprojective algebra is the internal direct sum of its graded pieces: this is the comparison of the direct-sum graded algebra with the ungraded quotient, in the internal sense in which the pieces are submodules of the algebra itself.

theorem TauCeti.mul_mem_preprojectiveGrade (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {m n : ℕ} {x y : preprojectiveAlgebra k Q} (hx : x ∈ preprojectiveGrade k Q m) (hy : y ∈ preprojectiveGrade k Q n) : x * y ∈ preprojectiveGrade k Q (m + n)

Multiplication adds degrees in the induced grading: the product of a degree-m class and a degree-n class lies in degree m + n.

theorem TauCeti.preprojectiveMk_ofArrow_mul_mem_iSup (k : Type w) {Q : Type u} [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] {i j : Quiver.Symmetrify Q} (b : i ⟶ j) (z : preprojectiveAlgebra k Q) : (preprojectiveMk k Q) (PathAlgebra.ofArrow b) * z ∈ ⨆ (n : ℕ), preprojectiveGrade k Q (n + 1)

Left multiplication by an arrow raises degrees: b z has positive degree for every z.

@[instance_reducible]

noncomputable def TauCeti.preprojectiveGradedAlgebra (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : GradedAlgebra (preprojectiveGrade k Q)

The preprojective algebra is a graded algebra for the induced path-length grading. This is kept as a definition rather than an instance so that callers choose when to introduce it locally; see TauCeti.GradedAlgebra.gradedAlgebraQuotientPiece.

Equations

• One or more equations did not get rendered due to their size.

The concrete pieces

theorem TauCeti.preprojectiveGrade_zero_eq_span_range_vertexIdempotent (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveGrade k Q 0 = Submodule.span k (Set.range fun (v : Quiver.Symmetrify Q) => (preprojectiveMk k Q) (PathAlgebra.vertexIdempotent k v))

Degree zero is spanned by the vertex idempotent classes: the images under preprojectiveMk of the vertex idempotents of the doubled quiver, that is, of the TauCeti.doubledVertexIdempotents at the vertices of Q.

theorem TauCeti.preprojectiveGrade_one_eq_span_range_ofArrow (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] : preprojectiveGrade k Q 1 = Submodule.span k (Set.range fun (e : (a : Quiver.Symmetrify Q) × (b : Quiver.Symmetrify Q) × (a ⟶ b)) => (preprojectiveMk k Q) (PathAlgebra.ofArrow e.snd.snd))

Degree one is spanned by the doubled arrow classes, one for each arrow of the doubled quiver Quiver.Symmetrify Q.

theorem TauCeti.preprojectiveGrade_eq_span_range_ofPath (k : Type w) (Q : Type u) [CommRing k] [Quiver Q] [Fintype Q] [(i j : Q) → Fintype (i ⟶ j)] (n : ℕ) : preprojectiveGrade k Q n = Submodule.span k (Set.range fun (x : { x : Quiver.TotalPath (Quiver.Symmetrify Q) // x.snd.snd.length = n }) => (preprojectiveMk k Q) (PathAlgebra.ofPath ↑x))

Every graded piece is spanned by the classes of the paths of that length: the degree-n piece of the preprojective algebra is the span of the images, under the quotient map, of the length-n paths of the doubled quiver.