The grading shift on the Grothendieck groups

The grading shift {1} of a graded exact category TauCeti.GradedExactStructure is an autoequivalence whose functor and inverse are both conflation-exact, so it induces an automorphism TauCeti.GradedExactStructure.shiftEquiv of the exact Grothendieck group, sending [M] to [M{1}]. Iterating it gives the ℤ-action TauCeti.GradedExactStructure.shiftZPow for which the Laurent-coefficient layer will read [M{n}] = qⁿ [M].

The underlying group of a graded category is not a new object: it is the corresponding ungraded K₀. Nothing is redefined here. The namespaces TauCeti.SplitK0, TauCeti.AbelianK0 and TauCeti.TriangulatedK0 provide the shift actions and graded universal properties for the split, abelian and triangulated products, while TauCeti.GradedExactStructure provides them for exact K₀.

The grading shift of a graded exact category is bundled with the exact structure, because the exact structure is itself data and the shift has to be compatible with the chosen one. In the split, abelian and triangulated cases the ambient structure is a typeclass, so no bundling is needed and the shift is passed as a bare autoequivalence, subject only to the hypotheses which make it act on the group in question: additivity, and in the triangulated case commutation with the suspension together with triangulatedness of the shift functor. Those triangulated hypotheses are lighter than the exact ones in one specific way, recorded at TauCeti.TriangulatedK0.shiftZPow: exactness of the inverse shift is a separate assumption for an exact category, whereas the inverse of a triangulated equivalence is automatically triangulated.

Main definitions

• TauCeti.GradedExactStructure.shiftEquiv: the automorphism [M] ↦ [M{1}] of exact K₀.
• TauCeti.GradedExactStructure.shiftZPow: the ℤ-action generated by that automorphism.
• TauCeti.GradedExactStructure.ShiftInvariant: a conflation-additive invariant equipped with a compatible invertible shift action.
• TauCeti.SplitK0.shiftZPow, TauCeti.AbelianK0.shiftZPow and TauCeti.TriangulatedK0.shiftZPow: the corresponding actions on split, abelian and triangulated K₀.
• TauCeti.TriangulatedK0.ShiftInvariant: a triangle-additive invariant equipped with a compatible invertible shift action.

Main results

• TauCeti.GradedExactStructure.ShiftInvariant.liftEquiv: the universal property of exact K₀ in the graded setting.
• TauCeti.GradedExactStructure.map_shiftEquiv: a graded conflation-exact functor induces a shift-equivariant homomorphism.
• TauCeti.GradedExactStructure.map_shiftEquiv_of_commShift: forgetting the grading along a conflation-exact functor which commutes with the shift induces a shift-invariant homomorphism.
• TauCeti.TriangulatedK0.ShiftInvariant.liftEquiv, TauCeti.TriangulatedK0.map_shiftEquiv and TauCeti.TriangulatedK0.map_shiftEquiv_of_commShift: the same three statements for triangulated K₀.
• TauCeti.TriangulatedK0.shiftZPow_of_shift: the grading shift and the suspension act on triangulated K₀ by commuting operators, the suspension acting by the sign (-1)ⁿ.
• TauCeti.TriangulatedK0.shiftZPow_apply_of_iso_shiftFunctor: a grading shift isomorphic to the suspension acts by (-1)ⁿ, so the action factors through the parity of n; it is never free, and it is nontrivial whenever some class is not its own negative.
• TauCeti.GradedExactStructure.fromSplit_shiftZPow and TauCeti.TriangulatedK0.fromSplit_shiftZPow: the comparisons out of graded split K₀ are equivariant.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Section 7, for the exact K₀ on which the grading shift acts here; the graded group is that group, and has no construction of its own.
• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Exercise II.9.15, for the triangulated K₀ on which the grading shift acts here.
• TauCetiRoadmap/GrothendieckEulerForms/README.md, Layer 2, which asks for the graded Grothendieck groups "each carrying the induced ℤ-action [M{n}] of the shift, with the universal property for invariants equipped with a compatible invertible shift action", and defers the Laurent-module repackaging of that action to Layer 6.

noncomputable def TauCeti.SplitK0.shiftZPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) : ℤ →+ AddAut (SplitK0 C)

The ℤ-action of a grading shift on split K₀, generated by the equivalence induced by the autoequivalence.

Equations

• TauCeti.SplitK0.shiftZPow e = (zmultiplesHom (AddAut (TauCeti.SplitK0 C))) (TauCeti.SplitK0.mapEquiv e)

@[simp]

theorem TauCeti.SplitK0.shiftZPow_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) (n : ℤ) : (shiftZPow e) n = n • mapEquiv e

