Triangulated K₀ of a pretriangulated category

The triangulated Grothendieck group TauCeti.TriangulatedK0 C of an essentially small pretriangulated category C is the free abelian group on the isomorphism classes of objects modulo the relations [Y] = [X] + [Z], one for each distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧. It is the universal recipient of an invariant which is constant on isomorphism classes and additive on distinguished triangles.

The construction is the presentation engine of TauCeti/CategoryTheory/GrothendieckGroup/Presentation.lean applied to the triangle relations, so the skeleton and shrink choices are made once and for all there, and the whole public API below is phrased in terms of objects and distinguished triangles of C.

Unlike exact K₀, triangulated K₀ sees the shift: the distinguished triangle X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧ forces [X⟦1⟧] = -[X], hence [X⟦n⟧] = (-1)ⁿ[X] for every integer n. The sign is recorded by Int.negOnePow, so that one statement covers negative shifts as well. The biproduct triangles are distinguished, so the class map is additive on biproducts and TauCeti.TriangulatedK0.fromSplit compares split K₀ with triangulated K₀.

Main definitions

• TauCeti.triangleRelation T: the relation [T.obj₂] - [T.obj₁] - [T.obj₃] attached to a triangle, and TauCeti.triangulatedRelations C the family of those attached to the distinguished triangles.
• TauCeti.TriangulatedK0 C: triangulated K₀, with class map TauCeti.TriangulatedK0.of.
• TauCeti.TriangulatedK0.AdditiveInvariant C G: an isomorphism-invariant, triangle-additive function on objects, and TauCeti.TriangulatedK0.lift the homomorphism it induces.
• TauCeti.TriangulatedK0.map and TauCeti.TriangulatedK0.mapEquiv: functoriality for triangulated functors and invariance under triangulated equivalences.
• TauCeti.TriangulatedK0.fromSplit: the canonical comparison from split K₀.

Main results

• TauCeti.TriangulatedK0.of_distTriang: the defining relation, with TauCeti.TriangulatedK0.of_biprod and TauCeti.TriangulatedK0.of_eq_zero_of_isZero its biproduct and zero-object consequences.
• TauCeti.TriangulatedK0.of_fullSubcategory_distTriang: in a full triangulated subcategory, a distinguished triangle of the ambient category with vertices in the subcategory gives the defining relation.
• TauCeti.TriangulatedK0.of_shift_one and TauCeti.TriangulatedK0.of_shift: the class of a shift, [X⟦1⟧] = -[X] and [X⟦n⟧] = (-1)ⁿ[X].
• TauCeti.TriangulatedK0.liftEquiv: the universal property. Triangle-additive invariants with values in G correspond bijectively to homomorphisms TriangulatedK0 C →+ G.
• TauCeti.TriangulatedK0.fromSplit_surjective and TauCeti.TriangulatedK0.map_comp_fromSplit: triangulated K₀ is a quotient of split K₀, naturally in a triangulated functor.

References

• Charles A. Weibel, The K-book: An Introduction to Algebraic K-theory, Chapter II, Exercise II.9.15, where K₀ of a triangulated category is presented by the distinguished triangles, and Section 6 for the presentation engine consumed here.

noncomputable def TauCeti.triangleRelation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.EssentiallySmall.{w, v, u} C] (T : CategoryTheory.Pretriangulated.Triangle C) : FreeAbelianGroup (ObjectCode C)

The relation [T.obj₂] - [T.obj₁] - [T.obj₃] attached to a triangle. Triangulated K₀ imposes it for every distinguished triangle.

Equations

• TauCeti.triangleRelation T = TauCeti.freeOf T.obj₂ - TauCeti.freeOf T.obj₁ - TauCeti.freeOf T.obj₃

@[simp]

theorem TauCeti.triangleRelation_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.EssentiallySmall.{w, v, u} C] (T : CategoryTheory.Pretriangulated.Triangle C) : triangleRelation T = freeOf T.obj₂ - freeOf T.obj₁ - freeOf T.obj₃

The defining equation of TauCeti.triangleRelation.

theorem TauCeti.map_triangleRelation_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.EssentiallySmall.{w, v, u} C] {G : Type u_1} [AddGroup G] (f : FreeAbelianGroup (ObjectCode C) →+ G) (T : CategoryTheory.Pretriangulated.Triangle C) : f (triangleRelation T) = 0 ↔ f (freeOf T.obj₂) = f (freeOf T.obj₁) + f (freeOf T.obj₃)

An additive homomorphism annihilates the relation of a triangle exactly when it is additive on that triangle. This evaluates a triangle relation once and for all, for both the quotient map presenting triangulated K₀ and the free extension of an invariant.

