Realizations of a triangulated Grothendieck group

A realization of K₀ C in an additive commutative group is simply an additive homomorphism. This file gives that canonical hom type a semantic abbreviation and records when a triangulated functor descends through two realizations.

Nothing here is numerical or geometric: a numerical Grothendieck group, a cohomological realization, or any other additive target is a consumer of the same root.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.K₀.Realization (C : Type u₁) [Category.{v₁, u₁} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (A : Type x₁) [AddCommGroup A] : Type (max u₁ x₁)

A realization of the triangulated Grothendieck group in an additive commutative group. This is an abbreviation, not a parallel one-field carrier.

Equations

• CategoryTheory.Triangulated.K₀.Realization C A = (CategoryTheory.Triangulated.K₀ C →+ A)

def CategoryTheory.Triangulated.K₀.Realization.Descends {C : Type u₁} {D : Type u₂} {A : Type x₁} {B : Type x₂} [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] [AddCommGroup A] [AddCommGroup B] (R : Realization C A) (R' : Realization D B) (F : Functor C D) [F.CommShift ℤ] [F.IsTriangulated] (f : A →+ B) : Prop

F descends to f along two realizations when the square formed by K₀.map F, the realizations, and f commutes.

Equations

• R.Descends R' F f = ∀ (x : CategoryTheory.Triangulated.K₀ C), R' ((CategoryTheory.Triangulated.K₀.map F) x) = f (R x)

theorem CategoryTheory.Triangulated.K₀.Realization.Descends.apply_of {C : Type u₁} {D : Type u₂} {A : Type x₁} {B : Type x₂} [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] [AddCommGroup A] [AddCommGroup B] {R : Realization C A} {R' : Realization D B} {F : Functor C D} [F.CommShift ℤ] [F.IsTriangulated] {f : A →+ B} (h : R.Descends R' F f) (X : C) : R' (of D (F.obj X)) = f (R (of C X))

A descent is determined on classes of objects.

theorem CategoryTheory.Triangulated.K₀.Realization.Descends.of_natIso {C : Type u₁} {D : Type u₂} {A : Type x₁} {B : Type x₂} [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] [AddCommGroup A] [AddCommGroup B] {R : Realization C A} {R' : Realization D B} {F G : Functor C D} [F.CommShift ℤ] [F.IsTriangulated] [G.CommShift ℤ] [G.IsTriangulated] {f : A →+ B} (h : R.Descends R' F f) (e : F ≅ G) : R.Descends R' G f

Naturally isomorphic triangulated functors have the same descents.