theorem TauCeti.SplitK0.shiftZPow_one_apply_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) (X : C) : ((shiftZPow e) 1) (of X) = of (e.functor.obj X)

The generator of the split K₀ action sends an object class to the class of its shift.

theorem TauCeti.SplitK0.shiftZPow_add_one_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) (n : ℤ) (x : SplitK0 C) : ((shiftZPow e) (n + 1)) x = (mapEquiv e) (((shiftZPow e) n) x)

Shifting by n + 1 on split K₀ is shifting by n and then once more.

theorem TauCeti.SplitK0.shiftZPow_sub_one_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) (n : ℤ) (x : SplitK0 C) : ((shiftZPow e) (n - 1)) x = (mapEquiv e).symm (((shiftZPow e) n) x)

Shifting by n - 1 on split K₀ is shifting by n and then back once.

structure TauCeti.SplitK0.ShiftInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (e : C ≌ C) (σ : AddAut G) extends TauCeti.SplitK0.AdditiveInvariant C G : Type (max u u_1)

A biproduct-additive invariant equipped with a compatible invertible grading-shift action.

• obj : C → G
• map_iso ⦃X Y : C⦄ : ∀ (a : X ≅ Y), self.obj X = self.obj Y
• map_biprod (X Y : C) : self.obj (X ⊞ Y) = self.obj X + self.obj Y
• map_shift (X : C) : self.obj (e.functor.obj X) = σ (self.obj X)

  The invariant intertwines the grading shift with σ.

theorem TauCeti.SplitK0.ShiftInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_1} {inst✝³ : AddCommGroup G} {e : C ≌ C} {σ : AddAut G} {x y : ShiftInvariant C e σ} : x = y ↔ x.obj = y.obj

theorem TauCeti.SplitK0.ShiftInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝² : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_1} {inst✝³ : AddCommGroup G} {e : C ≌ C} {σ : AddAut G} {x y : ShiftInvariant C e σ} (obj : x.obj = y.obj) : x = y

noncomputable def TauCeti.SplitK0.ShiftInvariant.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} {σ : AddAut G} (a : ShiftInvariant C e σ) : SplitK0 C →+ G

The homomorphism out of split K₀ induced by a shift-compatible invariant.

Equations

• a.lift = TauCeti.SplitK0.lift a.toAdditiveInvariant

@[simp]

theorem TauCeti.SplitK0.ShiftInvariant.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} {σ : AddAut G} (a : ShiftInvariant C e σ) (X : C) : a.lift (of X) = a.obj X

theorem TauCeti.SplitK0.ShiftInvariant.lift_mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} {σ : AddAut G} (a : ShiftInvariant C e σ) (x : SplitK0 C) : a.lift ((mapEquiv e) x) = σ (a.lift x)

The induced homomorphism intertwines the grading shift with the target automorphism.

noncomputable def TauCeti.SplitK0.ShiftInvariant.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (e : C ≌ C) (σ : AddAut G) : ShiftInvariant C e σ ≃ { f : SplitK0 C →+ G // ∀ (x : SplitK0 C), f ((mapEquiv e) x) = σ (f x) }

The universal property of graded split K₀: shift-compatible biproduct-additive invariants correspond to homomorphisms intertwining the chosen automorphisms.

Equations

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

@[simp]

theorem TauCeti.SplitK0.ShiftInvariant.liftEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} {σ : AddAut G} (a : ShiftInvariant C e σ) : ↑((liftEquiv e σ) a) = a.lift

@[simp]

