The Laurent coefficient ring acting on the graded Grothendieck group

The grading shift {1} of a graded exact category acts on its exact Grothendieck group by the automorphism TauCeti.GradedExactStructure.shiftEquiv, and iterating it gives the ℤ-action TauCeti.GradedExactStructure.shiftZPow. Repackaging that ℤ-action as a module structure over ℤ[q,q⁻¹] = LaurentPolynomial ℤ is what turns graded K₀ into the lattice on which a q-Euler form can live.

TauCeti.LaurentK0 E is the graded Grothendieck group of a graded exact category E carrying that module structure. It is a type synonym for TauCeti.ExactK0 E.toExactStructure, moved across by the additive equivalence TauCeti.LaurentK0.ofExactK0: no new group is constructed, and no relation is added. The synonym exists only because the module structure depends on the grading shift, which the underlying exact structure does not remember. The defining property is TauCeti.LaurentK0.T_smul, the normalization [M{n}] = qⁿ [M] of the roadmap.

The universal property TauCeti.LaurentK0.liftEquiv is the ℤ[q,q⁻¹]-linear form of the graded one: for a ℤ[q,q⁻¹]-module N, the ℤ[q,q⁻¹]-linear maps out of LaurentK0 E are exactly the conflation-additive invariants a with a(M{1}) = q · a(M), that is, the shift-compatible invariants of TauCeti.GradedExactStructure.ShiftInvariant for the automorphism TauCeti.laurentTAut ℤ N of multiplication by q.

Specializing at q = ε for a unit ε : ℤˣ, that is at q = 1 or q = -1, is the base change TauCeti.LaurentSpecialization ε (LaurentK0 E) along evaluation at ε. There the grading shift acts by the scalar ε, so at q = -1 it changes the sign of a class and at q = 1 it fixes it.

Forgetting the grading along a conflation-exact functor F into an ungraded exact category with {1} ⋙ F ≅ F identifies the classes of M and M{1}, so it factors through the specialization at q = 1: this is TauCeti.LaurentK0.forgetGrading. The factored map need not be an isomorphism; TauCeti.LaurentK0.forgetGradingEquiv gives sufficient hypotheses under which it is, namely lifting of ungraded conflations up to isomorphism and equality at q = 1 of the classes of graded objects with isomorphic images.

Main definitions

• TauCeti.LaurentK0: the graded exact Grothendieck group as a ℤ[q,q⁻¹]-module.
• TauCeti.LaurentK0.ofExactK0: the additive equivalence with the underlying exact K₀.
• TauCeti.LaurentK0.of: the class [M] of an object.
• TauCeti.LaurentK0.lift: the ℤ[q,q⁻¹]-linear map induced by a shift-compatible invariant.
• TauCeti.LaurentK0.map: the ℤ[q,q⁻¹]-linear map induced by a graded conflation-exact functor.
• TauCeti.LaurentK0.mapEquiv: the isomorphism induced by a graded exact equivalence.
• TauCeti.LaurentK0.forgetGrading: forgetting the grading, as a map out of graded K₀ specialized at q = 1.
• TauCeti.LaurentK0.forgetGradingEquiv: the same map as an isomorphism, under sufficient hypotheses.

Main results

• TauCeti.LaurentK0.T_smul: qⁿ · [M] = [M{n}], and its generating cases TauCeti.LaurentK0.T_one_smul_of and TauCeti.LaurentK0.T_neg_one_smul_of.
• TauCeti.LaurentK0.liftEquiv: the universal property over the Laurent coefficient ring.
• TauCeti.LaurentK0.of_conflation: the defining relation [M₂] = [M₁] + [M₃] of a conflation.
• TauCeti.LaurentK0.hom_ext: a ℤ[q,q⁻¹]-linear map out of LaurentK0 E is determined by its values on object classes.
• TauCeti.LaurentK0.mk_ofExactK0_shiftZPow: the shift/sign formula [M{n}] = εⁿ[M] after specializing at q = ε; at q = -1 a shift changes the sign of a class, at q = 1 it does not change the class.
• TauCeti.LaurentK0.hom_ext_laurentSpecialization: a map out of specialized graded K₀ is determined by its values on object classes.
• TauCeti.LaurentK0.forgetGrading_mk_ofExactK0: the map induced on exact K₀ by forgetting the grading factors through the 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, Definition 2.3, where the graded Grothendieck group is presented as a ℤ[q,q⁻¹]-module with [M{1}] = q[M].
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 6, first bullet: "For a graded exact category from Layer 2, construct the R-module structure on its graded K₀ and prove [M{n}] = qⁿ[M] for every n : ℤ, in particular [M{1}] = q[M]. State the universal property for additive invariants equipped with a compatible invertible shift action."

