Zigzag vertex projectives in the graded-module category

The path-length grading restricted to Z e_i is an internal direct sum, not just a family of subspaces. This makes each vertex projective an object of TauCeti.GradedModuleCat, and its ungraded projectivity implies categorical projectivity. Internal shifts use (P{d})_p = P_{p-d}.

The categorical space Hom(P_i, P_j{d}) is linearly equivalent to the homogeneous-map submodule already computed for the zigzag projectives. When the graph has no isolated vertices (∀ i, ∃ j, G.Adj i j), its Laurent support is finite, and its target-shift graded dimension is exactly TauCeti.zigzagProjectiveQHom. Thus the quantum Cartan entries are actual graded categorical Hom dimensions, ready for projective Euler evaluation.

These constructions concern the relation quotient. On a component with an edge it is the ordinary zigzag algebra; singleton components of the public algebra instead use dual numbers.

References

• Huerfano--Khovanov, A category for the adjoint representation, Section 3.
• Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.
• Năstăsescu--Van Oystaeyen, Methods of Graded Rings, Section 2.3, for projectivity in the graded-module category.

theorem TauCeti.zigzagVertexIdempotent_mem_zigzagIntegerGrade_zero (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : zigzagVertexIdempotent k G i ∈ zigzagIntegerGrade k G 0

The vertex idempotent has degree zero.

theorem TauCeti.isHomogeneous_zigzagProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] [GradedAlgebra (zigzagIntegerGrade k G)] (i : V) : Ideal.IsHomogeneous (zigzagIntegerGrade k G) (zigzagProjective k G i)

The vertex projective is a homogeneous submodule of the regular module: homogeneous projection preserves the fixed-point equation x * e_i = x.

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : GradedModuleCat (zigzagIntegerGrade k G)

The graded left vertex projective Z e_i, with its induced path-length grading. This is an abbreviation so its carrier and module structures remain those of the principal ideal.

theorem TauCeti.zigzagGradedProjective_piece (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (p : ℤ) : (zigzagGradedProjective k G i).grading.piece ℤ p = zigzagProjectiveGrade k G i p

The grading of the categorical projective is the restricted path-length grading.

theorem TauCeti.zigzagGradedProjective_shift_piece (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) (d p : ℤ) : ((zigzagGradedProjective k G i).shiftObj d).grading.piece ℤ p = zigzagProjectiveShiftGrade k G i d p

Shifting the categorical projective agrees with the previously defined projective shift.

instance TauCeti.projective_zigzagGradedProjective (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i : V) : CategoryTheory.Projective (zigzagGradedProjective k G i)

The vertex projective is projective in the graded-module category.

noncomputable def TauCeti.zigzagGradedProjectiveHomEquiv (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : (zigzagGradedProjective k G i ⟶ (zigzagGradedProjective k G j).shiftObj d) ≃ₗ[k] ↥(zigzagProjectiveTargetShiftHom k G i j d)

Categorical graded maps P_i → P_j{d} are exactly the homogeneous maps in zigzagProjectiveTargetShiftHom. The equivalence does not change the underlying linear map.

@[simp]

theorem TauCeti.coe_zigzagGradedProjectiveHomEquiv_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} (f : zigzagGradedProjective k G i ⟶ (zigzagGradedProjective k G j).shiftObj d) : ↑((zigzagGradedProjectiveHomEquiv k G i j d) f) = f.hom

@[simp]

theorem TauCeti.hom_zigzagGradedProjectiveHomEquiv_symm_apply (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] {i j : V} {d : ℤ} (f : ↥(zigzagProjectiveTargetShiftHom k G i j d)) : ((zigzagGradedProjectiveHomEquiv k G i j d).symm f).hom = ↑f

theorem TauCeti.finrank_zigzagGradedProjective_hom (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (i j : V) (d : ℤ) : Module.finrank k (zigzagGradedProjective k G i ⟶ (zigzagGradedProjective k G j).shiftObj d) = Module.finrank k ↥(zigzagProjectiveTargetShiftHom k G i j d)

Categorical shifted Hom spaces have the dimensions computed by the corner dictionary.

theorem TauCeti.hasFiniteLaurentSupport_zigzagGradedProjective_hom (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i j : V) : HasFiniteLaurentSupport k fun (d : ℤ) => zigzagGradedProjective k G i ⟶ (zigzagGradedProjective k G j).shiftObj d

The categorical shifted Hom family has finite Laurent support. No cohomological vanishing assumption is needed to define its q-Hom polynomial.

theorem TauCeti.targetShiftGradedDimension_zigzagGradedProjective_hom (k : Type w) [Field k] {V : Type u} (G : SimpleGraph V) [Finite V] (hns : ∀ (i : V), ∃ (j : V), G.Adj i j) (i j : V) : targetShiftGradedDimension k (fun (d : ℤ) => zigzagGradedProjective k G i ⟶ (zigzagGradedProjective k G j).shiftObj d) ⋯ = zigzagProjectiveQHom k G hns i j

The q-Hom polynomial already computed from homogeneous maps is the target-shift graded dimension of the categorical Hom spaces.