theorem TauCeti.SplitK0.ShiftInvariant.liftEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} {σ : AddAut G} (f : { f : SplitK0 C →+ G // ∀ (x : SplitK0 C), f ((mapEquiv e) x) = σ (f x) }) (X : C) : ((liftEquiv e σ).symm f).obj X = ↑f (of X)

noncomputable def TauCeti.AbelianK0.shiftZPow {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (e : A ≌ A) [e.functor.Additive] : ℤ →+ AddAut (AbelianK0 A)

The ℤ-action of a grading shift on abelian K₀, generated by the equivalence induced by the additive autoequivalence.

Equations

• TauCeti.AbelianK0.shiftZPow e = (zmultiplesHom (AddAut (TauCeti.AbelianK0 A))) (TauCeti.AbelianK0.mapEquiv e)

@[simp]

theorem TauCeti.AbelianK0.shiftZPow_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (e : A ≌ A) [e.functor.Additive] (n : ℤ) : (shiftZPow e) n = n • mapEquiv e

theorem TauCeti.AbelianK0.shiftZPow_one_apply_of {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (e : A ≌ A) [e.functor.Additive] (X : A) : ((shiftZPow e) 1) (of X) = of (e.functor.obj X)

The generator of the abelian K₀ action sends an object class to the class of its shift.

theorem TauCeti.AbelianK0.shiftZPow_add_one_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (e : A ≌ A) [e.functor.Additive] (n : ℤ) (x : AbelianK0 A) : ((shiftZPow e) (n + 1)) x = (mapEquiv e) (((shiftZPow e) n) x)

Shifting by n + 1 on abelian K₀ is shifting by n and then once more.

theorem TauCeti.AbelianK0.shiftZPow_sub_one_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] (e : A ≌ A) [e.functor.Additive] (n : ℤ) (x : AbelianK0 A) : ((shiftZPow e) (n - 1)) x = (mapEquiv e).symm (((shiftZPow e) n) x)

Shifting by n - 1 on abelian K₀ is shifting by n and then back once.

structure TauCeti.AbelianK0.ShiftInvariant (A : Type u) [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {G : Type u_1} [AddCommGroup G] (e : A ≌ A) [e.functor.Additive] (σ : AddAut G) extends TauCeti.AbelianK0.AdditiveInvariant A G : Type (max u u_1)

A short-exact-additive invariant equipped with a compatible invertible grading-shift action.

• obj : A → G
• map_shortExact ⦃S : CategoryTheory.ShortComplex A⦄ : S.ShortExact → self.obj S.X₂ = self.obj S.X₁ + self.obj S.X₃
• map_shift (X : A) : self.obj (e.functor.obj X) = σ (self.obj X)

  The invariant intertwines the grading shift with σ.

theorem TauCeti.AbelianK0.ShiftInvariant.ext {A : Type u} {inst✝ : CategoryTheory.Category.{v, u} A} {inst✝¹ : CategoryTheory.Abelian A} {G : Type u_1} {inst✝² : AddCommGroup G} {e : A ≌ A} {inst✝³ : e.functor.Additive} {σ : AddAut G} {x y : ShiftInvariant A e σ} (obj : x.obj = y.obj) : x = y

theorem TauCeti.AbelianK0.ShiftInvariant.ext_iff {A : Type u} {inst✝ : CategoryTheory.Category.{v, u} A} {inst✝¹ : CategoryTheory.Abelian A} {G : Type u_1} {inst✝² : AddCommGroup G} {e : A ≌ A} {inst✝³ : e.functor.Additive} {σ : AddAut G} {x y : ShiftInvariant A e σ} : x = y ↔ x.obj = y.obj

noncomputable def TauCeti.AbelianK0.ShiftInvariant.lift {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] {e : A ≌ A} [e.functor.Additive] {σ : AddAut G} (a : ShiftInvariant A e σ) : AbelianK0 A →+ G

The homomorphism out of abelian K₀ induced by a shift-compatible invariant.

Equations

• a.lift = TauCeti.AbelianK0.lift a.toAdditiveInvariant

@[simp]

theorem TauCeti.AbelianK0.ShiftInvariant.lift_of {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] {e : A ≌ A} [e.functor.Additive] {σ : AddAut G} (a : ShiftInvariant A e σ) (X : A) : a.lift (of X) = a.obj X

theorem TauCeti.AbelianK0.ShiftInvariant.lift_mapEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] {e : A ≌ A} [e.functor.Additive] {σ : AddAut G} (a : ShiftInvariant A e σ) (x : AbelianK0 A) : a.lift ((mapEquiv e) x) = σ (a.lift x)

The induced homomorphism intertwines the grading shift with the target automorphism.

noncomputable def TauCeti.AbelianK0.ShiftInvariant.liftEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] (e : A ≌ A) [e.functor.Additive] (σ : AddAut G) : ShiftInvariant A e σ ≃ { f : AbelianK0 A →+ G // ∀ (x : AbelianK0 A), f ((mapEquiv e) x) = σ (f x) }

The universal property of graded abelian K₀: shift-compatible short-exact-additive invariants correspond to homomorphisms intertwining the chosen automorphisms.

Equations

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

@[simp]

theorem TauCeti.AbelianK0.ShiftInvariant.liftEquiv_apply {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] {e : A ≌ A} [e.functor.Additive] {σ : AddAut G} (a : ShiftInvariant A e σ) : ↑((liftEquiv e σ) a) = a.lift

@[simp]

theorem TauCeti.AbelianK0.ShiftInvariant.liftEquiv_symm_apply_obj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] [CategoryTheory.EssentiallySmall.{w, v, u} A] {G : Type u_1} [AddCommGroup G] {e : A ≌ A} [e.functor.Additive] {σ : AddAut G} (f : { f : AbelianK0 A →+ G // ∀ (x : AbelianK0 A), f ((mapEquiv e) x) = σ (f x) }) (X : A) : ((liftEquiv e σ).symm f).obj X = ↑f (of X)

noncomputable def TauCeti.GradedExactStructure.shiftEquiv {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 ≃+ ExactK0 E.toExactStructure

The grading shift on exact K₀: the automorphism [M] ↦ [M{1}] induced by the grading shift of a graded exact category. Conflation-exactness of the shift and its inverse constructs this equivalence with the map induced by the inverse shift as its inverse.

Equations

• E.shiftEquiv = TauCeti.ExactK0.mapEquiv E.shift ⋯ ⋯

@[simp]

theorem TauCeti.GradedExactStructure.shiftEquiv_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) : E.shiftEquiv (ExactK0.of X) = ExactK0.of (E.shift.functor.obj X)

@[simp]

theorem TauCeti.GradedExactStructure.shiftEquiv_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) (X : C) : E.shiftEquiv.symm (ExactK0.of X) = ExactK0.of (E.shift.inverse.obj X)

theorem TauCeti.GradedExactStructure.shiftEquiv_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] (E : GradedExactStructure C) (f : ExactK0 E.toExactStructure →+ ExactK0 E.toExactStructure) (hf : ∀ (X : C), f (ExactK0.of X) = ExactK0.of (E.shift.functor.obj X)) : f = E.shiftEquiv.toAddMonoidHom

The grading shift is the unique endomorphism of exact K₀ sending the class of an object to the class of its shift.

noncomputable def TauCeti.GradedExactStructure.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) : ℤ →+ AddAut (ExactK0 E.toExactStructure)

The ℤ-action of the grading shift on exact K₀, sending n to the n-fold shift [M] ↦ [M{n}]. Mathlib writes the automorphism group of an additive group additively, so the n-fold shift is n • E.shiftEquiv; the Laurent-module repackaging of this action, in which it becomes multiplication by qⁿ, belongs to the coefficient layer downstream.

Equations

• E.shiftZPow = (zmultiplesHom (AddAut (TauCeti.ExactK0 E.toExactStructure))) E.shiftEquiv

@[simp]

theorem TauCeti.GradedExactStructure.shiftZPow_apply {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 : ℤ) : E.shiftZPow n = n • E.shiftEquiv

theorem TauCeti.GradedExactStructure.shiftZPow_one_apply_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) : (E.shiftZPow 1) (ExactK0.of X) = ExactK0.of (E.shift.functor.obj X)

