Documentation

TauCeti.RepresentationTheory.Quiver.Zigzag.Componentwise.Corner.Trace

Perfect trace pairings between signed graded corners #

Multiplication followed by the canonical componentwise trace pairs the degree d part of e_i Z e_j perfectly with the degree 2 - d part of e_j Z e_i. This holds over a commutative ring, for every finite simple graph, including its isolated dual-number components.

The existing signed-corner spans reduce the pairing to dual vertex/volume or reverse-arrow basis vectors, or to two zero modules. The existing componentwise trace Gram formula supplies the coefficient one in each nonzero case; no scalar inversion or dimension argument is needed. The induced equivalence with the dual is Mathlib's LinearMap.toPerfPair.

Main declarations #

This is an internal graded pairing. It does not identify internal degree with cohomological degree or assert Serre duality or cohomological sphericity of a projective module.

References #

The corner spans and trace Gram formula are those already formalized in TauCeti.RepresentationTheory.Quiver.Zigzag.Componentwise.Corner.Grading and TauCeti.RepresentationTheory.Quiver.Zigzag.Componentwise.Trace. The grading and trace conventions follow Huerfano--Khovanov, A category for the adjoint representation, Section 3, and Ehrig--Tubbenhauer, Algebraic properties of zigzag algebras, Section 2.

source
noncomputable def TauCeti.zigzagAlgebraGradedCornerTracePairing (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (d : ℤ) :
↥((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 d) →ₗ[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) j i (2 - d)) →ₗ[k] k

Multiplication and the componentwise trace pair opposite corners in complementary signed internal degrees.

Instances For
    source
    @[simp]
    theorem TauCeti.zigzagAlgebraGradedCornerTracePairing_apply (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (d : ℤ) (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 d)) (y : ↥((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) j i (2 - d))) :
    ((zigzagAlgebraGradedCornerTracePairing k G i j d) x) y = (zigzagAlgebraTrace k G) (↑x * ↑y)

    The restricted pairing evaluates to the trace of the actual product in the public algebra.

    source
    instance TauCeti.zigzagAlgebraGradedCornerTracePairing_isPerfPair (k : Type w) [CommRing k] {V : Type u} [Finite V] (G : SimpleGraph V) (i j : V) (d : ℤ) :
    (zigzagAlgebraGradedCornerTracePairing k G i j d).IsPerfPair

    Opposite signed graded corners of the public componentwise zigzag algebra are in perfect trace pairing over any commutative coefficient ring, including at isolated vertices.