theorem TauCeti.freeMap_triangleRelation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.EssentiallySmall.{w, v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.HasShift D ℤ] [CategoryTheory.EssentiallySmall.{w', v', u'} D] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] (T : CategoryTheory.Pretriangulated.Triangle C) : (freeMap F) (triangleRelation T) = triangleRelation (F.mapTriangle.obj T)

The free map of a functor commuting with the shift carries the relation of a triangle to the relation of its image.

def TauCeti.triangulatedRelations (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] : Set (FreeAbelianGroup (ObjectCode C))

The family of triangle relations presenting the triangulated K₀ of a pretriangulated category.

Equations

• TauCeti.triangulatedRelations C = {r : FreeAbelianGroup (TauCeti.ObjectCode C) | ∃ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, r = TauCeti.triangleRelation T}

theorem TauCeti.mem_triangulatedRelations_iff {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] {r : FreeAbelianGroup (ObjectCode C)} : r ∈ triangulatedRelations C ↔ ∃ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, r = triangleRelation T

theorem TauCeti.triangleRelation_mem_triangulatedRelations {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] {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : triangleRelation T ∈ triangulatedRelations C

def TauCeti.TriangulatedK0 (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] : Type w

The Grothendieck group of an essentially small pretriangulated category: the free abelian group on the isomorphism classes of objects, modulo [Y] = [X] + [Z] for every distinguished triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧.

Equations

• TauCeti.TriangulatedK0 C = TauCeti.PresentedK0 (TauCeti.triangulatedRelations C)

@[instance_reducible]

instance TauCeti.instAddCommGroupTriangulatedK0 {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] : AddCommGroup (TriangulatedK0 C)

Equations

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

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

The class of an object in triangulated K₀.

Equations

• TauCeti.TriangulatedK0.of X = TauCeti.PresentedK0.of X

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

theorem TauCeti.TriangulatedK0.of_distTriang {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] {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : of T.obj₂ = of T.obj₁ + of T.obj₃

The defining relation of triangulated K₀: the class of the middle term of a distinguished triangle is the sum of the classes of its two outer terms.

theorem TauCeti.TriangulatedK0.of_eq_add_of_distTriang {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] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X} (hT : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : of Y = of X + of Z

The defining relation of triangulated K₀, stated for a triangle presented by its three maps.

theorem TauCeti.TriangulatedK0.of_eq_sub_of_distTriang {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] {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : of T.obj₃ = of T.obj₂ - of T.obj₁

The class of the cone of a distinguished triangle is the difference of the classes of its first two terms.

@[simp]

theorem TauCeti.TriangulatedK0.of_zero {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] : of 0 = 0

The class of the zero object vanishes: it is the third term of the contractible triangle.

@[simp]

theorem TauCeti.TriangulatedK0.of_eq_zero_of_isZero {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] {X : C} (hX : CategoryTheory.Limits.IsZero X) : of X = 0

The class of an object which is zero vanishes.

@[simp]

theorem TauCeti.TriangulatedK0.of_biprod {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] (X Y : C) : of (X ⊞ Y) = of X + of Y

The class of a biproduct is the sum of the classes: the biproduct triangles are distinguished.

theorem TauCeti.TriangulatedK0.of_shift_one {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] (X : C) : of ((CategoryTheory.shiftFunctor C 1).obj X) = -of X

The class of a shift: [X⟦1⟧] = -[X], forced by the distinguished triangle X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧.

@[simp]

theorem TauCeti.TriangulatedK0.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] (n : ℤ) (X : C) : of ((CategoryTheory.shiftFunctor C n).obj X) = ↑n.negOnePow • of X

The class of an iterated shift: [X⟦n⟧] = (-1)ⁿ[X] for every integer n, the sign being Int.negOnePow n.

theorem TauCeti.TriangulatedK0.closure_range_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] : AddSubgroup.closure (Set.range of) = ⊤

The image of the class map generates triangulated K₀.

theorem TauCeti.TriangulatedK0.induction_on {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] {motive : TriangulatedK0 C → Prop} (x : TriangulatedK0 C) (zero : motive 0) (of : ∀ (X : C), motive (of X)) (add : ∀ (a b : TriangulatedK0 C), motive a → motive b → motive (a + b)) (neg : ∀ (a : TriangulatedK0 C), motive a → motive (-a)) : motive x

Induction on the classes of objects of C: no skeleton representative is ever mentioned.

theorem TauCeti.TriangulatedK0.hom_ext {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} [AddMonoid G] {f g : TriangulatedK0 C →+ G} (h : ∀ (X : C), f (of X) = g (of X)) : f = g

Two homomorphisms out of triangulated K₀ agreeing on the classes of objects are equal.

theorem TauCeti.TriangulatedK0.hom_ext_iff {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} [AddMonoid G] {f g : TriangulatedK0 C →+ G} : f = g ↔ ∀ (X : C), f (of X) = g (of X)

theorem TauCeti.TriangulatedK0.surjective_of_forall_of_mem_range {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} [AddGroup G] {f : G →+ TriangulatedK0 C} (h : ∀ (X : C), of X ∈ f.range) : Function.Surjective ⇑f

A homomorphism into triangulated K₀ whose range contains the class of every object is surjective.

structure TauCeti.TriangulatedK0.AdditiveInvariant (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_2) [AddCommGroup G] : Type (max u u_2)

An additive invariant for triangulated K₀: a function on objects of C additive on the distinguished triangles. It is then constant on isomorphism classes (TauCeti.TriangulatedK0.AdditiveInvariant.map_iso). These are exactly the data that factor through TauCeti.TriangulatedK0 C; see TauCeti.TriangulatedK0.liftEquiv.

• obj : C → G

  The value of the invariant on an object.

• map_distTriang ⦃T : CategoryTheory.Pretriangulated.Triangle C⦄ : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → self.obj T.obj₂ = self.obj T.obj₁ + self.obj T.obj₃

  The value on the middle term of a distinguished triangle is the sum of the outer values.

theorem TauCeti.TriangulatedK0.AdditiveInvariant.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_2} {inst✝⁶ : AddCommGroup G} {x y : AdditiveInvariant C G} : x = y ↔ x.obj = y.obj

theorem TauCeti.TriangulatedK0.AdditiveInvariant.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_2} {inst✝⁶ : AddCommGroup G} {x y : AdditiveInvariant C G} (obj : x.obj = y.obj) : x = y

theorem TauCeti.TriangulatedK0.AdditiveInvariant.map_iso {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] (a : AdditiveInvariant C G) ⦃X Y : C⦄ (e : X ≅ Y) : a.obj X = a.obj Y

An additive invariant takes equal values on isomorphic objects. Additivity on distinguished triangles alone forces invariance under isomorphisms of objects, which is the invariance the presentation of triangulated K₀ requires.

noncomputable def TauCeti.TriangulatedK0.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] (a : AdditiveInvariant C G) : TriangulatedK0 C →+ G