def TauCeti.LaurentK0 {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) : Type w

The graded Grothendieck group of a graded exact category, over the Laurent coefficient ring. The underlying additive group is the exact Grothendieck group of the underlying exact structure; the grading shift makes it a module over ℤ[q,q⁻¹], with q acting as [M] ↦ [M{1}].

The type synonym is needed because a ℤ[q,q⁻¹]-module structure is determined by an automorphism of the group, and ExactK0 E.toExactStructure does not mention the grading shift. Use TauCeti.LaurentK0.ofExactK0 to move between the two views.

Equations

• TauCeti.LaurentK0 E = TauCeti.ExactK0 E.toExactStructure

@[instance_reducible]

instance TauCeti.LaurentK0.instAddCommGroup {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) : AddCommGroup (LaurentK0 E)

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.LaurentK0.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] (E : GradedExactStructure C) : ExactK0 E.toExactStructure ≃+ LaurentK0 E

The graded Grothendieck group is the exact one. Moving a class across this equivalence changes nothing but which module structure is in scope.

Equations

• TauCeti.LaurentK0.ofExactK0 E = AddEquiv.refl (TauCeti.ExactK0 E.toExactStructure)

@[instance_reducible]

noncomputable instance TauCeti.LaurentK0.instModuleLaurentPolynomialInt {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) : Module (LaurentPolynomial ℤ) (LaurentK0 E)

The Laurent coefficient ring acts on the graded Grothendieck group, the variable acting by the grading shift.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LaurentK0.T_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) (n : ℤ) (x : ExactK0 E.toExactStructure) : LaurentPolynomial.T n • (ofExactK0 E) x = (ofExactK0 E) ((E.shiftZPow n) x)

qⁿ · [M] = [M{n}]: the Laurent variable acts on the graded Grothendieck group by the grading shift, and its n-th power by the n-fold shift. This is the normalization fixed by the roadmap, and it determines the module structure.

noncomputable def TauCeti.LaurentK0.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) (X : C) : LaurentK0 E

The class [M] of an object in the graded Grothendieck group.

Equations

• TauCeti.LaurentK0.of E X = (TauCeti.LaurentK0.ofExactK0 E) (TauCeti.ExactK0.of X)

@[simp]

theorem TauCeti.LaurentK0.ofExactK0_exactK0_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) (X : C) : (ofExactK0 E) (ExactK0.of X) = of E X

theorem TauCeti.LaurentK0.of_congr {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) {X Y : C} (e : X ≅ Y) : of E X = of E Y

Isomorphic objects have the same class.

theorem TauCeti.LaurentK0.of_conflation {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) {S : CategoryTheory.ShortComplex C} (hS : E.Conflation S) : of E S.X₂ = of E S.X₁ + of E S.X₃

The defining relation of graded K₀: the class of the middle term of a conflation is the sum of the classes of its outer terms. The grading plays no role, so this is ExactK0.of_conflation moved across TauCeti.LaurentK0.ofExactK0.

@[simp]

theorem TauCeti.LaurentK0.T_one_smul_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) (X : C) : LaurentPolynomial.T 1 • of E X = of E (E.shift.functor.obj X)

q · [M] = [M{1}].

@[simp]

theorem TauCeti.LaurentK0.T_neg_one_smul_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) (X : C) : LaurentPolynomial.T (-1) • of E X = of E (E.shift.inverse.obj X)

q⁻¹ · [M] = [M{-1}].

