Documentation

TauCeti.RepresentationTheory.GrothendieckGroup.GradedDualNumbers

The graded Cartan matrix of the dual numbers #

Let k be a field and grade the dual numbers A = k[ε] with ε in degree two (TauCeti.dualNumberIntegerGrade). The degree-zero piece of A is k, spanned by the idempotent 1, so up to internal shift A has one indecomposable finite graded projective, A itself, and one graded simple, the residue field S = A/(ε) concentrated in degree zero (TauCeti.dualNumberGradedResidue). The regular module has the graded composition factors S and S{2}, so the graded Cartan matrix of A is the one-by-one matrix 1 + q². These dual numbers are the factor of the zigzag algebra at an isolated vertex, where TauCeti.gradedCartanMatrix_zigzagAlgebra has the same diagonal entry 1 + q².

Its determinant 1 + q² is not a unit of ℤ[q,q⁻¹]: at q = 1 it becomes 2, the ungraded Cartan matrix of k[ε] (TauCeti.cartanMatrix_dualNumber). Graded Cartan unimodularity (TauCeti.isUnit_det_gradedCartanMatrix_gradedIdempotentProjectiveBasis) therefore fails for the only pair of graded simples: (S, S) is not graded Euler-admissible, so the q-Euler characteristic χ_q(S, S) is not defined and no totalised fallback value is exposed for it. This is the graded counterpart of the dual-numbers rejection TauCeti.not_isEulerAdmissible_dualNumberResidue. It also shows that S has no finite resolution by finite graded projectives, the graded counterpart of TauCeti.not_admitsFiniteResolution_dualNumberResidue.

Main definitions #

Main results #

Implementation notes #

The integer grading is installed with attribute [local instance] dualNumberIntegerGradedAlgebra, since TauCeti.dualNumberIntegerGradedAlgebra is a definition rather than a global instance. Importing modules activate it in the same way to restate these results.

References #

The idempotent data of the graded dual numbers #

The canonical bases #

source
noncomputable def TauCeti.dualNumberGradedProjectiveBasis (k : Type u) [Field k] :
Module.Basis Unit (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteProjectiveModulesExactStructure (dualNumberIntegerGrade k)))

The basis [A] of K₀^gr(proj A) over ℤ[q,q⁻¹], for the dual numbers A = k[ε] with ε in degree two.

Instances For
    source
    noncomputable def TauCeti.dualNumberGradedResidueBasis (k : Type u) [Field k] :
    Module.Basis Unit (LaurentPolynomial ℤ) (LaurentK0 (gradedFiniteModulesExactStructure (dualNumberIntegerGrade k)))

    The basis [S] of G₀^gr(mod A) over ℤ[q,q⁻¹] given by the graded residue field, for the dual numbers A = k[ε] with ε in degree two.

    Instances For
      source
      @[simp]
      theorem TauCeti.dualNumberGradedProjectiveBasis_apply (k : Type u) [Field k] (i : Unit) :
      (dualNumberGradedProjectiveBasis k) i = LaurentK0.of (gradedFiniteProjectiveModulesExactStructure (dualNumberIntegerGrade k)) { obj := GradedModuleCat.ofIdeal (dualNumberIntegerGrade k) (Ideal.span {1}) ⋯, property := ⋯ }

      The vector of TauCeti.dualNumberGradedProjectiveBasis is the class [A] of the regular module, as the graded ideal generated by 1.

      source
      @[simp]
      theorem TauCeti.dualNumberGradedResidueBasis_apply (k : Type u) [Field k] (i : Unit) :
      (dualNumberGradedResidueBasis k) i = LaurentK0.of (gradedFiniteModulesExactStructure (dualNumberIntegerGrade k)) { obj := dualNumberGradedResidue k, property := ⋯ }

      The vector of TauCeti.dualNumberGradedResidueBasis is the class [S] of the graded residue field.

      The graded Cartan matrix #

      source
      @[simp]
      theorem TauCeti.gradedCartanMatrix_dualNumber (k : Type u) [Field k] :
      gradedCartanMatrix (dualNumberIntegerGrade k) (dualNumberGradedProjectiveBasis k) (dualNumberGradedResidueBasis k) = Matrix.of fun (x x_1 : Unit) => 1 + LaurentPolynomial.T 2

      The graded Cartan matrix of the dual numbers is 1 + q², with ε in degree two, in the bases [A] and [S]: the regular module has the graded composition factors S and S{2}. At q = 1 this is the ungraded Cartan matrix 2 of TauCeti.cartanMatrix_dualNumber.

      source
      theorem TauCeti.det_gradedCartanMatrix_dualNumber (k : Type u) [Field k] :
      (gradedCartanMatrix (dualNumberIntegerGrade k) (dualNumberGradedProjectiveBasis k) (dualNumberGradedResidueBasis k)).det = 1 + LaurentPolynomial.T 2

      The graded Cartan matrix of the dual numbers has determinant 1 + q².

      source
      theorem TauCeti.not_isUnit_det_gradedCartanMatrix_dualNumber (k : Type u) [Field k] :
      ¬IsUnit (gradedCartanMatrix (dualNumberIntegerGrade k) (dualNumberGradedProjectiveBasis k) (dualNumberGradedResidueBasis k)).det

      The graded Cartan matrix of the dual numbers is not unimodular: its determinant 1 + q² is not a unit of ℤ[q,q⁻¹], because it evaluates to 2 at q = 1.

      The graded dual-numbers rejection #

      source
      theorem TauCeti.not_isGradedEulerAdmissible_dualNumberGradedResidue (k : Type u) [Field k] [CategoryTheory.HasExt (GradedModuleCat (dualNumberIntegerGrade k))] :
      ¬IsGradedEulerAdmissible k (GradedModuleCat.shift (dualNumberIntegerGrade k)) (dualNumberGradedResidue k) (dualNumberGradedResidue k)

      The graded dual-numbers rejection. The graded residue field S of k[ε], with ε in degree two, is not graded Euler-admissible against itself. Because TauCeti.gradedExtEuler consumes a proof of TauCeti.IsGradedEulerAdmissible, it cannot be instantiated for this pair.

      source
      theorem TauCeti.not_admitsFiniteResolution_dualNumberGradedResidue (k : Type u) [Field k] :
      ¬(gradedModuleCanonicalExactStructure (dualNumberIntegerGrade k)).admitsFiniteResolution (gradedFiniteProjectiveModules (dualNumberIntegerGrade k)) (dualNumberGradedResidue k)

      The graded residue field of k[ε] has no finite graded projective resolution: such a resolution would make (S, S) graded Euler-admissible.