The homomorphism out of triangulated K₀ induced by a triangle-additive invariant.

Equations

• TauCeti.TriangulatedK0.lift a = TauCeti.PresentedK0.lift (TauCeti.TriangulatedK0.AdditiveInvariant.toPresented✝ a)

@[simp]

theorem TauCeti.TriangulatedK0.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] (a : AdditiveInvariant C G) (X : C) : (lift a) (of X) = a.obj X

theorem TauCeti.TriangulatedK0.lift_unique {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] (a : AdditiveInvariant C G) (f : TriangulatedK0 C →+ G) (hf : ∀ (X : C), f (of X) = a.obj X) : f = lift a

Any homomorphism agreeing with a triangle-additive invariant on object classes is its induced lift.

noncomputable def TauCeti.TriangulatedK0.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] : AdditiveInvariant C G ≃ (TriangulatedK0 C →+ G)

The universal property of triangulated K₀: triangle-additive invariants with values in G correspond bijectively to additive homomorphisms TriangulatedK0 C →+ G.

Equations

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

@[simp]

theorem TauCeti.TriangulatedK0.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] (a : AdditiveInvariant C G) : liftEquiv a = lift a

@[simp]

theorem TauCeti.TriangulatedK0.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] (f : TriangulatedK0 C →+ G) (X : C) : (liftEquiv.symm f).obj X = f (of X)

noncomputable def TauCeti.TriangulatedK0.map {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : TriangulatedK0 C →+ TriangulatedK0 D

Functoriality of triangulated K₀: a triangulated functor induces a homomorphism of triangulated Grothendieck groups.

Equations

• TauCeti.TriangulatedK0.map F = TauCeti.PresentedK0.map F ⋯

@[simp]

theorem TauCeti.TriangulatedK0.map_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] {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (X : C) : (map F) (of X) = of (F.obj X)

theorem TauCeti.TriangulatedK0.map_unique {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (f : TriangulatedK0 C →+ TriangulatedK0 D) (hf : ∀ (X : C), f (of X) = of (F.obj X)) : f = map F

Any homomorphism sending object classes to the classes of their images is the induced map.

@[simp]

theorem TauCeti.TriangulatedK0.map_id (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] : map (CategoryTheory.Functor.id C) = AddMonoidHom.id (TriangulatedK0 C)

The identity functor induces the identity of triangulated K₀.

@[simp]

theorem TauCeti.TriangulatedK0.map_comp {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] {K : Type u''} [CategoryTheory.Category.{v'', u''} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.HasShift K ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor K n).Additive] [CategoryTheory.Pretriangulated K] [CategoryTheory.EssentiallySmall.{w'', v'', u''} K] (H : CategoryTheory.Functor D K) [H.CommShift ℤ] [H.IsTriangulated] : map (F.comp H) = (map H).comp (map F)

The induced maps of a composite of triangulated functors compose.

theorem TauCeti.TriangulatedK0.map_congr {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] {F' : CategoryTheory.Functor C D} [F'.CommShift ℤ] [F'.IsTriangulated] (h : ∀ (X : C), Nonempty (F.obj X ≅ F'.obj X)) : map F = map F'

