Forgetting the grading on a Grothendieck group

Let E be a graded exact category and let F be a conflation-exact functor from its underlying exact category to an ungraded exact category. If F identifies the grading shift with itself, then the induced map on exact Grothendieck groups identifies [M{1}] with [M]. Consequently it factors through the specialization of graded K₀ at q = 1.

This file constructs that factorization. It also characterizes surjectivity in terms of the original map on exact K₀, and injectivity in terms of the relations introduced by forgetting the grading. Establishing independently checkable hypotheses that imply these conditions requires additional structure and is not attempted here; shift compatibility by itself is not sufficient.

Main definitions

• TauCeti.LaurentK0.forgetGradingMap: the map from graded K₀ specialized at q = 1 to the exact K₀ of an ungraded target.

Main results

• TauCeti.LaurentK0.forgetGradingMap_mk_of: forgetting the grading sends the specialized class of M to the class of F(M).
• TauCeti.LaurentK0.forgetGradingMap_surjective_iff: the factor map is surjective exactly when the map before specialization is.
• TauCeti.LaurentK0.forgetGradingMap_injective_iff: the factor map is injective exactly when forgetting introduces no relations beyond specialization at q = 1.

References

• 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 and specialization at q = 1.

noncomputable def TauCeti.LaurentK0.forgetGradingUnderlyingMap {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) : LaurentK0 E →ₗ[ℤ] ExactK0 E'

The map on underlying exact Grothendieck groups, viewed as a ℤ-linear map whose source is graded K₀. This is the map which factors through specialization at q = 1.

Equations

• TauCeti.LaurentK0.forgetGradingUnderlyingMap hF = ((TauCeti.ExactK0.map F hF).comp (TauCeti.LaurentK0.ofExactK0 E).symm.toAddMonoidHom).toIntLinearMap

@[simp]

theorem TauCeti.LaurentK0.forgetGradingUnderlyingMap_ofExactK0 {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (x : ExactK0 E.toExactStructure) : (forgetGradingUnderlyingMap hF) ((ofExactK0 E) x) = (ExactK0.map F hF) x

@[simp]

theorem TauCeti.LaurentK0.forgetGradingUnderlyingMap_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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (X : C) : (forgetGradingUnderlyingMap hF) (of E X) = ExactK0.of (F.obj X)

theorem TauCeti.LaurentK0.forgetGradingUnderlyingMap_T_one {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (x : LaurentK0 E) : (forgetGradingUnderlyingMap hF) (LaurentPolynomial.T 1 • x) = (forgetGradingUnderlyingMap hF) x

If the functor identifies the grading shift with itself, its map on K₀ sends multiplication by q to the identity.

noncomputable def TauCeti.LaurentK0.forgetGradingMap {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) : LaurentSpecialization 1 (LaurentK0 E) →ₗ[ℤ] ExactK0 E'

The comparison after forgetting the grading. A conflation-exact functor which identifies its composite with the grading shift with itself induces a map from graded K₀ specialized at q = 1 to the exact Grothendieck group of its ungraded target.

Equations

• TauCeti.LaurentK0.forgetGradingMap hF comm = TauCeti.LaurentSpecialization.lift 1 (TauCeti.LaurentK0.forgetGradingUnderlyingMap hF) ⋯

@[simp]

theorem TauCeti.LaurentK0.forgetGradingMap_mk {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (x : LaurentK0 E) : (forgetGradingMap hF comm) ((LaurentSpecialization.mk 1) x) = (forgetGradingUnderlyingMap hF) x

The comparison is the expected map before passing to specialization.

theorem TauCeti.LaurentK0.forgetGradingMap_mk_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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (X : C) : (forgetGradingMap hF comm) ((LaurentSpecialization.mk 1) (of E X)) = ExactK0.of (F.obj X)

Forgetting the grading sends the specialized class of an object to the class of its image.

theorem TauCeti.LaurentK0.forgetGradingMap_unique {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (f : LaurentSpecialization 1 (LaurentK0 E) →ₗ[ℤ] ExactK0 E') (hf : ∀ (X : C), f ((LaurentSpecialization.mk 1) (of E X)) = ExactK0.of (F.obj X)) : f = forgetGradingMap hF comm

The comparison after forgetting grading is the unique linear map with its prescribed values on object classes.

theorem TauCeti.LaurentK0.forgetGradingMap_surjective_iff {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) : Function.Surjective ⇑(forgetGradingMap hF comm) ↔ Function.Surjective ⇑(ExactK0.map F hF)

The comparison after forgetting grading is surjective exactly when the original map on exact Grothendieck groups is surjective.

theorem TauCeti.LaurentK0.forgetGradingMap_injective_iff {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] {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 : GradedExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) : Function.Injective ⇑(forgetGradingMap hF comm) ↔ (forgetGradingUnderlyingMap hF).ker = Submodule.restrictScalars ℤ (RingHom.ker (laurentEval 1) • ⊤)

The comparison after forgetting grading is injective exactly when the kernel of the original map consists of the relations imposed by specialization at q = 1.