Graded Grothendieck groups of full subcategories

This file compares the exact Grothendieck groups associated to the graded and ungraded exact structures induced on a shift-stable, extension-closed full subcategory. It also records the transport of the Euler class of a finite resolution across this comparison, and the compatibility of that Euler class with forgetting the grading along a conflation-exact functor into an ungraded exact category.

Main results

• TauCeti.GradedExactStructure.ofExactK0_toUngraded_symm_eulerClassFullSubcategory: the graded Euler class of a finite resolution is the alternating sum of the graded classes of its terms.
• TauCeti.GradedExactStructure.forgetGrading_foldAlternating: at q = 1, forgetting the grading carries the graded Euler class of a finite resolution to the Euler class of its image resolution.

noncomputable def TauCeti.GradedExactStructure.toUngraded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) : ExactK0 (E.fullSubcategory R hR hRshift).toExactStructure ≃+ ExactK0 (ExactStructure.fullSubcategory R hR)

The graded and the ungraded induced exact structures on a full subcategory have the same conflations, so the identity functor compares their exact Grothendieck groups.

Equations

• E.toUngraded R hR hRshift = TauCeti.ExactK0.ofLEEquiv ⋯

@[simp]

theorem TauCeti.GradedExactStructure.toUngraded_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) (X : R.FullSubcategory) : (E.toUngraded R hR hRshift) (ExactK0.of X) = ExactK0.of X

The comparison with the ungraded induced structure fixes every object class.

@[simp]

theorem TauCeti.GradedExactStructure.toUngraded_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) (X : R.FullSubcategory) : (E.toUngraded R hR hRshift).symm (ExactK0.of X) = ExactK0.of X

The inverse comparison with the ungraded induced structure fixes every object class.

theorem TauCeti.GradedExactStructure.ofExactK0_toUngraded_symm_eulerClassFullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) {X : C} (r : E.FiniteResolution R X) : (LaurentK0.ofExactK0 (E.fullSubcategory R hR hRshift)) ((E.toUngraded R hR hRshift).symm (ExactStructure.FiniteResolution.eulerClassFullSubcategory hR r)) = ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) r

Transported to the graded Grothendieck group, the Euler class of a finite R-resolution is the alternating sum of the graded classes of its terms.

theorem TauCeti.GradedExactStructure.foldAlternating_shift_eq_T_one_smul_of_linearMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] (f : N →ₗ[LaurentPolynomial ℤ] LaurentK0 (E.fullSubcategory R hR hRshift)) {X : C} (r : E.FiniteResolution R X) (s : E.FiniteResolution R (E.shift.functor.obj X)) (x x' : N) (hr : f x = ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) r) (hs : f x' = ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) s) (hshift : x' = LaurentPolynomial.T 1 • x) : ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) s = LaurentPolynomial.T 1 • ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) r

A linear map transports shift covariance from two target classes to the Euler classes of finite resolutions that it computes.

theorem TauCeti.GradedExactStructure.forgetGrading_foldAlternating {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.LocallySmall.{w, v, u} C] (E : GradedExactStructure C) (R : CategoryTheory.ObjectProperty C) [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} R] [R.ContainsZero] [R.IsClosedUnderBinaryProducts] (hR : E.IsExtensionClosed R) (hRshift : R.inverseImage E.shift.functor = R) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.LocallySmall.{w', v', u'} D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [CategoryTheory.ObjectProperty.EssentiallySmall.{w', v', u'} Q] [Q.ContainsZero] [Q.IsClosedUnderBinaryProducts] (hQ : E'.IsExtensionClosed Q) {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hRQ : ∀ (Y : R.FullSubcategory), Q (F.obj Y.obj)) {X : C} (r : E.FiniteResolution R X) : (LaurentK0.forgetGrading ⋯ (E.liftCommShift R hR hRshift hRQ comm)) ((LaurentSpecialization.mk 1) (ExactStructure.FiniteResolution.foldAlternating (fun (Z : C) (hZ : R Z) => LaurentK0.of (E.fullSubcategory R hR hRshift) { obj := Z, property := hZ }) r)) = ExactStructure.FiniteResolution.eulerClassFullSubcategory hQ (ExactStructure.FiniteResolution.map hF ⋯ r)

Forgetting the grading of a finite resolution. Let F be a conflation-exact functor into an ungraded exact category with {1} ⋙ F ≅ F, carrying the shift-stable extension-closed property R into an extension-closed property Q. Applying F to a finite R-resolution of X gives a finite Q-resolution of F X, and the graded Euler class of the first, specialized at q = 1, is the Euler class of the second.

Both alternating sums are computed termwise, and forgetting the grading sends the graded class of each term to the ungraded class of its image.