Triangulated functors with isomorphic values on every object induce the same map.

noncomputable def TauCeti.TriangulatedK0.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] {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 ≌ D) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] : TriangulatedK0 C ≃+ TriangulatedK0 D

Equivalence invariance of triangulated K₀: an equivalence whose functor is triangulated induces an isomorphism of triangulated Grothendieck groups. The inverse functor inherits a compatible shift and is triangulated (CategoryTheory.Equivalence.commShiftInverse, CategoryTheory.Equivalence.IsTriangulated.mk'), so no data about it is needed.

Equations

• TauCeti.TriangulatedK0.mapEquiv e = TauCeti.PresentedK0.mapEquiv e ⋯ ⋯

@[simp]

theorem TauCeti.TriangulatedK0.mapEquiv_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] {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 ≌ D) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (X : C) : (mapEquiv e) (of X) = of (e.functor.obj X)

@[simp]

theorem TauCeti.TriangulatedK0.mapEquiv_symm_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] {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 ≌ D) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] (Y : D) : (mapEquiv e).symm (of Y) = of (e.inverse.obj Y)

@[simp]

theorem TauCeti.TriangulatedK0.mapEquiv_toAddMonoidHom {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 ≌ D) [e.functor.CommShift ℤ] [e.functor.IsTriangulated] : ↑(mapEquiv e) = map e.functor

The homomorphism underlying equivalence invariance is the map induced by the functor.

theorem TauCeti.TriangulatedK0.of_fullSubcategory_distTriang {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] (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] [CategoryTheory.EssentiallySmall.{w', v, u} P.FullSubcategory] {T : CategoryTheory.Pretriangulated.Triangle C} (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (h₁ : P T.obj₁) (h₂ : P T.obj₂) (h₃ : P T.obj₃) : of { obj := T.obj₂, property := h₂ } = of { obj := T.obj₁, property := h₁ } + of { obj := T.obj₃, property := h₃ }

In triangulated K₀ of a full triangulated subcategory, a distinguished triangle of the ambient category whose three vertices lie in the subcategory gives the defining relation. The triangle need not be one of the subcategory: its connecting morphism is only required to exist in the ambient category.

noncomputable def TauCeti.TriangulatedK0.fromSplit (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] : SplitK0 C →+ TriangulatedK0 C

The canonical comparison from split K₀ to triangulated K₀. It is induced by the class map, which respects the biproduct relations because the biproduct triangles are distinguished.

Equations

• TauCeti.TriangulatedK0.fromSplit C = TauCeti.SplitK0.lift { obj := fun (X : C) => TauCeti.TriangulatedK0.of X, map_iso := ⋯, map_biprod := ⋯ }

@[simp]

theorem TauCeti.TriangulatedK0.fromSplit_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] (X : C) : (fromSplit C) (SplitK0.of X) = of X

theorem TauCeti.TriangulatedK0.fromSplit_unique {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] (f : SplitK0 C →+ TriangulatedK0 C) (hf : ∀ (X : C), f (SplitK0.of X) = of X) : f = fromSplit C

The canonical comparison out of split K₀ is the unique homomorphism preserving the classes of objects.

theorem TauCeti.TriangulatedK0.fromSplit_surjective {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] : Function.Surjective ⇑(fromSplit C)

The canonical comparison out of split K₀ is surjective: the classes of objects generate triangulated K₀, so triangulated K₀ is a quotient of split K₀.

theorem TauCeti.TriangulatedK0.map_comp_fromSplit {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] (F : CategoryTheory.Functor C D) [F.CommShift ℤ] [F.IsTriangulated] : (map F).comp (fromSplit C) = (fromSplit D).comp (SplitK0.map F)

Naturality of the comparison out of split K₀ in a triangulated functor, which is in particular additive and so also acts on split K₀.