The path-length grading of the signless preprojective algebra

The signless backtrack relators have degree two. Their two-sided ideal is therefore homogeneous, so the path grading descends to the signless quotient. In particular, the positive-degree part can be used as the kernel of a vertex augmentation in its Koszul complex.

theorem TauCeti.isHomogeneous_signlessPreprojectiveIdeal (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : Ideal.IsHomogeneous (PathAlgebra.grade k R) (TwoSidedIdeal.asIdeal (signlessPreprojectiveIdeal k R))

The signless preprojective ideal is homogeneous for path length: every defining relator has degree two.

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

The degree-n piece of the signless preprojective algebra, induced from the path algebra.

theorem TauCeti.signlessPreprojectiveMk_mem_grade (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] {n : ℕ} {y : pathAlgebra k R} (hy : y ∈ PathAlgebra.grade k R n) : (signlessPreprojectiveMk k R) y ∈ signlessPreprojectiveGrade k R n

A class of a homogeneous path-algebra element belongs to its induced graded piece.

@[simp]

theorem TauCeti.mem_signlessPreprojectiveGrade_iff (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] {n : ℕ} {x : signlessPreprojectiveAlgebra k R} : x ∈ signlessPreprojectiveGrade k R n ↔ ∃ y ∈ PathAlgebra.grade k R n, (signlessPreprojectiveMk k R) y = x

Membership in the induced graded piece is represented by a homogeneous path-algebra element.

theorem TauCeti.isInternal_signlessPreprojectiveGrade (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : DirectSum.IsInternal (signlessPreprojectiveGrade k R)

The signless quotient is the internal direct sum of its path-length pieces.

theorem TauCeti.mul_mem_signlessPreprojectiveGrade (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] {m n : ℕ} {x y : signlessPreprojectiveAlgebra k R} (hx : x ∈ signlessPreprojectiveGrade k R m) (hy : y ∈ signlessPreprojectiveGrade k R n) : x * y ∈ signlessPreprojectiveGrade k R (m + n)

Multiplication adds path lengths in the signless preprojective algebra.

@[instance_reducible]

noncomputable def TauCeti.signlessPreprojectiveGradedAlgebra (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] : GradedAlgebra (signlessPreprojectiveGrade k R)

The signless preprojective algebra, equipped with its induced path-length grading.

theorem TauCeti.exists_signlessPreprojectiveMk_ofPath_ne_zero_of_ne_bot (k : Type w) (R : Type u) [CommRing k] [Quiver R] [Quiver.HasReverse R] [Finite R] [(x : R) → Fintype (Quiver.Star x)] {d : ℕ} (h : signlessPreprojectiveGrade k R d ≠ ⊥) : ∃ (p : Quiver.TotalPath R), p.snd.snd.length = d ∧ (signlessPreprojectiveMk k R) (PathAlgebra.ofPath p) ≠ 0

A nonzero path-length piece of the signless quotient contains the nonzero class of an actual path of that length.

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

Left multiplication by an arrow lands in the positive-degree part of the signless quotient.