Functoriality of the triangulated Grothendieck group

Triangulated functors induce homomorphisms on the repository-owned Grothendieck group. Naturally isomorphic functors induce equal homomorphisms.

instance CategoryTheory.Triangulated.K₀.isTriangleAdditive_map {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] : IsTriangleAdditive fun (X : C) => of D (F.obj X)

Object classes transported by a triangulated functor are triangle-additive.

def CategoryTheory.Triangulated.K₀.map {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] : K₀ C →+ K₀ D

The homomorphism on Grothendieck groups induced by a triangulated functor.

Equations

• CategoryTheory.Triangulated.K₀.map F = CategoryTheory.Triangulated.K₀.lift C fun (X : C) => CategoryTheory.Triangulated.K₀.of D (F.obj X)

@[simp]

theorem CategoryTheory.Triangulated.K₀.map_of {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) [F.Additive] [F.CommShift ℤ] [F.IsTriangulated] (X : C) : (map F) (of C X) = of D (F.obj X)

@[simp]

theorem CategoryTheory.Triangulated.K₀.map_id {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : map (Functor.id C) = AddMonoidHom.id (K₀ C)

@[simp]

theorem CategoryTheory.Triangulated.K₀.map_comp {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) {E : Type u_1} [Category.{u_2, u_1} E] [Limits.HasZeroObject E] [HasShift E ℤ] [Preadditive E] [∀ (n : ℤ), (shiftFunctor E n).Additive] [Pretriangulated E] (G : Functor D E) [F.Additive] [G.Additive] [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] : map (F.comp G) = (map G).comp (map F)

theorem CategoryTheory.Triangulated.K₀.map_congr {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] {F G : Functor C D} [F.Additive] [G.Additive] [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] (e : F ≅ G) : map F = map G

Naturally isomorphic triangulated functors induce the same map on Grothendieck groups.

theorem CategoryTheory.Triangulated.K₀.map_comp_map_eq_id {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (G : Functor D C) [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] (e : F.comp G ≅ Functor.id C) : (map G).comp (map F) = AddMonoidHom.id (K₀ C)

A one-sided inverse of triangulated functors gives a one-sided inverse on Grothendieck groups.

def CategoryTheory.Triangulated.K₀.mapAddEquiv {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (G : Functor D C) [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] (e : F.comp G ≅ Functor.id C) (e' : G.comp F ≅ Functor.id D) : K₀ C ≃+ K₀ D

An exact equivalence induces an isomorphism on K₀.

Stated from the two unit/counit isomorphisms rather than from Equivalence, so that a caller who has a quasi-inverse triangulated functor in hand does not first have to package it.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.K₀.mapAddEquiv_apply {C : Type u} {D : Type u'} [Category.{v, u} C] [Category.{v', u'} D] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Limits.HasZeroObject D] [HasShift D ℤ] [Preadditive D] [∀ (n : ℤ), (shiftFunctor D n).Additive] [Pretriangulated D] (F : Functor C D) (G : Functor D C) [F.CommShift ℤ] [G.CommShift ℤ] [F.IsTriangulated] [G.IsTriangulated] (e : F.comp G ≅ Functor.id C) (e' : G.comp F ≅ Functor.id D) (x : K₀ C) : (mapAddEquiv F G e e') x = (map F) x