The generator of the ℤ-action is the shift itself: [M{1}] is the class of M{1}.

theorem TauCeti.GradedExactStructure.shiftZPow_neg_one_apply {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 : ExactK0 E.toExactStructure) : (E.shiftZPow (-1)) x = E.shiftEquiv.symm x

The inverse generator of the ℤ-action is the inverse shift.

theorem TauCeti.GradedExactStructure.shiftZPow_neg_one_apply_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) : (E.shiftZPow (-1)) (ExactK0.of X) = ExactK0.of (E.shift.inverse.obj X)

theorem TauCeti.GradedExactStructure.shiftZPow_add_one_apply {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) : (E.shiftZPow (n + 1)) x = E.shiftEquiv ((E.shiftZPow n) x)

Shifting by n + 1 is shifting by n and then once more: this is [M{n+1}] = [(M{n}){1}].

theorem TauCeti.GradedExactStructure.shiftZPow_sub_one_apply {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) : (E.shiftZPow (n - 1)) x = E.shiftEquiv.symm ((E.shiftZPow n) x)

Shifting by n - 1 is shifting by n and then back once.

structure TauCeti.GradedExactStructure.ShiftInvariant {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {G : Type u_1} [AddCommGroup G] (E : GradedExactStructure C) (σ : AddAut G) extends TauCeti.ExactK0.AdditiveInvariant E.toExactStructure G : Type (max u u_1)

A conflation-additive invariant equipped with a compatible invertible shift action: its value on M{1} is the value on M moved by the given automorphism σ of the target.

• obj : C → G
• map_conflation ⦃S : CategoryTheory.ShortComplex C⦄ : E.Conflation S → self.obj S.X₂ = self.obj S.X₁ + self.obj S.X₃
• map_shift (X : C) : self.obj (E.shift.functor.obj X) = σ (self.obj X)

  The invariant intertwines the grading shift with σ.

theorem TauCeti.GradedExactStructure.ShiftInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_1} {inst✝⁴ : AddCommGroup G} {E : GradedExactStructure C} {σ : AddAut G} {x y : E.ShiftInvariant σ} : x = y ↔ x.obj = y.obj

theorem TauCeti.GradedExactStructure.ShiftInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.Limits.HasBinaryBiproducts C} {G : Type u_1} {inst✝⁴ : AddCommGroup G} {E : GradedExactStructure C} {σ : AddAut G} {x y : E.ShiftInvariant σ} (obj : x.obj = y.obj) : x = y

