The graded resolution theorem

Let E be a graded exact category and P a class of E-projectives containing a zero object, closed under binary biproducts, and stable under the grading shift {1}. The resolution theorem TauCeti.ExactStructure.resolutionEquiv identifies the exact K₀ of P with the exact K₀ of the objects of finite P-dimension, the inverse sending [X] to the alternating class of any finite P-resolution of X.

Both full subcategories are shift-stable, so both carry induced graded exact structures and their Grothendieck groups are modules over ℤ[q,q⁻¹], with q acting by the shift. This file proves that the resolution isomorphism is an isomorphism of ℤ[q,q⁻¹]-modules. The forward map is induced by the graded conflation-exact inclusion, hence q-linear; the content is that the inverse, the Euler class of a finite resolution, is q-linear as well: the alternating class of any finite resolution of X{1} is q times the alternating class of any finite resolution of X.

Main definitions

• TauCeti.GradedExactStructure.laurentResolutionEquiv: the resolution isomorphism between the graded Grothendieck groups, as a ℤ[q,q⁻¹]-linear equivalence.

Main results

• TauCeti.GradedExactStructure.laurentResolutionEquiv_toLinearMap: its forward map is the map induced by the graded inclusion.
• TauCeti.GradedExactStructure.laurentResolutionEquiv_of and TauCeti.GradedExactStructure.laurentResolutionEquiv_symm_of: its values on classes; the inverse sends [X] to the alternating sum of the graded classes of the terms of any finite P-resolution of X.
• TauCeti.GradedExactStructure.foldAlternating_shift_eq_T_one_smul: the graded Euler class: the Euler class of X{1} is q times that of X.

Implementation notes

The underlying exact structure of TauCeti.GradedExactStructure.fullSubcategory equals the ungraded induced structure TauCeti.ExactStructure.fullSubcategory only propositionally, by TauCeti.GradedExactStructure.fullSubcategory_toExactStructure. The two exact K₀ groups are compared by the identity maps TauCeti.ExactK0.ofLE in both directions, and the ungraded resolution theorem is transported along them.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Theorem 7.6: the resolution theorem.
• Zsuzsanna Dancso and Anthony Licata, "Koszul algebras and flow lattices", Journal of Combinatorial Theory, Series A 185 (2022), Section 2.2, for graded Grothendieck groups as ℤ[q,q⁻¹]-modules with [M{1}] = q[M].

theorem TauCeti.GradedExactStructure.instIsClosedUnderIsomorphisms_1 {C : Type u} [CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} [P.ContainsZero] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

noncomputable def TauCeti.GradedExactStructure.laurentResolutionEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) : LaurentK0 (E.fullSubcategory P ⋯ hshift) ≃ₗ[LaurentPolynomial ℤ] LaurentK0 (E.fullSubcategory (E.admitsFiniteResolution P) ⋯ ⋯)

The graded resolution theorem. Let P be a class of E-projectives containing a zero object, closed under binary biproducts, and stable under the grading shift. Then the inclusion of P into the objects of finite P-dimension induces an isomorphism of graded Grothendieck groups as ℤ[q,q⁻¹]-modules. Its inverse sends the class of an object to its Euler class, by TauCeti.GradedExactStructure.laurentResolutionEquiv_symm_of.

Equations

• E.laurentResolutionEquiv hproj hshift = (TauCeti.GradedExactStructure.resolutionAddEquiv✝ E hproj hshift).toLinearEquiv ⋯

@[simp]

theorem TauCeti.GradedExactStructure.laurentResolutionEquiv_toLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) : ↑(E.laurentResolutionEquiv hproj hshift) = LaurentK0.map (GradedConflationExact.ιOfLE E P ⋯ ⋯ hshift ⋯ ⋯)

The forward map of the graded resolution isomorphism is the map induced by the graded conflation-exact inclusion of P into the objects of finite P-dimension.

@[simp]

theorem TauCeti.GradedExactStructure.laurentResolutionEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) (X : P.FullSubcategory) : (E.laurentResolutionEquiv hproj hshift) (LaurentK0.of (E.fullSubcategory P ⋯ hshift) X) = LaurentK0.of (E.fullSubcategory (E.admitsFiniteResolution P) ⋯ ⋯) { obj := X.obj, property := ⋯ }

The graded resolution isomorphism sends the class of a P-object to its class among the objects of finite P-dimension.

theorem TauCeti.GradedExactStructure.laurentResolutionEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) {X : C} (hX : E.admitsFiniteResolution P X) (r : E.FiniteResolution P X) : (E.laurentResolutionEquiv hproj hshift).symm (LaurentK0.of (E.fullSubcategory (E.admitsFiniteResolution P) ⋯ ⋯) { obj := X, property := hX }) = ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : P Z) => LaurentK0.of (E.fullSubcategory P ⋯ hshift) { obj := Z, property := hZ }) r

The inverse of the graded resolution isomorphism is the Euler class: it sends the class of an object of finite P-dimension to the alternating sum [Q₀] - [Q₁] + ⋯ + (-1)ⁿ [Kₙ] of the graded classes of the terms of any of its finite P-resolutions.

theorem TauCeti.GradedExactStructure.foldAlternating_shift_eq_T_one_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : GradedExactStructure C) [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P] [P.ContainsZero] [P.IsClosedUnderBinaryProducts] [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (E.admitsFiniteResolution P)] (hproj : P ≤ E.isProjective) (hshift : P.inverseImage E.shift.functor = P) {X : C} (r : E.FiniteResolution P X) (s : E.FiniteResolution P (E.shift.functor.obj X)) : ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : P Z) => LaurentK0.of (E.fullSubcategory P ⋯ hshift) { obj := Z, property := hZ }) s = LaurentPolynomial.T 1 • ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : P Z) => LaurentK0.of (E.fullSubcategory P ⋯ hshift) { obj := Z, property := hZ }) r

The graded Euler class. The alternating class of a finite P-resolution of X{1} is q times the alternating class of a finite P-resolution of X, in the graded Grothendieck group of P. The two resolutions are arbitrary: neither need be the shift of the other.