Documentation

TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Graded.GradedVectorSpace

The q-Euler form of graded vector spaces #

Let k be a field, and let TauCeti.GradedVectorSpace k be the category of ℤ-graded vector spaces with its grading shift (V{1})ᵢ = V_{i-1}, from TauCeti.Algebra.Category.GradedVectorSpace.Basic.

The one-dimensional space M = k placed in degree 0 is the smallest nontrivial test of the q-Euler formalism: it is projective, it is not isomorphic to any of its shifts M{j} with j ≠ 0, its degree-zero endomorphisms are one-dimensional, and it has no higher Ext. Hence

χ_q(M, M) = 1,    χ_q(M, M{1}) = q = q χ_q(M, M),    χ_q(M{1}, M) = q⁻¹ = q⁻¹ χ_q(M, M).

At q = 1 the three values agree, while at q = -1 a single shift changes the sign.

Forgetting the grading is the functor U taking the direct sum ⨁ᵢ Vᵢ of the pieces; it is invariant under the shift, {1} ⋙ U ≅ U, and U M ≅ k. In every cohomological degree the bigraded Ext groups of (M, M) assemble into the ungraded Ext groups of (U M, U M) in ModuleCat k; this is checked directly, by computing both sides, and it identifies the value of χ_q(M, M) at q = 1 with the ordinary Ext-Euler characteristic χ(U M, U M) = 1.

Main results #

Implementation notes #

The results hold for every choice of HasExt instances on the two categories: Ext groups are only used through their dimensions.

References #

source
theorem TauCeti.GradedVectorSpace.hasFiniteLaurentSupport_hom_unit (k : Type u) [Field k] :
HasFiniteLaurentSupport k fun (j : ℤ) => unit k ⟶ (shift k ^ j).functor.obj (unit k)

The graded morphism spaces Hom(M, M{j}) have finite Laurent support.

The q-Euler characteristic of M = unit k #

source
theorem TauCeti.GradedVectorSpace.isGradedEulerAdmissible_unit (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] :
IsGradedEulerAdmissible k (shift k) (unit k) (unit k)

The pair (M, M) is graded Euler-admissible: M is projective and its graded morphism spaces have finite Laurent support.

source
@[simp]
theorem TauCeti.GradedVectorSpace.gradedExtEuler_unit (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] :
gradedExtEuler k (shift k) ⋯ = 1

χ_q(M, M) = 1: the only surviving bigraded Ext group of (M, M) is the one-dimensional space of degree-zero endomorphisms.

source
@[simp]
theorem TauCeti.GradedVectorSpace.gradedExtEuler_unit_shiftTarget (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] (h : IsGradedEulerAdmissible k (shift k) (unit k) ((CategoryTheory.shiftFunctor (GradedVectorSpace k) 1).obj (unit k))) :
gradedExtEuler k (shift k) h = LaurentPolynomial.T 1

χ_q(M, M{1}) = q, that is, q · χ_q(M, M): the q-Euler form is q-linear in its second argument. This holds for any admissibility witness, e.g. (isGradedEulerAdmissible_unit k).shiftTarget; the shifted target is written as shiftFunctor _ 1, the simp-normal form of (shift k).functor.

source
@[simp]
theorem TauCeti.GradedVectorSpace.gradedExtEuler_unit_shiftSource (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] (h : IsGradedEulerAdmissible k (shift k) ((CategoryTheory.shiftFunctor (GradedVectorSpace k) 1).obj (unit k)) (unit k)) :
gradedExtEuler k (shift k) h = LaurentPolynomial.T (-1)

χ_q(M{1}, M) = q⁻¹, that is, q⁻¹ · χ_q(M, M): the q-Euler form is q-antilinear in its first argument. This holds for any admissibility witness, e.g. (isGradedEulerAdmissible_unit k).shiftSource; the shifted source is written as shiftFunctor _ 1, the simp-normal form of (shift k).functor.

source
theorem TauCeti.GradedVectorSpace.laurentEval_gradedExtEuler_unit_shiftTarget (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] (ε : ℤˣ) :
(laurentEval ε) (gradedExtEuler k (shift k) ⋯) = ↑ε

At q = ε for a unit ε : ℤˣ, the value χ_q(M, M{1}) becomes ε.

source
theorem TauCeti.GradedVectorSpace.laurentEval_gradedExtEuler_unit_shiftSource (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] (ε : ℤˣ) :
(laurentEval ε) (gradedExtEuler k (shift k) ⋯) = ↑ε⁻¹

At q = ε for a unit ε : ℤˣ, the value χ_q(M{1}, M) becomes ε⁻¹.

source
theorem TauCeti.GradedVectorSpace.laurentEval_neg_one_gradedExtEuler_unit_shiftTarget (k : Type u) [Field k] [CategoryTheory.HasExt (GradedVectorSpace k)] :
(laurentEval (-1)) (gradedExtEuler k (shift k) ⋯) = -(laurentEval (-1)) (gradedExtEuler k (shift k) ⋯)

At q = -1 a single shift changes the sign: χ_q(M, M{1}) specializes to the negative of the specialization of χ_q(M, M).

Comparison with the underlying ungraded pair (U M, U M) #

source
@[simp]
theorem TauCeti.GradedVectorSpace.extEuler_moduleCat_field_self (k : Type u) [Field k] [CategoryTheory.HasExt (ModuleCat k)] (h : IsEulerAdmissible k ↧k ↧k) :
extEuler k h = 1

The ungraded Ext-Euler characteristic χ(k, k) = 1 in ModuleCat k, for any admissibility witness: k is projective with one-dimensional endomorphisms.

source
theorem TauCeti.GradedVectorSpace.isGradedExtComparison_unit (k : Type u) [Field k] [CategoryTheory.HasExt (ModuleCat k)] [CategoryTheory.HasExt (GradedVectorSpace k)] :
IsGradedExtComparison k (shift k) (unit k) (unit k) ((CategoryTheory.GradedObject.total ℤ (ModuleCat k)).obj (unit k)) ((CategoryTheory.GradedObject.total ℤ (ModuleCat k)).obj (unit k))

The graded Ext groups of (M, M) assemble into the ungraded ones of (U M, U M): in each cohomological degree n, ⨁ j, Extⁿ(M, M{j}) ≅ Extⁿ_k(U M, U M). Both sides are computed: they are one-dimensional for n = 0 and zero otherwise.

source
theorem TauCeti.GradedVectorSpace.laurentEval_one_gradedExtEuler_unit (k : Type u) [Field k] [CategoryTheory.HasExt (ModuleCat k)] [CategoryTheory.HasExt (GradedVectorSpace k)] :
(laurentEval 1) (gradedExtEuler k (shift k) ⋯) = extEuler k ⋯

At q = 1 the q-Euler characteristic of (M, M) is the ordinary Ext-Euler characteristic of the underlying ungraded pair (U M, U M), as it must be after forgetting the grading.