noncomputable def TauCeti.GradedExactStructure.ShiftInvariant.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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} {σ : AddAut G} (a : E.ShiftInvariant σ) : ExactK0 E.toExactStructure →+ G

The homomorphism out of exact K₀ induced by a shift-compatible invariant. It is the ungraded lift; the shift compatibility is extra information about it, not a change of construction.

Equations

• a.lift = TauCeti.ExactK0.lift a.toAdditiveInvariant

@[simp]

theorem TauCeti.GradedExactStructure.ShiftInvariant.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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} {σ : AddAut G} (a : E.ShiftInvariant σ) (X : C) : a.lift (ExactK0.of X) = a.obj X

theorem TauCeti.GradedExactStructure.ShiftInvariant.lift_shiftEquiv {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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} {σ : AddAut G} (a : E.ShiftInvariant σ) (x : ExactK0 E.toExactStructure) : a.lift (E.shiftEquiv x) = σ (a.lift x)

The induced homomorphism is shift-equivariant.

noncomputable def TauCeti.GradedExactStructure.ShiftInvariant.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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} (σ : AddAut G) : E.ShiftInvariant σ ≃ { f : ExactK0 E.toExactStructure →+ G // ∀ (x : ExactK0 E.toExactStructure), f (E.shiftEquiv x) = σ (f x) }

The universal property of exact K₀ in the graded setting: for a fixed automorphism σ of G, conflation-additive invariants compatible with the grading shift through σ correspond bijectively to the homomorphisms ExactK0 E →+ G intertwining the shift with σ.

Equations

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

@[simp]

theorem TauCeti.GradedExactStructure.ShiftInvariant.liftEquiv_apply {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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} {σ : AddAut G} (a : E.ShiftInvariant σ) : ↑((liftEquiv σ) a) = a.lift

@[simp]

theorem TauCeti.GradedExactStructure.ShiftInvariant.liftEquiv_symm_apply_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] {G : Type u_1} [AddCommGroup G] {E : GradedExactStructure C} {σ : AddAut G} (f : { f : ExactK0 E.toExactStructure →+ G // ∀ (x : ExactK0 E.toExactStructure), f (E.shiftEquiv x) = σ (f x) }) (X : C) : ((liftEquiv σ).symm f).obj X = ↑f (ExactK0.of X)

theorem TauCeti.GradedExactStructure.map_shiftEquiv {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} {F : CategoryTheory.Functor C D} [F.Additive] {E' : GradedExactStructure D} (h : GradedConflationExact E E' F) (x : ExactK0 E.toExactStructure) : (ExactK0.map F ⋯) (E.shiftEquiv x) = E'.shiftEquiv ((ExactK0.map F ⋯) x)

A graded conflation-exact functor induces a shift-equivariant homomorphism of exact Grothendieck groups: the commutation isomorphism with the two grading shifts is exactly what makes the square commute.

theorem TauCeti.GradedExactStructure.map_shiftEquiv_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] {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} {F : CategoryTheory.Functor C D} [F.Additive] {E' : GradedExactStructure D} (h : GradedConflationExact E E' F) (x : ExactK0 E.toExactStructure) : (ExactK0.map F ⋯) (E.shiftEquiv.symm x) = E'.shiftEquiv.symm ((ExactK0.map F ⋯) x)

The equivariance of the induced homomorphism for the inverse shift.

theorem TauCeti.GradedExactStructure.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] {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} {F : CategoryTheory.Functor C D} [F.Additive] {E' : GradedExactStructure D} (h : GradedConflationExact E E' F) (n : ℤ) (x : ExactK0 E.toExactStructure) : (ExactK0.map F ⋯) ((E.shiftZPow n) x) = (E'.shiftZPow n) ((ExactK0.map F ⋯) x)

Equivariance for the whole ℤ-action: a graded conflation-exact functor carries [M{n}] to [(FM){n}] for every integer n.

theorem TauCeti.GradedExactStructure.map_shiftEquiv_of_commShift {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} {F : CategoryTheory.Functor C D} [F.Additive] {E' : ExactStructure D} (hU : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (x : ExactK0 E.toExactStructure) : (ExactK0.map F hU) (E.shiftEquiv x) = (ExactK0.map F hU) x

Forgetting the grading. A conflation-exact functor into an ungraded exact category which commutes with the grading shift induces a homomorphism of exact Grothendieck groups sending the class of M{1} and the class of M to the same element, that is, one invariant under the grading shift.

The factorization of this map through the specialization of graded K₀ at q = 1, and sufficient hypotheses for the factored map to be an isomorphism, are TauCeti.LaurentK0.forgetGrading and TauCeti.LaurentK0.forgetGradingEquiv.

theorem TauCeti.GradedExactStructure.map_shiftZPow_of_commShift {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} {F : CategoryTheory.Functor C D} [F.Additive] {E' : ExactStructure D} (hU : E.IsConflationExact E' F) (comm : E.shift.functor.comp F ≅ F) (n : ℤ) (x : ExactK0 E.toExactStructure) : (ExactK0.map F hU) ((E.shiftZPow n) x) = (ExactK0.map F hU) x

Forgetting the grading is invariant under the whole ℤ-action, not only under the generating shift.

theorem TauCeti.GradedExactStructure.fromSplit_shiftEquiv {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 : SplitK0 C) : (ExactK0.fromSplit E.toExactStructure) ((SplitK0.mapEquiv E.shift) x) = E.shiftEquiv ((ExactK0.fromSplit E.toExactStructure) x)

The graded split Grothendieck group maps to the graded exact one. The shift of split K₀ is TauCeti.SplitK0.mapEquiv of the grading shift — no separate construction is needed, since every additive functor preserves split conflations — and the comparison homomorphism intertwines it with the shift of exact K₀.

theorem TauCeti.GradedExactStructure.fromSplit_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 : SplitK0 C) : (ExactK0.fromSplit E.toExactStructure) (((SplitK0.shiftZPow E.shift) n) x) = (E.shiftZPow n) ((ExactK0.fromSplit E.toExactStructure) x)

The comparison from graded split K₀ to graded exact K₀ intertwines the whole ℤ-action.

noncomputable def TauCeti.TriangulatedK0.shiftZPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] : ℤ →+ AddAut (TriangulatedK0 C)

