Graded vertex projectives of the componentwise zigzag algebra

For the public algebra Z = zigzagAlgebra k G, the ideal Z e_i is a finite graded projective in the signed componentwise grading. Its Laurent Grothendieck class represents an internal shift by multiplication by qᵈ.

These objects use the actual componentwise algebra. At an isolated vertex they retain the degree-two infinitesimal of the dual-number factor. The relation-quotient objects zigzagGradedProjective belong to a different algebra.

The construction uses GradedModuleCat.ofIdeal and the existing graded projective Grothendieck group and its shift computation.

theorem TauCeti.isHomogeneous_span_zigzagAlgebraBasis_inl (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : have x := zigzagAlgebraIntegerGradedAlgebra k G; Ideal.IsHomogeneous (zigzagAlgebraIntegerGrade k G) (Ideal.span {(fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i})

The principal vertex ideal is homogeneous for the canonical signed grading.

@[reducible, inline]

noncomputable abbrev TauCeti.zigzagAlgebraGradedProjective (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : GradedModuleCat (zigzagAlgebraIntegerGrade k G)

The graded principal left ideal Z e_i of the public componentwise algebra.

theorem TauCeti.mem_zigzagAlgebraGradedProjective_piece_iff (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) (d : ℤ) {x : (zigzagAlgebraGradedProjective k G i).carrier} : x ∈ (zigzagAlgebraGradedProjective k G i).grading.piece ℤ d ↔ ↑x ∈ zigzagAlgebraIntegerGrade k G d

The projective's grading is the restriction of the signed algebra grading.

theorem TauCeti.spanSingletonGenerator_mem_zigzagAlgebraGradedProjective_piece_zero (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i) ∈ (zigzagAlgebraGradedProjective k G i).grading.piece ℤ 0

The canonical vertex generator lies in degree zero of its graded projective.

theorem TauCeti.gradedFiniteProjectiveModules_zigzagAlgebraGradedProjective (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : gradedFiniteProjectiveModules (zigzagAlgebraIntegerGrade k G) (zigzagAlgebraGradedProjective k G i)

The vertex ideal is a finite projective over the public algebra.

noncomputable def TauCeti.zigzagAlgebraGradedProjectiveClass (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : LaurentK0 (gradedFiniteProjectiveModulesExactStructure (zigzagAlgebraIntegerGrade k G))

The class of the vertex projective in the actual Laurent projective Grothendieck group.

theorem TauCeti.zigzagAlgebraGradedProjectiveClass_def (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i : V) : zigzagAlgebraGradedProjectiveClass k G i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure (zigzagAlgebraIntegerGrade k G)) { obj := zigzagAlgebraGradedProjective k G i, property := ⋯ }

The named vertex-projective class is the class of its finite graded projective object.