Shifted projective homomorphisms and the componentwise trace

Evaluation at the vertex idempotent identifies graded maps P_i ⟶ P_j{s} with the degree -s part of the corner e_i Z e_j. The inverse is right multiplication by the corner vector. Composition, with the target shift applied to the second map, corresponds to multiplication of these vectors in the public componentwise zigzag algebra.

The corner trace pairing therefore pairs Hom(P_i, P_j{s}) perfectly with Hom(P_j, P_i{-2-s}). Its value is the trace of the composed underlying module map evaluated at the vertex generator. All shifts here are internal grading shifts.

The dictionary uses the existing graded idempotent evaluation equivalence TauCeti.GradedModuleCat.ofIdealSpanSingletonHomEquiv and its corner-piece calculation. Perfectness is transported from the signed graded corner pairing using Mathlib's LinearMap.IsPerfPair.compl₁₂; the induced dual equivalence is LinearMap.toPerfPair.

References

• Huerfano--Khovanov, A category for the adjoint representation, Sections 3 and 4.6.
• Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

noncomputable def TauCeti.zigzagAlgebraGradedProjectiveHomEquivCorner (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) : (fun (i j : V) (s : ℤ) => zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) i j s ≃ₗ[k] ↥((fun (i j : V) (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) i j (-s))

Evaluation at the vertex generator identifies maps into internal shift s with the signed degree-(-s) corner of the public componentwise algebra.

@[simp]

theorem TauCeti.coe_zigzagAlgebraGradedProjectiveHomEquivCorner_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) (f : zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) : ↑((zigzagAlgebraGradedProjectiveHomEquivCorner k G i j s) f) = ↑(f.hom (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))

The corner vector of a shifted graded map is its value at the source vertex generator.

@[simp]

theorem TauCeti.coe_zigzagAlgebraGradedProjectiveHomEquivCorner_symm_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) (x : ↥((fun (i j : V) (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) i j (-s))) (a : (zigzagAlgebraGradedProjective k G i).carrier) : ↑(((zigzagAlgebraGradedProjectiveHomEquivCorner k G i j s).symm x).hom a) = ↑a * ↑x

The inverse corner dictionary acts by right multiplication on the vertex ideal.

theorem TauCeti.coe_zigzagAlgebraGradedProjectiveHomEquivCorner_comp (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j l : V) (s t : ℤ) (f : zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) (g : zigzagAlgebraGradedProjective k G j ⟶ (zigzagAlgebraGradedProjective k G l).shiftObj t) : ↑((zigzagAlgebraGradedProjectiveHomEquivCorner k G i l (t + s)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((GradedModuleCat.shiftFunctor s).map g) ((GradedModuleCat.shiftFunctorAddIso (zigzagAlgebraIntegerGrade k G) t s).hom.app (zigzagAlgebraGradedProjective k G l))))) = ↑((zigzagAlgebraGradedProjectiveHomEquivCorner k G i j s) f) * ↑((zigzagAlgebraGradedProjectiveHomEquivCorner k G j l t) g)

Shifted composition corresponds to multiplication of corner vectors in the same order.

noncomputable def TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) : (fun (i j : V) (s : ℤ) => zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) i j s →ₗ[k] (fun (i j : V) (s : ℤ) => zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) j i (-2 - s) →ₗ[k] k

The componentwise trace pairs shifted graded projective maps in complementary internal shifts s and -2-s.

@[simp]

theorem TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) (f : zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) (g : zigzagAlgebraGradedProjective k G j ⟶ (zigzagAlgebraGradedProjective k G i).shiftObj (-2 - s)) : ((zigzagAlgebraGradedProjectiveHomTracePairing k G i j s) f) g = (zigzagAlgebraTrace k G) (↑(f.hom (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i))) * ↑(g.hom (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) j))))

The Hom pairing is the trace of the product of the two generator images.

theorem TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_eq_trace_comp (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) (f : zigzagAlgebraGradedProjective k G i ⟶ (zigzagAlgebraGradedProjective k G j).shiftObj s) (g : zigzagAlgebraGradedProjective k G j ⟶ (zigzagAlgebraGradedProjective k G i).shiftObj (-2 - s)) : ((zigzagAlgebraGradedProjectiveHomTracePairing k G i j s) f) g = (zigzagAlgebraTrace k G) ↑((CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((GradedModuleCat.shiftFunctor s).map g) ((GradedModuleCat.shiftFunctorAddIso (zigzagAlgebraIntegerGrade k G) (-2 - s) s).hom.app (zigzagAlgebraGradedProjective k G i)))).hom (spanSingletonGenerator ((fun (i : V) => (zigzagAlgebraBasis k G) (Sum.inl i)) i)))

The same pairing evaluates the shifted composite at the source generator and takes its trace. The composite has internal target shift (-2-s)+s = -2.

instance TauCeti.zigzagAlgebraGradedProjectiveHomTracePairing_isPerfPair (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (s : ℤ) : (zigzagAlgebraGradedProjectiveHomTracePairing k G i j s).IsPerfPair

Complementary shifted Hom spaces of actual componentwise vertex projectives are in perfect trace pairing over every commutative coefficient ring.