The ℤ-action of a grading shift on triangulated K₀, generated by the isomorphism induced by the triangulated autoequivalence.

The hypotheses on the grading shift are lighter here than in the exact case. A graded exact category must record conflation-exactness of the inverse shift separately, because an autoequivalence can enlarge the class of conflations strictly; for a triangulated autoequivalence CategoryTheory.Equivalence.IsTriangulated.mk' derives the hypothesis on the inverse from the one on the functor, since the inverse is an adjoint of a triangulated functor.

Equations

• TauCeti.TriangulatedK0.shiftZPow e = (zmultiplesHom (AddAut (TauCeti.TriangulatedK0 C))) (TauCeti.TriangulatedK0.mapEquiv e)

@[simp]

theorem TauCeti.TriangulatedK0.shiftZPow_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (n : ℤ) : (shiftZPow e) n = n • mapEquiv e

theorem TauCeti.TriangulatedK0.shiftZPow_one_apply_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (X : C) : ((shiftZPow e) 1) (of X) = of (e.functor.obj X)

The generator of the triangulated K₀ action sends an object class to the class of its shift.

theorem TauCeti.TriangulatedK0.shiftZPow_add_one_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (n : ℤ) (x : TriangulatedK0 C) : ((shiftZPow e) (n + 1)) x = (mapEquiv e) (((shiftZPow e) n) x)

Shifting by n + 1 on triangulated K₀ is shifting by n and then once more.

theorem TauCeti.TriangulatedK0.shiftZPow_sub_one_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (n : ℤ) (x : TriangulatedK0 C) : ((shiftZPow e) (n - 1)) x = (mapEquiv e).symm (((shiftZPow e) n) x)

Shifting by n - 1 on triangulated K₀ is shifting by n and then back once.

theorem TauCeti.TriangulatedK0.of_functor_obj_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] (n : ℤ) (X : C) : of (e.functor.obj ((CategoryTheory.shiftFunctor C n).obj X)) = of ((CategoryTheory.shiftFunctor C n).obj (e.functor.obj X))

The grading shift commutes with the suspension. This is the commutation isomorphism carried by the grading shift, read at the level of object classes; it is what makes the grading shift of a graded triangulated category act on triangulated K₀ at all.

theorem TauCeti.TriangulatedK0.shiftZPow_of_shift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (n m : ℤ) (X : C) : ((shiftZPow e) n) (of ((CategoryTheory.shiftFunctor C m).obj X)) = ↑m.negOnePow • ((shiftZPow e) n) (of X)

The two shifts of a graded triangulated category on K₀. The suspension already acts by the sign (-1)ⁿ, so the grading action, being additive, absorbs it: internal degree and cohomological degree do not interact beyond that sign.

theorem TauCeti.TriangulatedK0.mapEquiv_apply_of_iso_shiftFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (h : e.functor ≅ CategoryTheory.shiftFunctor C 1) (x : TriangulatedK0 C) : (mapEquiv e) x = -x

A grading shift isomorphic to the suspension acts by -1. Nothing forbids the internal degree shift of a graded triangulated category from being the suspension itself, and then the generator of the ℤ-action is negation.

