The zigzag relations are homogeneous and the induced grading

Every zigzag relator of a simple graph is homogeneous for the path-length grading of the path algebra of the doubled quiver: the two quadratic families sit in degree two, and each long generator is a single path, homogeneous of its own length. Consequently both relation ideals of TauCeti.RepresentationTheory.Quiver.Zigzag.Relations are homogeneous ideals.

Because the relation ideals are homogeneous, the generic descent TauCeti.RingTheory.GradedAlgebra.Homogeneous.Quotient applies to them: the relation quotient carries the induced grading TauCeti.zigzagGrade, this file packages its graded-algebra structure, and it computes the concrete pieces.

Main definitions

• TauCeti.zigzagGrade: the induced degree-n piece on the relation quotient, the descent of TauCeti.PathAlgebra.grade along the quotient map.
• TauCeti.zigzagIntegerGrade: the same grading extended by zero to integer degrees.
• TauCeti.zigzagGradedAlgebra: the zigzag relation quotient is a graded algebra for the induced path-length grading.
• TauCeti.zigzagIntegerGradedAlgebra: the same graded-algebra structure after extension to integer degrees.

Main results

• TauCeti.DoubledQuiver.backtrackElem_mem_grade_two: a backtrack has degree two.
• TauCeti.IsZigzagRelator.isHomogeneousElem and TauCeti.IsQuadraticZigzagRelator.mem_grade_two: the relators are homogeneous, the quadratic ones in degree two.
• TauCeti.isHomogeneous_zigzagIdeal and TauCeti.isHomogeneous_quadraticZigzagIdeal: the relation ideals are homogeneous.
• TauCeti.mem_zigzagGrade_iff: a graded piece consists of the classes of the homogeneous elements of its degree.
• TauCeti.isInternal_zigzagGrade: the quotient is the internal direct sum of its graded pieces, the comparison of the direct-sum graded algebra with the ungraded quotient asked for by the roadmap.
• TauCeti.zigzagGrade_zero_eq_span_range_vertexIdempotent, TauCeti.zigzagGrade_one_eq_span_range_ofArrow and TauCeti.zigzagGrade_two_eq_span_range_zigzagVolume: the concrete pieces, spanned by the vertex idempotent classes, the arrow classes, and the volume classes respectively.
• TauCeti.zigzagGrade_eq_bot_of_three_le: every piece of degree at least three vanishes.
• TauCeti.isInternal_zigzagIntegerGrade: the extension by zero to integer degrees is still an internal direct sum, so it is an integer grading of the quotient.
• TauCeti.zigzagBasis_coord_dart_eq_zero_of_mem_zigzagIntegerGrade: an arrow coordinate vanishes on every piece of degree other than one.
• TauCeti.zigzagBasis_coord_dart_koszulTwist_one: the degree-one Koszul twist of the path-length grading negates arrow coordinates.

References

This is the grading clause of Layer 0 of TauCetiRoadmap/ZigzagPreprojective/README.md, which asks for the relation ideal to be homogeneous for the path-length grading and for the induced nonnegative grading on the quotient to be compared with the ungraded quotient rather than postulated as an unrelated graded copy. See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

