Bridgeland Stability Conditions

2.1. GrothendieckGroup: Basic🔗

2.1.1. trianglePresentation🔗

The triangle presentation of a pretriangulated category \mathcal{C}: a K0Presentation whose objects are objects of \mathcal{C} and whose relations are distinguished triangles A \to B \to C \to A[1], with \operatorname{obj}_1 = A, \operatorname{obj}_2 = B, \operatorname{obj}_3 = C.

Construction: An abbreviation instantiating K0Presentation C {T : Triangle C // T \in distTriang C} with the three vertex projections.

🔗def
CategoryTheory.Triangulated.trianglePresentation.{v, u} (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [CategoryTheory.Pretriangulated C] :
  K0Presentation C
    { T // T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles }
CategoryTheory.Triangulated.trianglePresentation.{v,
    u}
  (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasZeroObject C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [∀ (n : ℤ),
      (CategoryTheory.shiftFunctor C
          n).Additive]
  [CategoryTheory.Pretriangulated C] :
  K0Presentation C
    { T //
      T ∈
        CategoryTheory.Pretriangulated.distinguishedTriangles }

Something wrong, better idea? Suggest a change

2.1.2. K₀🔗

The Grothendieck group K_0(\mathcal{C}) of a pretriangulated category \mathcal{C}, defined as the quotient of the free abelian group on objects of \mathcal{C} by the relations [B] = [A] + [C] for each distinguished triangle A \to B \to C \to A[1].

Construction: Defined as (trianglePresentation C).K0, the Grothendieck group of the triangle presentation.

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

Something wrong, better idea? Suggest a change

2.1.3. instAddCommGroup🔗

The Grothendieck group K_0(\mathcal{C}) carries a canonical additive commutative group structure inherited from the quotient of the free abelian group.

Proof: Inferred from the AddCommGroup instance on the quotient (trianglePresentation C).K0.

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

Something wrong, better idea? Suggest a change

2.1.4. of🔗

The class map [\cdot] : \mathcal{C} \to K_0(\mathcal{C}) sending an object X to its class [X] in the Grothendieck group.

Construction: Defined as QuotientAddGroup.mk (FreeAbelianGroup.of X) through the triangle presentation.

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

Something wrong, better idea? Suggest a change

2.1.5. trianglePresentation_of🔗

The class map of the triangle presentation agrees with K_0.\operatorname{of}.

Proof: Definitional equality (rfl).

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

Something wrong, better idea? Suggest a change

2.1.6. of_triangle🔗

Additivity on triangles: for a distinguished triangle A \to B \to C \to A[1], one has [B] = [A] + [C] in K_0(\mathcal{C}).

Proof: Immediate from the fundamental relation of_rel of the triangle presentation.

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

Something wrong, better idea? Suggest a change

2.1.7. of_zero🔗

The class of the zero object vanishes in K_0: [0] = 0.

Proof: Apply of_triangle to the contractible triangle 0 \to 0 \to 0 \to 0[1], yielding [0] = [0] + [0], then cancel.

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

Something wrong, better idea? Suggest a change

2.1.8. of_iso🔗

Isomorphic objects have the same class in K_0: if X \cong Y then [X] = [Y].

Proof: Construct a distinguished triangle X \xrightarrow{e} Y \to 0 \to X[1] from the isomorphism e, apply of_triangle, and use of_zero.

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

Something wrong, better idea? Suggest a change

2.1.9. of_isZero🔗

The class of any zero object vanishes: if \operatorname{IsZero}(X) then [X] = 0.

Proof: Transport via the isomorphism to the explicit zero object and apply of_zero.

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

Something wrong, better idea? Suggest a change

2.1.10. of_shift_one🔗

Shifting by [1] negates the class: [X[1]] = -[X] in K_0(\mathcal{C}).

Proof: Rotate the contractible triangle of X to obtain a distinguished triangle X \to 0 \to X[1] \to X[1], apply of_triangle to get 0 = [X] + [X[1]], and rearrange.

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

Something wrong, better idea? Suggest a change

2.1.11. of_shift_neg_one🔗

Shifting by [-1] negates the class: [X[-1]] = -[X] in K_0(\mathcal{C}).

Proof: Apply of_shift_one to X[-1], use the natural isomorphism (X[-1])[1] \cong X, and solve for [X[-1]].

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

Something wrong, better idea? Suggest a change

2.1.12. IsTriangleAdditive🔗

A function f : \mathcal{C} \to A to an additive group is triangle-additive if f(B) = f(A) + f(C) for every distinguished triangle A \to B \to C \to A[1]. This is the universal property hypothesis for lifting through K_0.

Construction: A Prop-valued typeclass with a single field additive quantifying over all distinguished triangles.

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

Instance Constructor

CategoryTheory.Triangulated.IsTriangleAdditive.mk.{v, u, u_1}

Methods

additive : ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, f T.obj₂ = f T.obj₁ + f T.obj₃

Something wrong, better idea? Suggest a change

2.1.13. instIsAdditiveSubtypeTriangleMemSetDistinguishedTrianglesTrianglePresentationOfIsTriangleAdditive🔗

Any triangle-additive function f : \mathcal{C} \to A is additive for the triangle presentation of K_0, i.e., satisfies the K_0-presentation's additivity condition.

Construction: Unwraps the subtype: the K0Presentation.IsAdditive instance for trianglePresentation C is given by IsTriangleAdditive.additive T hT applied to the underlying triangle and membership proof.

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

Something wrong, better idea? Suggest a change

2.1.14. lift🔗

The universal property of K_0(\mathcal{C}): any triangle-additive function f : \mathcal{C} \to A lifts uniquely to a group homomorphism K_0(\mathcal{C}) \to A.

Construction: Defined as (trianglePresentation C).lift f, delegating to the algebraic universal property of the K_0-presentation.

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

Something wrong, better idea? Suggest a change

2.1.15. lift_of🔗

The lift agrees with the original function on generators: \operatorname{lift}(f)([X]) = f(X).

Proof: Immediate from K0Presentation.lift_of.

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

Something wrong, better idea? Suggest a change

2.1.16. hom_ext🔗

Extensionality for K_0(\mathcal{C}): two group homomorphisms from K_0(\mathcal{C}) that agree on all object classes [X] are equal.

Proof: Delegates to K0Presentation.hom_ext.

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

Something wrong, better idea? Suggest a change

2.1.17. hom_ext_iff🔗

Two group homomorphisms f, g : K_0(\mathcal{C}) \to A are equal if and only if they agree on all object classes [X] for X \in \mathcal{C}.

Proof: The forward direction is trivial; the reverse direction is K₀.hom_ext.

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

Something wrong, better idea? Suggest a change

2.1.18. of_postnikovTower_eq_sum🔗

K_0 additivity for Postnikov towers: if P is a Postnikov tower of E with factors F_0, \ldots, F_{n-1}, then [E] = \sum_{i=0}^{n-1} [F_i] in K_0(\mathcal{C}). This is the key algebraic identity used in the sector bound (Lemma 6.2 of Bridgeland).

Proof: Induction on the chain length via the auxiliary lemma of_chain_eq_partial_sum, which telescopes using of_triangle at each step. The base case uses of_isZero on the zero base object, and the top isomorphism identifies the final chain object with E.

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

Something wrong, better idea? Suggest a change

2.1.19. cl🔗

The class of an object E in a target lattice \Lambda, via a group homomorphism v : K_0(\mathcal{C}) \to \Lambda. This is v([E]) in the notation of Bridgeland.

Construction: An abbreviation for v (K_0.of C E), composing the class map with the lattice homomorphism.

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

Something wrong, better idea? Suggest a change

2.1.20. cl_id🔗

When v = \operatorname{id}, the class map reduces to K_0.\operatorname{of}.

Proof: Definitional equality (rfl).

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

Something wrong, better idea? Suggest a change

2.1.21. cl_isZero🔗

The class of a zero object vanishes in the target lattice.

Proof: Follows from [E] = 0 in K_0 (of_isZero) and map_zero.

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

Something wrong, better idea? Suggest a change

2.1.22. cl_triangle🔗

The class map respects distinguished triangles: v([B]) = v([A]) + v([C]).

Proof: Follows from of_triangle and the additivity of v (map_add).

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

Something wrong, better idea? Suggest a change

2.1.23. cl_iso🔗

The class map respects isomorphisms: if X \cong Y then v([X]) = v([Y]).

Proof: Immediate from of_iso.

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

Something wrong, better idea? Suggest a change

2.1.24. cl_shift_one🔗

Shifting by [1] negates the class in the target lattice: v([E[1]]) = -v([E]).

Proof: Follows from of_shift_one and map_neg.

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

Something wrong, better idea? Suggest a change

2.1.25. cl_shift_neg_one🔗

Shifting by [-1] negates the class in the target lattice: v([E[-1]]) = -v([E]).

Proof: Follows from of_shift_neg_one and map_neg.

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

Something wrong, better idea? Suggest a change

2.1.26. cl_postnikovTower_eq_sum🔗

The class of a Postnikov tower total object equals the sum of the classes of the factors in the target lattice: v([E]) = \sum_i v([F_i]).

Proof: Follows from of_postnikovTower_eq_sum and map_sum.

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

Something wrong, better idea? Suggest a change