Signed graded corners of the componentwise zigzag algebra

A self corner has its vertex vector in degree zero and its volume vector in degree two. This includes the infinitesimal at an isolated vertex. An adjacent corner is concentrated in degree one. The existing corner spans and the homogeneous vertex–arrow–volume basis determine their intersections with the signed grading. These degree-wise dimensions compute graded vertex-projective Hom dimensions and the coefficients of the graded Cartan matrix.

References

The vertex–arrow–volume graded-corner calculation was previously formalized in TauCeti/RepresentationTheory/Quiver/Zigzag/CartanMatrix.lean for the path-graded relation quotient under the no-isolated-vertex hypothesis. Here the componentwise algebra and signed grading retain the degree-two volume of every isolated dual-number factor.

The algebra and grading conventions follow Huerfano--Khovanov, A category for the adjoint representation, Section 3, and Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

@[simp]

theorem TauCeti.cornerSubmodule_zigzagAlgebra_self_inf_integerGrade (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) (d : ℤ) : cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ⊓ zigzagAlgebraIntegerGrade k G d = if d = 0 then k ∙ (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i else if d = 2 then k ∙ (fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inr (Sum.inr i))) i else ⊥

A self corner has its vertex and volume spans in degrees zero and two, respectively.

@[simp]

theorem TauCeti.cornerSubmodule_zigzagAlgebra_inf_integerGrade_of_adj (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) {i j : V} (h : G.Adj j i) (d : ℤ) : cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j) ⊓ zigzagAlgebraIntegerGrade k G d = if d = 1 then cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j) else ⊥

An adjacent corner is concentrated in signed degree one.

@[simp]

theorem TauCeti.finrank_cornerSubmodule_zigzagAlgebra_inf_integerGrade (k : Type w) [Field k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (d : ℤ) : Module.finrank k ↥(cornerSubmodule k ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j) ⊓ zigzagAlgebraIntegerGrade k G d) = if i = j then if d = 0 ∨ d = 2 then 1 else 0 else if G.Adj i j ∧ d = 1 then 1 else 0

The dimensions of all signed corners: self degrees zero and two, or an edge in degree one.