theorem TauCeti.DoubledQuiver.backtrackElem_mem_grade_two (k : Type w) [Semiring k] {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : backtrackElem G k h ∈ PathAlgebra.grade k (DoubledQuiver G) 2

A backtrack element has degree two: it is the basis element of a single length-two path.

theorem TauCeti.IsQuadraticZigzagRelator.mem_grade_two (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsQuadraticZigzagRelator k G x) : x ∈ PathAlgebra.grade k (DoubledQuiver G) 2

The quadratic zigzag relators sit in degree two: a non-returning length-two path is a single basis path of length two, and a difference of two length-two backtracks is a difference of two such.

theorem TauCeti.IsQuadraticZigzagRelator.isHomogeneousElem (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsQuadraticZigzagRelator k G x) : SetLike.IsHomogeneousElem (PathAlgebra.grade k (DoubledQuiver G)) x

The quadratic zigzag relators are homogeneous.

theorem TauCeti.IsZigzagRelator.isHomogeneousElem (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) {x : pathAlgebra k (DoubledQuiver G)} (hx : IsZigzagRelator k G x) : SetLike.IsHomogeneousElem (PathAlgebra.grade k (DoubledQuiver G)) x

The uniform zigzag relators are homogeneous: the quadratic ones in degree two, and each long generator in the degree its own length names.

theorem TauCeti.isHomogeneous_quadraticZigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : Ideal.IsHomogeneous (PathAlgebra.grade k (DoubledQuiver G)) (TwoSidedIdeal.asIdeal (quadraticZigzagIdeal k G))

The quadratic relation ideal is homogeneous for the path-length grading.

theorem TauCeti.isHomogeneous_zigzagIdeal (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : Ideal.IsHomogeneous (PathAlgebra.grade k (DoubledQuiver G)) (TwoSidedIdeal.asIdeal (zigzagIdeal k G))

The uniform relation ideal is homogeneous for the path-length grading. This is the condition needed to descend the grading to the zigzag quotient.

The induced grading on the relation quotient

noncomputable def TauCeti.zigzagGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (n : ℕ) : Submodule k (nonisolatedZigzagQuotient k G)

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

@[simp]

theorem TauCeti.zigzagMk_mem_zigzagGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {n : ℕ} {y : pathAlgebra k (DoubledQuiver G)} (hy : y ∈ PathAlgebra.grade k (DoubledQuiver G) n) : (zigzagMk k G) y ∈ zigzagGrade k G n

A homogeneous element lands in the piece its degree names.

theorem TauCeti.mem_zigzagGrade_iff (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {n : ℕ} {x : nonisolatedZigzagQuotient k G} : x ∈ zigzagGrade k G n ↔ ∃ y ∈ PathAlgebra.grade k (DoubledQuiver G) n, (zigzagMk k G) y = x

Membership in a graded piece is being the class of a homogeneous element of that degree.

@[simp]

theorem TauCeti.nonisolatedZigzagQuotientEquiv_mem_zigzagGrade_iff (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {W : Type u_1} [Finite W] {H : SimpleGraph W} (e : G ≃g H) {n : ℕ} {x : nonisolatedZigzagQuotient k G} : (nonisolatedZigzagQuotientEquiv k e) x ∈ zigzagGrade k H n ↔ x ∈ zigzagGrade k G n

Graph relabelling preserves and reflects the descended path-length grading.

theorem TauCeti.isInternal_zigzagGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : DirectSum.IsInternal (zigzagGrade k G)

The quotient is the internal direct sum of its graded pieces: this is the comparison of the direct-sum graded algebra with the ungraded quotient asked for by the roadmap, in the internal sense in which the pieces are submodules of the quotient itself rather than a separate graded copy.

theorem TauCeti.mul_mem_zigzagGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {m n : ℕ} {x y : nonisolatedZigzagQuotient k G} (hx : x ∈ zigzagGrade k G m) (hy : y ∈ zigzagGrade k G n) : x * y ∈ zigzagGrade k G (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.

@[instance_reducible]

noncomputable def TauCeti.zigzagGradedAlgebra (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : GradedAlgebra (zigzagGrade k G)

The zigzag relation quotient 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.

theorem TauCeti.zigzagGrade_zero_eq_span_range_vertexIdempotent (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : zigzagGrade k G 0 = Submodule.span k (Set.range fun (i : V) => (zigzagMk k G) (PathAlgebra.vertexIdempotent k (DoubledQuiver.vertex G i)))

Degree zero is spanned by the vertex idempotent classes.

theorem TauCeti.zigzagGrade_one_eq_span_range_ofArrow (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : zigzagGrade k G 1 = Submodule.span k (Set.range fun (d : G.Dart) => (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)))

Degree one is spanned by the arrow classes, one for each dart of the graph.

theorem TauCeti.zigzagGrade_two_eq_span_range_zigzagVolume (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : zigzagGrade k G 2 = Submodule.span k (Set.range fun (i : V) => zigzagVolume k G i)

Degree two is spanned by the volume classes: every length-two path either does not return, and dies, or returns to its source, and equals a backtrack there.

theorem TauCeti.zigzagGrade_eq_bot_of_three_le (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {n : ℕ} (hn : 3 ≤ n) : zigzagGrade k G n = ⊥

Every piece of degree at least three vanishes: all long paths are relations.

Integer-indexed grading

noncomputable def TauCeti.zigzagIntegerGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : ℤ) : Submodule k (nonisolatedZigzagQuotient k G)

The path-length grading of the zigzag relation quotient, extended by zero from ℕ to ℤ. This signed indexing is needed to state every internal grading shift.

@[simp]

theorem TauCeti.zigzagIntegerGrade_ofNat (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : ℕ) : zigzagIntegerGrade k G ↑d = zigzagGrade k G d

theorem TauCeti.zigzagIntegerGrade_eq_bot_of_neg (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {d : ℤ} (hd : d < 0) : zigzagIntegerGrade k G d = ⊥

The integer extension of the path-length grading vanishes in negative degrees.

theorem TauCeti.isInternal_zigzagIntegerGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : DirectSum.IsInternal (zigzagIntegerGrade k G)

The integer extension of the path-length grading is an internal direct sum: the pieces in nonnegative degrees are those of TauCeti.zigzagGrade, and those in negative degrees vanish.

@[instance_reducible]

noncomputable def TauCeti.zigzagIntegerGradedAlgebra (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] : GradedAlgebra (zigzagIntegerGrade k G)

The zigzag relation quotient is an integer-graded algebra for the path-length grading indexed by ℤ, extended by zero in negative degrees.

theorem TauCeti.zigzagBasis_coord_dart_eq_zero_of_mem_zigzagIntegerGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (d : G.Dart) {e : ℤ} (he : e ≠ 1) {x : nonisolatedZigzagQuotient k G} (hx : x ∈ zigzagIntegerGrade k G e) : ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) x = 0

An arrow coordinate vanishes off degree one: the pieces of degree other than one are spanned by vertex idempotents and volume classes, which have no arrow component.

theorem TauCeti.zigzagBasis_coord_vertex_eq_zero_of_mem_zigzagIntegerGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i : V) {e : ℤ} (he : e ≠ 0) {x : nonisolatedZigzagQuotient k G} (hx : x ∈ zigzagIntegerGrade k G e) : ((zigzagBasis k G hns).coord (Sum.inl i)) x = 0

A vertex coordinate vanishes off degree zero: the pieces of nonzero degree are spanned by arrows and volume classes, which have no vertex-idempotent component.

theorem TauCeti.zigzagMk_ofArrow_mem_zigzagIntegerGrade_one (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (d : G.Dart) : (zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯)) ∈ zigzagIntegerGrade k G 1

Every arrow class has degree one.

theorem TauCeti.zigzagVolume_mem_zigzagIntegerGrade_two (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVolume k G i ∈ zigzagIntegerGrade k G 2

Every volume class has degree two.

theorem TauCeti.mul_mem_zigzagIntegerGrade (k : Type w) [CommRing k] {V : Type u} (G : SimpleGraph V) [Finite V] {m n : ℤ} {x y : nonisolatedZigzagQuotient k G} (hx : x ∈ zigzagIntegerGrade k G m) (hy : y ∈ zigzagIntegerGrade k G n) : x * y ∈ zigzagIntegerGrade k G (m + n)

Multiplication adds signed degrees in the integer extension of the path-length grading.

The degree-one Koszul twist of the path-length grading

theorem TauCeti.koszulTwist_one_zigzagMk_ofArrow {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {𝒢 : InternalGrading k (nonisolatedZigzagQuotient k G) ℤ} (h𝒢 : 𝒢.piece ℤ = zigzagIntegerGrade k G) (d : G.Dart) : (𝒢.koszulTwist 1) ((zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))) = -(zigzagMk k G) (PathAlgebra.ofArrow (DoubledQuiver.arrow G ⋯))

The degree-one Koszul twist of the path-length grading negates arrows.

theorem TauCeti.zigzagBasis_coord_dart_koszulTwist_one {k : Type w} [CommRing k] {V : Type u} {G : SimpleGraph V} [Finite V] {hns : ∀ (i : V), ∃ (j : V), G.Adj i j} {𝒢 : InternalGrading k (nonisolatedZigzagQuotient k G) ℤ} (h𝒢 : 𝒢.piece ℤ = zigzagIntegerGrade k G) (d : G.Dart) (x : nonisolatedZigzagQuotient k G) : ((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) ((𝒢.koszulTwist 1) x) = -((zigzagBasis k G hns).coord (Sum.inr (Sum.inl d))) x

The degree-one Koszul twist of the path-length grading negates arrow coordinates.