instance TauCeti.LaurentK0.instIsScalarTowerIntLaurentPolynomial {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) : IsScalarTower ℤ (LaurentPolynomial ℤ) (LaurentK0 E)

The Laurent action restricts along the constants to the underlying integer action: an integer scalar may be pushed through a Laurent scalar. This is the content of TauCeti.laurentPolynomialC_smul in the form Module consumers need, and it is what lets ℤ-linear arguments about the underlying group be reused verbatim over ℤ[q,q⁻¹].

theorem TauCeti.LaurentK0.hom_ext {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) {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] {f g : LaurentK0 E →ₗ[LaurentPolynomial ℤ] N} (h : ∀ (X : C), f (of E X) = g (of E X)) : f = g

A ℤ[q,q⁻¹]-linear map out of the graded Grothendieck group is determined by its values on object classes, because those classes generate the underlying group.

theorem TauCeti.LaurentK0.map_shiftZPow {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} {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] (f : ExactK0 E.toExactStructure →+ N) (hf : ∀ (x : ExactK0 E.toExactStructure), f (E.shiftEquiv x) = LaurentPolynomial.T 1 • f x) (n : ℤ) (x : ExactK0 E.toExactStructure) : f ((E.shiftZPow n) x) = LaurentPolynomial.T n • f x

An additive map out of the exact Grothendieck group which turns the grading shift into multiplication by q turns the whole ℤ-action into multiplication by qⁿ.

noncomputable def TauCeti.LaurentK0.lift {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) {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] (a : E.ShiftInvariant (laurentTAut ℤ N)) : LaurentK0 E →ₗ[LaurentPolynomial ℤ] N

The homomorphism out of graded K₀ induced by a shift-compatible invariant, as a map of ℤ[q,q⁻¹]-modules. The invariant is compared against multiplication by q on the target.

Equations

• TauCeti.LaurentK0.lift E a = TauCeti.LaurentK0.liftAux✝ a.lift ⋯

@[simp]

theorem TauCeti.LaurentK0.lift_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} {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] (a : E.ShiftInvariant (laurentTAut ℤ N)) (X : C) : (lift E a) (of E X) = a.obj X

noncomputable def TauCeti.LaurentK0.liftEquiv {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) {N : Type u_1} [AddCommGroup N] [Module (LaurentPolynomial ℤ) N] : E.ShiftInvariant (laurentTAut ℤ N) ≃ (LaurentK0 E →ₗ[LaurentPolynomial ℤ] N)

The universal property of graded K₀ over the Laurent coefficient ring. For a ℤ[q,q⁻¹]-module N, the ℤ[q,q⁻¹]-linear maps out of LaurentK0 E correspond bijectively to the conflation-additive invariants whose value on M{1} is q times the value on M.

