Documentation

TauCeti.CategoryTheory.GrothendieckGroup.Laurent.Resolving

The graded resolution theorem for resolving subcategories #

Let E be a graded exact category and let P be a resolving property for its underlying exact structure. If P is stable under the grading shift, then its induced exact structure is graded, and the inclusion of P into the ambient category induces an isomorphism

K₀^gr(P) ≃ K₀^gr(C)

of modules over ℤ[q,q⁻¹]. Its inverse sends the class of an object to the alternating class of any finite P-resolution. In particular, shifting an object and its resolution multiplies the Euler class by q.

The additive equivalence is the general resolution theorem of TauCeti.ExactStructure.IsResolving.resolutionEquiv. Laurent-linearity follows because its forward map is induced by the graded conflation-exact inclusion. Thus the common-refinement argument establishing independence and additivity of the Euler class is inherited unchanged from the ungraded theorem.

This differs from TauCeti.GradedExactStructure.laurentResolutionEquiv, which assumes that P consists of projectives and compares it with the full subcategory of objects of finite P-dimension. Here P is resolving, so every ambient object has a finite P-resolution, and the comparison is with the whole category.

A conflation-exact functor F into an ungraded exact category with {1} ⋙ F ≅ F, carrying P into a resolving property of the target, forgets the grading on both sides of this isomorphism; the resulting square commutes, so the specialization at q = 1 of the graded resolution class of an object is the resolution class of its image. The termwise form of that statement, for an arbitrary finite resolution rather than the resolution theorem, is TauCeti.GradedExactStructure.forgetGrading_foldAlternating.

Main definitions #

Main results #

References #

source
theorem TauCeti.GradedExactStructure.IsResolving.instEssentiallySmall {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (P : CategoryTheory.ObjectProperty C) :
CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P
source
noncomputable def TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) :
LaurentK0 (E.fullSubcategory P ⋯ hshift) ≃ₗ[LaurentPolynomial ℤ] LaurentK0 E

The graded resolution theorem for a resolving subcategory. If P is resolving for the underlying exact structure and stable under the grading shift, then inclusion induces an isomorphism of graded Grothendieck groups as ℤ[q,q⁻¹]-modules. Its inverse is computed by the Euler class of any finite P-resolution.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv_toLinearMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) :
    ↑(laurentResolutionEquiv E P hshift) = LaurentK0.map (GradedConflationExact.ι E P ⋯ hshift)

    The forward map of the graded resolution theorem is induced by the graded conflation-exact inclusion of the resolving subcategory.

    source
    @[simp]
    theorem TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) (X : P.FullSubcategory) :
    (laurentResolutionEquiv E P hshift) (LaurentK0.of (E.fullSubcategory P ⋯ hshift) X) = LaurentK0.of E X.obj

    The graded resolution equivalence sends the class of a resolving object to its ambient class.

    source
    theorem TauCeti.GradedExactStructure.IsResolving.laurentResolutionEquiv_symm_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) {X : C} (r : E.FiniteResolution P X) :
    (laurentResolutionEquiv E P hshift).symm (LaurentK0.of E X) = 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 equivalence is the Euler class. It sends the class of an object to the alternating sum [Q₀] - [Q₁] + ⋯ + (-1)ⁿ[Kₙ] of the graded classes of the terms of any finite P-resolution.

    source
    theorem TauCeti.GradedExactStructure.IsResolving.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] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (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

    Shift covariance of the graded Euler class. The alternating class of any finite P-resolution of X{1} is q times the alternating class of any finite P-resolution of X. The two resolutions need not be related.

    source
    theorem TauCeti.GradedExactStructure.IsResolving.instEssentiallySmall_1 {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {Q : CategoryTheory.ObjectProperty D} :
    CategoryTheory.ObjectProperty.EssentiallySmall.{w', v', u'} Q
    source
    theorem TauCeti.GradedExactStructure.IsResolving.forgetGrading_laurentResolutionEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [E'.IsResolving Q] {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hPQ : ∀ (Y : P.FullSubcategory), Q (F.obj Y.obj)) (x : LaurentK0 (E.fullSubcategory P ⋯ hshift)) :
    (LaurentK0.forgetGrading hF comm) ((LaurentSpecialization.mk 1) ((laurentResolutionEquiv E P hshift) x)) = (ExactStructure.IsResolving.resolutionEquiv E' Q) ((LaurentK0.forgetGrading ⋯ (E.liftCommShift P ⋯ hshift hPQ comm)) ((LaurentSpecialization.mk 1) x))

    Forgetting the grading commutes with the resolution theorems. A conflation-exact functor F into an ungraded exact category, with {1} ⋙ F ≅ F and carrying the resolving property P into the resolving property Q, makes the square formed by the graded resolution theorem, the ungraded resolution theorem and the two maps forgetting the grading commute.

    source
    theorem TauCeti.GradedExactStructure.IsResolving.forgetGrading_laurentResolutionEquiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (E : GradedExactStructure C) (P : CategoryTheory.ObjectProperty C) [E.IsResolving P] (hshift : P.inverseImage E.shift.functor = P) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {E' : ExactStructure D} {Q : CategoryTheory.ObjectProperty D} [E'.IsResolving Q] {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hPQ : ∀ (Y : P.FullSubcategory), Q (F.obj Y.obj)) (X : C) :
    (LaurentK0.forgetGrading ⋯ (E.liftCommShift P ⋯ hshift hPQ comm)) ((LaurentSpecialization.mk 1) ((laurentResolutionEquiv E P hshift).symm (LaurentK0.of E X))) = ExactStructure.eulerClassOf ⋯ ⋯

    Forgetting the grading of the graded resolution class. The graded Euler class of an object, specialized at q = 1, is the Euler class of its image: the two inverse resolution comparisons agree after forgetting the grading.