theorem TauCeti.TriangulatedK0.mapEquiv_symm_apply_of_iso_shiftFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (h : e.functor ≅ CategoryTheory.shiftFunctor C 1) (x : TriangulatedK0 C) : (mapEquiv e).symm x = -x

The inverse of a grading shift isomorphic to the suspension is again negation.

theorem TauCeti.TriangulatedK0.shiftZPow_apply_of_iso_shiftFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (h : e.functor ≅ CategoryTheory.shiftFunctor C 1) (n : ℤ) (x : TriangulatedK0 C) : ((shiftZPow e) n) x = ↑n.negOnePow • x

The ℤ-action of a grading shift isomorphic to the suspension is the sign action, [M{n}] = (-1)ⁿ[M]. The generator acts by negation, so the action factors through the parity of n: it is never free, and it is nontrivial exactly when some class is not its own negative — on a K₀ of exponent two, negation is the identity and the action collapses. Contrast TauCeti.GradedExactStructure.shiftZPow, where no such factorization is available, exact K₀ having no suspension to be isomorphic to.

structure TauCeti.TriangulatedK0.ShiftInvariant (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {G : Type u_1} [AddCommGroup G] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (σ : AddAut G) extends TauCeti.TriangulatedK0.AdditiveInvariant C G : Type (max u u_1)

A triangle-additive invariant equipped with a compatible invertible grading-shift action.

• obj : C → G
• map_distTriang ⦃T : CategoryTheory.Pretriangulated.Triangle C⦄ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → self.obj T.obj₂ = self.obj T.obj₁ + self.obj T.obj₃
• map_shift (X : C) : self.obj (e.functor.obj X) = σ (self.obj X)

  The invariant intertwines the grading shift with σ.

theorem TauCeti.TriangulatedK0.ShiftInvariant.ext {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁵ : CategoryTheory.Pretriangulated C} {G : Type u_1} {inst✝⁶ : AddCommGroup G} {e : C ≌ C} {inst✝⁷ : e.functor.CommShift ℤ} {inst✝⁸ : e.functor.IsTriangulated} {σ : AddAut G} {x y : ShiftInvariant C e σ} (obj : x.obj = y.obj) : x = y

theorem TauCeti.TriangulatedK0.ShiftInvariant.ext_iff {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {inst✝¹ : CategoryTheory.Preadditive C} {inst✝² : CategoryTheory.Limits.HasZeroObject C} {inst✝³ : CategoryTheory.HasShift C ℤ} {inst✝⁴ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} {inst✝⁵ : CategoryTheory.Pretriangulated C} {G : Type u_1} {inst✝⁶ : AddCommGroup G} {e : C ≌ C} {inst✝⁷ : e.functor.CommShift ℤ} {inst✝⁸ : e.functor.IsTriangulated} {σ : AddAut G} {x y : ShiftInvariant C e σ} : x = y ↔ x.obj = y.obj

noncomputable def TauCeti.TriangulatedK0.ShiftInvariant.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) : TriangulatedK0 C →+ G

The homomorphism out of triangulated K₀ induced by a shift-compatible invariant.

Equations

• a.lift = TauCeti.TriangulatedK0.lift a.toAdditiveInvariant

@[simp]

theorem TauCeti.TriangulatedK0.ShiftInvariant.lift_of {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) (X : C) : a.lift (of X) = a.obj X

theorem TauCeti.TriangulatedK0.ShiftInvariant.lift_mapEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) (x : TriangulatedK0 C) : a.lift ((mapEquiv e) x) = σ (a.lift x)

The induced homomorphism intertwines the grading shift with the target automorphism.

theorem TauCeti.TriangulatedK0.ShiftInvariant.lift_mapEquiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) (x : TriangulatedK0 C) : a.lift ((mapEquiv e).symm x) = (AddEquiv.symm σ) (a.lift x)

The induced homomorphism intertwines the inverse grading shift with the inverse target automorphism.

theorem TauCeti.TriangulatedK0.ShiftInvariant.lift_shiftZPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) (n : ℤ) (x : TriangulatedK0 C) : a.lift (((shiftZPow e) n) x) = (n • σ) (a.lift x)

The induced homomorphism intertwines the whole ℤ-action with the powers of the target automorphism.