This is the Layer 2 universal property of a shift-compatible invariant, with the abstract automorphism of the target replaced by the one the coefficient ring supplies.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.LaurentK0.map {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} {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 D} {F : CategoryTheory.Functor C D} [F.Additive] (h : GradedConflationExact E E' F) : LaurentK0 E →ₗ[LaurentPolynomial ℤ] LaurentK0 E'

A graded conflation-exact functor induces a ℤ[q,q⁻¹]-linear map of graded Grothendieck groups: the shift-equivariance proved in the ℤ-graded layer is exactly q-linearity.

Equations

• TauCeti.LaurentK0.map h = TauCeti.LaurentK0.liftAux✝ ((TauCeti.LaurentK0.ofExactK0 E').toAddMonoidHom.comp (TauCeti.ExactK0.map F ⋯)) ⋯

@[simp]

theorem TauCeti.LaurentK0.map_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} {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 D} {F : CategoryTheory.Functor C D} [F.Additive] (h : GradedConflationExact E E' F) (X : C) : (map h) (of E X) = of E' (F.obj X)

@[simp]

theorem TauCeti.LaurentK0.map_id {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} : map (GradedConflationExact.id E) = LinearMap.id

The identity functor induces the identity map of graded Grothendieck groups.

@[simp]

theorem TauCeti.LaurentK0.map_comp {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} {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 D} {F : CategoryTheory.Functor C D} [F.Additive] {K : Type u''} [CategoryTheory.Category.{v'', u''} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] [CategoryTheory.EssentiallySmall.{w'', v'', u''} K] {E'' : GradedExactStructure K} {H : CategoryTheory.Functor D K} [H.Additive] (h : GradedConflationExact E E' F) (h' : GradedConflationExact E' E'' H) : map (h.comp h') = map h' ∘ₗ map h

LaurentK0.map is functorial: a composite of graded conflation-exact functors induces the composite ℤ[q,q⁻¹]-linear map.

noncomputable def TauCeti.LaurentK0.mapEquiv {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} {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 D} (h : GradedExactEquiv E E') : LaurentK0 E ≃ₗ[LaurentPolynomial ℤ] LaurentK0 E'

A graded exact equivalence induces an isomorphism of ℤ[q,q⁻¹]-modules. Graded K₀ over the Laurent coefficient ring is therefore an invariant of the graded exact category, not of a presentation of it.

Equations

• TauCeti.LaurentK0.mapEquiv h = LinearEquiv.ofLinearMap (TauCeti.LaurentK0.map h.toGradedConflationExact) (TauCeti.LaurentK0.map h.symm.toGradedConflationExact) ⋯ ⋯

@[simp]

theorem TauCeti.LaurentK0.mapEquiv_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} {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 D} (h : GradedExactEquiv E E') (X : C) : (mapEquiv h) (of E X) = of E' (h.equiv.functor.obj X)

@[simp]

theorem TauCeti.LaurentK0.mapEquiv_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} {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 D} (h : GradedExactEquiv E E') (X : D) : (mapEquiv h).symm (of E' X) = of E (h.equiv.inverse.obj X)

theorem TauCeti.LaurentK0.mk_ofExactK0_shiftZPow {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} (ε : ℤˣ) (n : ℤ) (x : ExactK0 E.toExactStructure) : (LaurentSpecialization.mk ε) ((ofExactK0 E) ((E.shiftZPow n) x)) = ↑(ε ^ n) • (LaurentSpecialization.mk ε) ((ofExactK0 E) x)

The shift/sign formula of specialized graded K₀. After specializing at q = ε, the n-fold grading shift multiplies a class by εⁿ. At q = -1 this is the sign (-1)ⁿ, and at q = 1 all shifts of an object have the same specialized class.

@[simp]

theorem TauCeti.LaurentK0.mk_of_shift_functor_obj {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} (ε : ℤˣ) (X : C) : (LaurentSpecialization.mk ε) (of E (E.shift.functor.obj X)) = ↑ε • (LaurentSpecialization.mk ε) (of E X)

After specializing at q = ε, the class of M{1} is ε times the class of M.

theorem TauCeti.LaurentK0.hom_ext_laurentSpecialization {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} (ε : ℤˣ) {A : Type u_1} [AddCommGroup A] {f g : LaurentSpecialization ε (LaurentK0 E) →ₗ[ℤ] A} (h : ∀ (X : C), f ((LaurentSpecialization.mk ε) (of E X)) = g ((LaurentSpecialization.mk ε) (of E X))) : f = g

A map out of specialized graded K₀ is determined by its values on object classes.

theorem TauCeti.LaurentK0.hom_ext_laurentSpecialization_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] {E : GradedExactStructure C} {ε : ℤˣ} {A : Type u_1} [AddCommGroup A] {f g : LaurentSpecialization ε (LaurentK0 E) →ₗ[ℤ] A} : f = g ↔ ∀ (X : C), f ((LaurentSpecialization.mk ε) (of E X)) = g ((LaurentSpecialization.mk ε) (of E X))

noncomputable def TauCeti.LaurentK0.forgetGrading {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} {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} {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'

Forgetting the grading, through the specialization at q = 1. A conflation-exact functor F into an ungraded exact category with {1} ⋙ F ≅ F induces a map from graded K₀, specialized at q = 1, to the ungraded K₀, sending the specialized class of M to the class of F M.

By TauCeti.LaurentK0.forgetGrading_mk_ofExactK0 this factors the map ExactK0.map F induced on the underlying exact K₀ through the specialization; it is not an isomorphism in general, see TauCeti.LaurentK0.forgetGradingEquiv for sufficient hypotheses.

Equations

• TauCeti.LaurentK0.forgetGrading hF comm = TauCeti.LaurentSpecialization.lift 1 ((TauCeti.ExactK0.map F hF).comp (TauCeti.LaurentK0.ofExactK0 E).symm.toAddMonoidHom).toIntLinearMap ⋯

@[simp]

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

The forgetful map on graded K₀ factors through the specialization at q = 1: forgetting the grading of a specialized class is the map induced by F on the underlying exact K₀.

@[simp]

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

Forgetting the grading sends the specialized class of M to the class of F M.

noncomputable def TauCeti.LaurentK0.forgetGradingEquiv {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} {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} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hlift : ∀ (S : CategoryTheory.ShortComplex D), E'.Conflation S → ∃ (S' : CategoryTheory.ShortComplex C), E.Conflation S' ∧ Nonempty (F.obj S'.X₁ ≅ S.X₁) ∧ Nonempty (F.obj S'.X₂ ≅ S.X₂) ∧ Nonempty (F.obj S'.X₃ ≅ S.X₃)) (hclass : ∀ (X X' : C), Nonempty (F.obj X ≅ F.obj X') → (LaurentSpecialization.mk 1) (of E X) = (LaurentSpecialization.mk 1) (of E X')) : LaurentSpecialization 1 (LaurentK0 E) ≃ₗ[ℤ] ExactK0 E'

Sufficient hypotheses for forgetting the grading to be an isomorphism at q = 1. Let F be a conflation-exact functor into an ungraded exact category with {1} ⋙ F ≅ F. Suppose that

• every conflation Y₁ ↪ Y₂ ↠ Y₃ of the ungraded category lifts, up to isomorphism of each term, to a graded conflation M₁ ↪ M₂ ↠ M₃ with F Mᵢ ≅ Yᵢ (applied to 0 ↪ Y ↠ Y, this makes F essentially surjective), and
• two graded objects with isomorphic images under F have the same class at q = 1.

Then TauCeti.LaurentK0.forgetGrading is an isomorphism, whose inverse sends the class of F M to the specialized class of M. The second hypothesis is also necessary for injectivity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LaurentK0.forgetGradingEquiv_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} {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} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hlift : ∀ (S : CategoryTheory.ShortComplex D), E'.Conflation S → ∃ (S' : CategoryTheory.ShortComplex C), E.Conflation S' ∧ Nonempty (F.obj S'.X₁ ≅ S.X₁) ∧ Nonempty (F.obj S'.X₂ ≅ S.X₂) ∧ Nonempty (F.obj S'.X₃ ≅ S.X₃)) (hclass : ∀ (X X' : C), Nonempty (F.obj X ≅ F.obj X') → (LaurentSpecialization.mk 1) (of E X) = (LaurentSpecialization.mk 1) (of E X')) : ↑(forgetGradingEquiv hF comm hlift hclass) = forgetGrading hF comm

The forward linear map of TauCeti.LaurentK0.forgetGradingEquiv is TauCeti.LaurentK0.forgetGrading.

@[simp]

theorem TauCeti.LaurentK0.forgetGradingEquiv_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} {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} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (hlift : ∀ (S : CategoryTheory.ShortComplex D), E'.Conflation S → ∃ (S' : CategoryTheory.ShortComplex C), E.Conflation S' ∧ Nonempty (F.obj S'.X₁ ≅ S.X₁) ∧ Nonempty (F.obj S'.X₂ ≅ S.X₂) ∧ Nonempty (F.obj S'.X₃ ≅ S.X₃)) (hclass : ∀ (X X' : C), Nonempty (F.obj X ≅ F.obj X') → (LaurentSpecialization.mk 1) (of E X) = (LaurentSpecialization.mk 1) (of E X')) (X : C) : (forgetGradingEquiv hF comm hlift hclass).symm (ExactK0.of (F.obj X)) = (LaurentSpecialization.mk 1) (of E X)

The inverse of TauCeti.LaurentK0.forgetGradingEquiv sends the class of F M to the specialized class of M.