The Grothendieck group of a pretriangulated category #

The owner-controlled K₀ C is the free abelian group on objects of C, quotiented by the relations [B] = [A] + [D] for distinguished triangles A ⟶ B ⟶ D ⟶ A⟦1⟧.

source

@[reducible, inline]

abbrev CategoryTheory.Triangulated.triangulatedPresentation (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :

GrothendieckPresentation C { T : Pretriangulated.Triangle C // T ∈ Pretriangulated.distinguishedTriangles }

The Grothendieck presentation associated to distinguished triangles.

Equations

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

Instances For

source

@[reducible, inline]

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

Type u

The Grothendieck group of a pretriangulated category.

Equations

CategoryTheory.Triangulated.K₀ C = (CategoryTheory.Triangulated.triangulatedPresentation C).Group

Instances For

source

def CategoryTheory.Triangulated.K₀.of (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : C) :

K₀ C

The class of an object in the Grothendieck group.

Equations

CategoryTheory.Triangulated.K₀.of C X = (CategoryTheory.Triangulated.triangulatedPresentation C).of X

Instances For

source

theorem CategoryTheory.Triangulated.K₀.of_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) :

of C T.obj₂ = of C T.obj₁ + of C T.obj₃

A distinguished triangle gives the relation [B] = [A] + [D].

source

@[simp]

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

of C 0 = 0

The class of the chosen zero object vanishes.

source

theorem CategoryTheory.Triangulated.K₀.of_iso (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X Y : C} (e : X ≅ Y) :

of C X = of C Y

Isomorphic objects have equal Grothendieck classes.

source

@[simp]

theorem CategoryTheory.Triangulated.K₀.of_isZero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {X : C} (hX : Limits.IsZero X) :

of C X = 0

Every zero object has zero Grothendieck class.

source

@[simp]

theorem CategoryTheory.Triangulated.K₀.of_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : C) :

of C ((shiftFunctor C 1).obj X) = -of C X

Shifting by one negates the Grothendieck class.

source

@[simp]

theorem CategoryTheory.Triangulated.K₀.of_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : C) :

of C ((shiftFunctor C (-1)).obj X) = -of C X

Shifting by minus one negates the Grothendieck class.

source

theorem CategoryTheory.Triangulated.K₀.of_shift_int (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (X : C) (n : ℤ) :

of C ((shiftFunctor C n).obj X) = (-1) ^ n.natAbs • of C X

An integral shift changes a Grothendieck class only by its parity sign.

source

class CategoryTheory.Triangulated.IsTriangleAdditive {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] (f : C → A) :

Prop

A function on objects is triangle-additive when it respects every distinguished-triangle relation.

additive (T : Pretriangulated.Triangle C) : T ∈ Pretriangulated.distinguishedTriangles → f T.obj₂ = f T.obj₁ + f T.obj₃

Instances

source

instance CategoryTheory.Triangulated.instIsAdditiveSubtypeTriangleMemSetDistinguishedTrianglesTriangulatedPresentationOfIsTriangleAdditive {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] (f : C → A) [IsTriangleAdditive f] :

(triangulatedPresentation C).IsAdditive f

source

def CategoryTheory.Triangulated.K₀.lift (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] (f : C → A) [IsTriangleAdditive f] :

K₀ C →+ A

Universal lift of a triangle-additive function.

Equations

CategoryTheory.Triangulated.K₀.lift C f = (CategoryTheory.Triangulated.triangulatedPresentation C).lift f

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.K₀.lift_of (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] (f : C → A) [IsTriangleAdditive f] (X : C) :

(lift C f) (of C X) = f X

source

theorem CategoryTheory.Triangulated.K₀.hom_ext (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] {f g : K₀ C →+ A} (h : ∀ (X : C), f (of C X) = g (of C X)) :

f = g

Additive maps from K₀ C are determined by object classes.

source

theorem CategoryTheory.Triangulated.K₀.hom_ext_iff {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {A : Type u_1} [AddCommGroup A] {f g : K₀ C →+ A} :

f = g ↔ ∀ (X : C), f (of C X) = g (of C X)

source

theorem CategoryTheory.Triangulated.K₀.of_postnikovTower_eq_sum (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {E : C} (P : PostnikovTower C E) :

of C E = ∑ i : Fin P.n, of C (P.factor i)

The class of the filtered object is the sum of the classes of the Postnikov factors.

source

@[reducible, inline]

abbrev CategoryTheory.Triangulated.classOf (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (E : C) :

The class of an object in a target lattice.

Equations

CategoryTheory.Triangulated.classOf C v E = v (CategoryTheory.Triangulated.K₀.of C E)

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.classOf_id (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (E : C) :

classOf C (AddMonoidHom.id (K₀ C)) E = K₀.of C E

source

@[simp]

theorem CategoryTheory.Triangulated.classOf_isZero (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) {E : C} (hE : Limits.IsZero E) :

classOf C v E = 0

source

theorem CategoryTheory.Triangulated.classOf_triangle (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (T : Pretriangulated.Triangle C) (hT : T ∈ Pretriangulated.distinguishedTriangles) :

classOf C v T.obj₂ = classOf C v T.obj₁ + classOf C v T.obj₃

source

theorem CategoryTheory.Triangulated.classOf_iso (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) {X Y : C} (e : X ≅ Y) :

classOf C v X = classOf C v Y

source

@[simp]

theorem CategoryTheory.Triangulated.classOf_shift_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (E : C) :

classOf C v ((shiftFunctor C 1).obj E) = -classOf C v E

source

@[simp]

theorem CategoryTheory.Triangulated.classOf_shift_neg_one (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) (E : C) :

classOf C v ((shiftFunctor C (-1)).obj E) = -classOf C v E

source

theorem CategoryTheory.Triangulated.classOf_postnikovTower_eq_sum (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] {Λ : Type u'} [AddCommGroup Λ] (v : K₀ C →+ Λ) {E : C} (P : PostnikovTower C E) :

classOf C v E = ∑ i : Fin P.n, classOf C v (P.factor i)

Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.GrothendieckGroup.Basic

The Grothendieck group of a pretriangulated category #