The grading of the componentwise zigzag algebra

The public zigzag algebra carries the product grading of its connected-component factors. On a component with an edge this is the grading descended from path length; on a singleton it is the dual-number grading with the infinitesimal generator in degree two. The global vertex–arrow–volume basis is homogeneous in degrees zero, one and two, respectively.

The graded pieces are submodules of the public algebra itself. Their internal direct-sum property and multiplicativity supply a GradedAlgebra, including for disconnected graphs and graphs with isolated vertices. As for the relation quotient, the grading is also extended by zero to integer degrees, in which internal grading shifts are stated.

The signed GradedAlgebra bundle follows TauCeti.zigzagIntegerGradedAlgebra for the relation quotient. TauCeti.zigzagAlgebraInternalGrading packages these same signed pieces for internally graded modules and bimodule tensor products.

See Huerfano–Khovanov, A category for the adjoint representation, Section 3, for the path grading and singleton convention.

noncomputable def TauCeti.zigzagComponentGrade (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) (n : ℕ) : Submodule k ↑(zigzagComponentAlgebra k G C)

The degree-n submodule of a component algebra, transported from its quotient or its dual-number presentation.

@[simp]

theorem TauCeti.mem_zigzagComponentGrade_of_nontrivial (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Nontrivial ↥C] {n : ℕ} {x : ↑(zigzagComponentAlgebra k G C)} : x ∈ zigzagComponentGrade k G C n ↔ (zigzagComponentAlgebraEquivNonisolated k G C) x ∈ zigzagGrade k C.toSimpleGraph n

On a nontrivial component, homogeneous membership is detected in the relation quotient.

@[simp]

theorem TauCeti.mem_zigzagComponentGrade_of_subsingleton (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) [Subsingleton ↥C] {n : ℕ} {x : ↑(zigzagComponentAlgebra k G C)} : x ∈ zigzagComponentGrade k G C n ↔ ((zigzagComponentAlgebraEquivULiftDualNumber k G C) x).down ∈ dualNumberGrade k n

On a singleton component, homogeneous membership is detected in the dual numbers.

instance TauCeti.instGradedMonoidNatCarrierZigzagComponentAlgebraSubmoduleZigzagComponentGrade (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (C : G.ConnectedComponent) : SetLike.GradedMonoid (zigzagComponentGrade k G C)

Multiplication in a component adds degrees, and its unit has degree zero.

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

Every component grade above degree two vanishes.

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

The componentwise degree-n submodule of the public zigzag algebra.

@[simp]

theorem TauCeti.mem_zigzagAlgebraGrade (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {n : ℕ} {x : ↑(zigzagAlgebra k G)} : x ∈ zigzagAlgebraGrade k G n ↔ ∀ (C : G.ConnectedComponent), (zigzagComponentProjection k G C) x ∈ zigzagComponentGrade k G C n

An element is homogeneous exactly when every component has the same degree.

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

The public algebra has no homogeneous pieces in degrees three and above.

instance TauCeti.instGradedMonoidNatCarrierZigzagAlgebraSubmoduleZigzagAlgebraGrade (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : SetLike.GradedMonoid (zigzagAlgebraGrade k G)

The componentwise grading respects the unit and multiplication of the public algebra.

@[simp]

theorem TauCeti.zigzagAlgebraBasis_inl_mem_grade_zero (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : (zigzagAlgebraBasis k G) (Sum.inl i) ∈ zigzagAlgebraGrade k G 0

The global vertex basis vectors have degree zero.

@[simp]

theorem TauCeti.zigzagAlgebraBasis_inr_inl_mem_grade_one (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (d : G.Dart) : (zigzagAlgebraBasis k G) (Sum.inr (Sum.inl d)) ∈ zigzagAlgebraGrade k G 1

The global arrow basis vectors have degree one.

@[simp]

theorem TauCeti.zigzagAlgebraBasis_inr_inr_mem_grade_two (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i)) ∈ zigzagAlgebraGrade k G 2

The global volume basis vectors have degree two, including at isolated vertices.

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

The public zigzag algebra is the internal direct sum of its componentwise graded pieces.

@[instance_reducible]

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

The product grading on the public algebra, including the degree-two singleton generators. Install this structure locally to use Mathlib's graded-algebra projections and direct-sum algebra equivalence.

Integer-indexed grading

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

The componentwise grading of the public zigzag algebra, extended by zero from ℕ to ℤ, as TauCeti.zigzagIntegerGrade extends that of the relation quotient. This signed indexing is needed to state internal grading shifts.

@[simp]

theorem TauCeti.zigzagAlgebraIntegerGrade_ofNat (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (d : ℕ) : zigzagAlgebraIntegerGrade k G ↑d = zigzagAlgebraGrade k G d

theorem TauCeti.zigzagAlgebraBasis_inl_mem_integerGrade_zero (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : (zigzagAlgebraBasis k G) (Sum.inl i) ∈ zigzagAlgebraIntegerGrade k G 0

The vertex idempotent is homogeneous of degree zero in the signed grading.

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

The integer extension of the componentwise grading vanishes in negative degrees.

theorem TauCeti.zigzagAlgebraIntegerGrade_eq_bot_of_not_mem (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {d : ℤ} (hd : d ∉ {0, 1, 2}) : zigzagAlgebraIntegerGrade k G d = ⊥

The integer path grading has no pieces outside degrees zero, one and two.

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

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

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

Multiplication adds signed degrees in the integer extension of the componentwise grading.

@[instance_reducible]

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

The signed grading as a graded algebra. Install it locally when tensoring graded modules.

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagAlgebraInternalGrading (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) : InternalGrading k ↑(zigzagAlgebra k G) ℤ

The signed path-length grading of the public zigzag algebra as an internal grading.