noncomputable def TauCeti.TriangulatedK0.ShiftInvariant.liftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (σ : AddAut G) : ShiftInvariant C e σ ≃ { f : TriangulatedK0 C →+ G // ∀ (x : TriangulatedK0 C), f ((mapEquiv e) x) = σ (f x) }

The universal property of graded triangulated K₀: shift-compatible triangle-additive invariants correspond to homomorphisms intertwining the chosen automorphisms.

Equations

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

@[simp]

theorem TauCeti.TriangulatedK0.ShiftInvariant.liftEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (a : ShiftInvariant C e σ) : ↑((liftEquiv e σ) a) = a.lift

@[simp]

theorem TauCeti.TriangulatedK0.ShiftInvariant.liftEquiv_symm_apply_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddCommGroup G] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {σ : AddAut G} (f : { f : TriangulatedK0 C →+ G // ∀ (x : TriangulatedK0 C), f ((mapEquiv e) x) = σ (f x) }) (X : C) : ((liftEquiv e σ).symm f).obj X = ↑f (of X)

theorem TauCeti.TriangulatedK0.map_shiftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {e' : D ≌ D} [e'.functor.CommShift ℤ] [e'.functor.IsTriangulated] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (comm : e.functor.comp F ≅ F.comp e'.functor) (x : TriangulatedK0 C) : (map F) ((mapEquiv e) x) = (mapEquiv e') ((map F) x)

A graded triangulated functor induces a shift-equivariant homomorphism of triangulated Grothendieck groups: the commutation isomorphism with the two grading shifts is exactly what makes the square commute.

The isomorphism is a hypothesis here, where the exact case bundles it into TauCeti.GradedConflationExact. That bundling exists because a conflation-exact functor carries the two exact structures it relates as data; being triangulated is a typeclass on the functor, so there is nothing for a graded triangulated functor to bundle beyond this isomorphism.

theorem TauCeti.TriangulatedK0.map_shiftEquiv_symm {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {e' : D ≌ D} [e'.functor.CommShift ℤ] [e'.functor.IsTriangulated] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (comm : e.functor.comp F ≅ F.comp e'.functor) (x : TriangulatedK0 C) : (map F) ((mapEquiv e).symm x) = (mapEquiv e').symm ((map F) x)

The equivariance of the induced homomorphism for the inverse shift.

theorem TauCeti.TriangulatedK0.map_shiftZPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {e' : D ≌ D} [e'.functor.CommShift ℤ] [e'.functor.IsTriangulated] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (comm : e.functor.comp F ≅ F.comp e'.functor) (n : ℤ) (x : TriangulatedK0 C) : (map F) (((shiftZPow e) n) x) = ((shiftZPow e') n) ((map F) x)

Equivariance for the whole ℤ-action: a graded triangulated functor carries [M{n}] to [(FM){n}] for every integer n.

theorem TauCeti.TriangulatedK0.map_shiftEquiv_of_commShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (comm : e.functor.comp F ≅ F) (x : TriangulatedK0 C) : (map F) ((mapEquiv e) x) = (map F) x

Forgetting the grading. A triangulated functor into an ungraded pretriangulated category which commutes with the grading shift induces a homomorphism of triangulated Grothendieck groups sending the class of M{1} and the class of M to the same element, that is, one invariant under the grading shift.

As in the exact case, that invariance is the whole content: no factorization through a quotient of TauCeti.TriangulatedK0 is constructed, because the map from the graded group to the ungraded one is not an isomorphism in general, and shift compatibility alone supplies none of the extra hypotheses which make it one.

theorem TauCeti.TriangulatedK0.map_shiftZPow_of_commShift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated D] [CategoryTheory.EssentiallySmall.{w', v', u'} D] {e : C ≌ C} [e.functor.CommShift ℤ] [e.functor.IsTriangulated] {F : CategoryTheory.Functor C D} [F.CommShift ℤ] [F.IsTriangulated] (comm : e.functor.comp F ≅ F) (n : ℤ) (x : TriangulatedK0 C) : (map F) (((shiftZPow e) n) x) = (map F) x

Forgetting the grading is invariant under the whole ℤ-action, not only under the generating shift.

theorem TauCeti.TriangulatedK0.fromSplit_shiftEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (x : SplitK0 C) : (fromSplit C) ((SplitK0.mapEquiv e) x) = (mapEquiv e) ((fromSplit C) x)

The graded split Grothendieck group maps to the graded triangulated one. The shift of split K₀ is TauCeti.SplitK0.mapEquiv of the grading shift — a triangulated functor is in particular additive, and every additive functor preserves split conflations — and the comparison homomorphism intertwines it with the shift of triangulated K₀.

theorem TauCeti.TriangulatedK0.fromSplit_shiftZPow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.EssentiallySmall.{w, v, u} C] (e : C ≌ C) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (n : ℤ) (x : SplitK0 C) : (fromSplit C) (((SplitK0.shiftZPow e) n) x) = ((shiftZPow e) n) ((fromSplit C) x)

The comparison from graded split K₀ to graded triangulated K₀ intertwines the whole ℤ-action.