Bridgeland Stability Conditions

3. EulerForm🔗

3.1. finrank_mid_of_exact🔗

For a middle-exact sequence K \xrightarrow{f} M \xrightarrow{g} N of finite-dimensional k-vector spaces (i.e., \operatorname{im} f = \ker g), we have \dim M = \dim(\operatorname{im} f) + \dim(\operatorname{im} g).

Proof: Apply rank-nullity to g (giving \dim M = \dim(\ker g) + \dim(\operatorname{im} g)) and substitute \ker g = \operatorname{im} f.

🔗theorem
CategoryTheory.Triangulated.finrank_mid_of_exact.{w, v} (k : Type w)
  [Field k] {K M N : Type v} [AddCommGroup K] [Module k K]
  [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N]
  [Module.Finite k M] (f : K →ₗ[k] M) (g : M →ₗ[k] N)
  (hfg : f.range = g.ker) :
  ↑(Module.finrank k M) =
    ↑(Module.finrank k ↥f.range) + ↑(Module.finrank k ↥g.range)
CategoryTheory.Triangulated.finrank_mid_of_exact.{w,
    v}
  (k : Type w) [Field k] {K M N : Type v}
  [AddCommGroup K] [Module k K]
  [AddCommGroup M] [Module k M]
  [AddCommGroup N] [Module k N]
  [Module.Finite k M] (f : K →ₗ[k] M)
  (g : M →ₗ[k] N)
  (hfg : f.range = g.ker) :
  ↑(Module.finrank k M) =
    ↑(Module.finrank k ↥f.range) +
      ↑(Module.finrank k ↥g.range)

Something wrong, better idea? Suggest a change

3.2. finsum_alternating_shift_cancel🔗

The sum \sum_{n \in \mathbb{Z}} (-1)^n r(n-1) + \sum_{n \in \mathbb{Z}} (-1)^n r(n) = 0 for any finitely-supported integer sequence r.

Proof: Shift the index in the first sum (n \mapsto n+1) to get \sum_m (-1)^{m+1} r(m); since (-1)^{m+1} = -(-1)^m, the two sums cancel.

🔗theorem
CategoryTheory.Triangulated.finsum_alternating_shift_cancel
  {r : ℤ → ℤ} :
  ∑ᶠ (n : ℤ), ↑n.negOnePow * r (n - 1) +
      ∑ᶠ (n : ℤ), ↑n.negOnePow * r n =
    0
CategoryTheory.Triangulated.finsum_alternating_shift_cancel
  {r : ℤ → ℤ} :
  ∑ᶠ (n : ℤ), ↑n.negOnePow * r (n - 1) +
      ∑ᶠ (n : ℤ), ↑n.negOnePow * r n =
    0

Something wrong, better idea? Suggest a change

3.3. eulerSum_of_rank_identity🔗

If the Hom-space dimensions satisfy \dim(E \to b_n) = \dim(E \to a_n) + \dim(E \to c_n) - r_{n-1} - r_n for a finitely-supported correction r, then the alternating Euler sums satisfy \sum_n (-1)^n \dim(E \to b_n) = \sum_n (-1)^n \dim(E \to a_n) + \sum_n (-1)^n \dim(E \to c_n).

Proof: The correction terms (-1)^n r_{n-1} and (-1)^n r_n cancel by finsum_alternating_shift_cancel.

🔗theorem
CategoryTheory.Triangulated.eulerSum_of_rank_identity.{w, v, u}
  (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (E : C)
  {a b c : ℤ → C} {r : ℤ → ℤ}
  (hrank :
    ∀ (n : ℤ),
      ↑(Module.finrank k (E ⟶ b n)) =
        ↑(Module.finrank k (E ⟶ a n)) + ↑(Module.finrank k (E ⟶ c n)) -
            r (n - 1) -
          r n)
  (hfin_a : {n | Nontrivial (E ⟶ a n)}.Finite)
  (hfin_b : {n | Nontrivial (E ⟶ b n)}.Finite)
  (hfin_c : {n | Nontrivial (E ⟶ c n)}.Finite)
  (hr : (Function.support r).Finite) :
  ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ b n)) =
    ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ a n)) +
      ∑ᶠ (n : ℤ), ↑n.negOnePow * ↑(Module.finrank k (E ⟶ c n))
CategoryTheory.Triangulated.eulerSum_of_rank_identity.{w,
    v, u}
  (k : Type w) [Field k] (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] (E : C)
  {a b c : ℤ → C} {r : ℤ → ℤ}
  (hrank :
    ∀ (n : ℤ),
      ↑(Module.finrank k (E ⟶ b n)) =
        ↑(Module.finrank k (E ⟶ a n)) +
              ↑(Module.finrank k
                  (E ⟶ c n)) -
            r (n - 1) -
          r n)
  (hfin_a :
    {n | Nontrivial (E ⟶ a n)}.Finite)
  (hfin_b :
    {n | Nontrivial (E ⟶ b n)}.Finite)
  (hfin_c :
    {n | Nontrivial (E ⟶ c n)}.Finite)
  (hr : (Function.support r).Finite) :
  ∑ᶠ (n : ℤ),
      ↑n.negOnePow *
        ↑(Module.finrank k (E ⟶ b n)) =
    ∑ᶠ (n : ℤ),
        ↑n.negOnePow *
          ↑(Module.finrank k (E ⟶ a n)) +
      ∑ᶠ (n : ℤ),
        ↑n.negOnePow *
          ↑(Module.finrank k (E ⟶ c n))

Something wrong, better idea? Suggest a change

3.4. eulerSum_of_rank_identity_int🔗

An integer-valued version of eulerSum_of_rank_identity: if integer sequences a, b, c, r satisfy b(n) = a(n) + c(n) - r(n-1) - r(n) with a, c, r finitely supported, then \sum_n (-1)^n b(n) = \sum_n (-1)^n a(n) + \sum_n (-1)^n c(n).

Proof: Same telescoping cancellation as eulerSum_of_rank_identity, applied to abstract integer sequences rather than Hom-space dimensions.

🔗theorem
CategoryTheory.Triangulated.eulerSum_of_rank_identity_int
  {a b c r : ℤ → ℤ}
  (hrank : ∀ (n : ℤ), b n = a n + c n - r (n - 1) - r n)
  (hfa : (Function.support a).Finite)
  (hfc : (Function.support c).Finite)
  (hr : (Function.support r).Finite) :
  ∑ᶠ (n : ℤ), ↑n.negOnePow * b n =
    ∑ᶠ (n : ℤ), ↑n.negOnePow * a n + ∑ᶠ (n : ℤ), ↑n.negOnePow * c n
CategoryTheory.Triangulated.eulerSum_of_rank_identity_int
  {a b c r : ℤ → ℤ}
  (hrank :
    ∀ (n : ℤ),
      b n = a n + c n - r (n - 1) - r n)
  (hfa : (Function.support a).Finite)
  (hfc : (Function.support c).Finite)
  (hr : (Function.support r).Finite) :
  ∑ᶠ (n : ℤ), ↑n.negOnePow * b n =
    ∑ᶠ (n : ℤ), ↑n.negOnePow * a n +
      ∑ᶠ (n : ℤ), ↑n.negOnePow * c n

Something wrong, better idea? Suggest a change

3.5. linearRange_eq_linearKer_of_ab_exact🔗

If a composable pair f : A \to B, g : B \to C in a k-linear category satisfies f \circ g = 0 and abelian-group exactness at \operatorname{Hom}(E, B), then \operatorname{im}(f \circ -) = \ker(g \circ -) as k-linear subspaces.

Proof: Straightforward from the exactness hypothesis.

🔗theorem
CategoryTheory.Triangulated.linearRange_eq_linearKer_of_ab_exact.{w, v,
    u}
  (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C]
  {A B C' : C} (E : C) (f : A ⟶ B) (g : B ⟶ C')
  (hfg : CategoryTheory.CategoryStruct.comp f g = 0)
  (hexact :
    ∀ (x : E ⟶ B),
      CategoryTheory.CategoryStruct.comp x g = 0 →
        ∃ y, CategoryTheory.CategoryStruct.comp y f = x) :
  (CategoryTheory.Linear.rightComp k E f).range =
    (CategoryTheory.Linear.rightComp k E g).ker
CategoryTheory.Triangulated.linearRange_eq_linearKer_of_ab_exact.{w,
    v, u}
  (k : Type w) [Field k] (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] {A B C' : C}
  (E : C) (f : A ⟶ B) (g : B ⟶ C')
  (hfg :
    CategoryTheory.CategoryStruct.comp f
        g =
      0)
  (hexact :
    ∀ (x : E ⟶ B),
      CategoryTheory.CategoryStruct.comp x
            g =
          0 →
        ∃ y,
          CategoryTheory.CategoryStruct.comp
              y f =
            x) :
  (CategoryTheory.Linear.rightComp k E
        f).range =
    (CategoryTheory.Linear.rightComp k E
        g).ker

Something wrong, better idea? Suggest a change

3.6. linearMap_range_eq_ker_of_addMonoidHom🔗

If two k-linear maps f : V \to W and g : W \to X satisfy \operatorname{im}(f^{\mathrm{AbGrp}}) = \ker(g^{\mathrm{AbGrp}}) as subgroups, then \operatorname{im} f = \ker g as k-submodules.

Proof: Directly from the pointwise equivalence between module membership and group membership.

🔗theorem
CategoryTheory.Triangulated.linearMap_range_eq_ker_of_addMonoidHom.{w,
    v}
  (k : Type w) [Field k] {V W X : Type v} [AddCommGroup V] [Module k V]
  [AddCommGroup W] [Module k W] [AddCommGroup X] [Module k X]
  (f : V →ₗ[k] W) (g : W →ₗ[k] X)
  (h : f.toAddMonoidHom.range = g.toAddMonoidHom.ker) : f.range = g.ker
CategoryTheory.Triangulated.linearMap_range_eq_ker_of_addMonoidHom.{w,
    v}
  (k : Type w) [Field k] {V W X : Type v}
  [AddCommGroup V] [Module k V]
  [AddCommGroup W] [Module k W]
  [AddCommGroup X] [Module k X]
  (f : V →ₗ[k] W) (g : W →ₗ[k] X)
  (h :
    f.toAddMonoidHom.range =
      g.toAddMonoidHom.ker) :
  f.range = g.ker

Something wrong, better idea? Suggest a change

3.7. linearCoyonedaObjIsHomological🔗

For any object E in a k-linear triangulated category, the k-linear Yoneda functor \operatorname{Hom}(E, -) (viewed as a functor to k-modules) is homological, i.e., it sends distinguished triangles to long exact sequences.

Construction: Reduced to exactness of the preadditive Yoneda functor via preadditiveYoneda.map_distinguished_exact and ShortComplex.exact_iff_exact_map_forget₂.

🔗theorem
CategoryTheory.Triangulated.linearCoyonedaObjIsHomological.{w, v, u}
  (k : Type w) [Field k] (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.Linear k C]
  (E : C) :
  ((CategoryTheory.linearCoyoneda k C).obj
      (Opposite.op E)).IsHomological
CategoryTheory.Triangulated.linearCoyonedaObjIsHomological.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C] (E : C) :
  ((CategoryTheory.linearCoyoneda k C).obj
      (Opposite.op E)).IsHomological

Something wrong, better idea? Suggest a change

3.8. eulerFormObj_contravariant_triangleAdditive🔗

The contravariant Euler form F \mapsto \chi(E, F) is additive on distinguished triangles: if A \to B \to C \to A[1] is distinguished, then \chi(E, A) - \chi(E, B) + \chi(E, C) = 0.

Proof: Follows from the long exact sequence of Hom spaces induced by the distinguished triangle and the alternating-sum telescoping that results from rank-nullity applied to each connecting map.

🔗theorem
CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C] (E : C) :
  CategoryTheory.Triangulated.IsTriangleAdditive fun F =>
    CategoryTheory.Triangulated.eulerFormObj k C E F
CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  (E : C) :
  CategoryTheory.Triangulated.IsTriangleAdditive
    fun F =>
    CategoryTheory.Triangulated.eulerFormObj
      k C E F

Something wrong, better idea? Suggest a change

3.9. eulerFormObj_covariant_triangleAdditive🔗

For fixed F, the function E \mapsto \chi(E, F) = \sum_n (-1)^n \dim_k \operatorname{Hom}(E, F[n]) is triangle-additive: for any distinguished triangle A \to B \to C \to A[1] one has \chi(B, F) = \chi(A, F) + \chi(C, F).

Proof: Apply the long exact sequence in \operatorname{Hom}(-, F[n]) from the preadditiveYoneda functor, extract rank-nullity data for each degree, and use eulerSum_of_rank_identity_int to telescope the alternating sum.

🔗theorem
CategoryTheory.Triangulated.eulerFormObj_covariant_triangleAdditive.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C] (F : C)
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.IsTriangleAdditive fun E =>
    CategoryTheory.Triangulated.eulerFormObj k C E F
CategoryTheory.Triangulated.eulerFormObj_covariant_triangleAdditive.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  (F : C)
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.IsTriangleAdditive
    fun E =>
    CategoryTheory.Triangulated.eulerFormObj
      k C E F

Something wrong, better idea? Suggest a change

3.10. eulerFormInner🔗

The Euler form \chi(E, F) = \sum_{n} (-1)^n \dim_k \operatorname{Hom}(E, F[n]) is the signed alternating sum of dimensions of shifted Hom spaces. It defines a bilinear pairing on objects of a numerically finite triangulated category.

Construction: Defined as the integer-valued function that sums (-1)^n * finrank k Hom(E, F[n]) over the finitely many nonzero shifts, using the NumericallyFinite hypothesis to ensure the sum is well-defined.

🔗def
CategoryTheory.Triangulated.eulerFormInner.{w, v, u} (k : Type w)
  [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C] (E : C) :
  CategoryTheory.Triangulated.K₀ C →+ ℤ
CategoryTheory.Triangulated.eulerFormInner.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  (E : C) :
  CategoryTheory.Triangulated.K₀ C →+ ℤ

Something wrong, better idea? Suggest a change

3.11. eulerFormInner_isTriangleAdditive🔗

The assignment E \mapsto \chi(E, -) (as a group homomorphism K_0 \to \mathbb{Z}) is triangle-additive in E, so the Euler form descends to a bilinear form on K_0.

🔗theorem
CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive.{w, v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.IsTriangleAdditive
    (CategoryTheory.Triangulated.eulerFormInner k C)
CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.IsTriangleAdditive
    (CategoryTheory.Triangulated.eulerFormInner
      k C)

Something wrong, better idea? Suggest a change

3.12. eulerForm🔗

The Euler form \chi : K_0(\mathcal{C}) \times K_0(\mathcal{C}) \to \mathbb{Z}, obtained by applying the universal property of K_0 twice to the function (E, F) \mapsto \sum_n (-1)^n \dim_k \operatorname{Hom}(E, F[n]).

Construction: Defined by lifting eulerFormInner k C (which is itself the lift of the contravariant Euler form) along K_0 via K₀.lift.

🔗def
CategoryTheory.Triangulated.eulerForm.{w, v, u} (k : Type w) [Field k]
  (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.K₀ C →+ ℤ
CategoryTheory.Triangulated.eulerForm.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.K₀ C →+ ℤ

Something wrong, better idea? Suggest a change

3.13. eulerFormRad🔗

The left radical of the Euler form: the additive subgroup of K_0(\mathcal{C}) consisting of classes e such that \chi(e, f) = 0 for all f \in K_0(\mathcal{C}).

Construction: Defined as the kernel of the group homomorphism eulerForm k C : K₀ C →+ K₀ C →+ ℤ.

🔗def
CategoryTheory.Triangulated.eulerFormRad.{w, v, u} (k : Type w)
  [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  AddSubgroup (CategoryTheory.Triangulated.K₀ C)
CategoryTheory.Triangulated.eulerFormRad.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  AddSubgroup
    (CategoryTheory.Triangulated.K₀ C)

Something wrong, better idea? Suggest a change

3.14. NumericalK₀🔗

The numerical Grothendieck group N(\mathcal{C}), defined as the quotient K_0(\mathcal{C}) / \operatorname{rad}(\chi) where \operatorname{rad}(\chi) is the left radical of the Euler form \chi(E,F) = \sum_i (-1)^i \dim_k \operatorname{Ext}^i(E,F).

Construction: The quotient of K_0(\mathcal{C}) by the kernel of the map e \mapsto (f \mapsto \chi(e, f)), i.e., by eulerFormRad.

🔗def
CategoryTheory.Triangulated.NumericalK₀.{w, v, u} (k : Type w) [Field k]
  (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  Type u
CategoryTheory.Triangulated.NumericalK₀.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  Type u

Something wrong, better idea? Suggest a change

3.15. instAddCommGroup🔗

The numerical Grothendieck group N(\mathcal{C}) inherits an abelian group structure from the quotient K_0(\mathcal{C}) / \operatorname{rad}(\chi).

Construction: Derived by inferInstanceAs from the AddCommGroup instance on a quotient of an abelian group.

🔗def
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup.{w, v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  AddCommGroup (CategoryTheory.Triangulated.NumericalK₀ k C)
CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  AddCommGroup
    (CategoryTheory.Triangulated.NumericalK₀
      k C)

Something wrong, better idea? Suggest a change

3.16. numericalQuotientMap🔗

The canonical surjection K_0(\mathcal{C}) \twoheadrightarrow N(\mathcal{C}) sending each class [E] to its image in the numerical Grothendieck group N(\mathcal{C}) = K_0 / \operatorname{rad}(\chi).

Construction: The quotient map QuotientAddGroup.mk' (eulerFormRad k C).

🔗def
CategoryTheory.Triangulated.numericalQuotientMap.{w, v, u} (k : Type w)
  [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.NumericalK₀ k C
CategoryTheory.Triangulated.numericalQuotientMap.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  CategoryTheory.Triangulated.K₀ C →+
    CategoryTheory.Triangulated.NumericalK₀
      k C

Something wrong, better idea? Suggest a change

3.17. NumericallyFinite🔗

A k-linear triangulated category \mathcal{T} is numerically finite if for all objects E, F \in \mathcal{T}, the graded vector space \bigoplus_n \operatorname{Hom}(E, F[n]) is finite-dimensional over k.

Construction: The typeclass packages the finiteness hypothesis as a Module.Finite instance on the direct sum of shifted Hom spaces, parameterized by the base field and the shift functor.

🔗type class
CategoryTheory.Triangulated.NumericallyFinite.{w, v, u} (k : Type w)
  [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  Prop
CategoryTheory.Triangulated.NumericallyFinite.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  Prop

Instance Constructor

CategoryTheory.Triangulated.NumericallyFinite.mk.{w, v, u}

Methods

fg : AddGroup.FG (CategoryTheory.Triangulated.NumericalK₀ k C)

The Euler-form numerical Grothendieck group is finitely generated.

Something wrong, better idea? Suggest a change

3.18. instFGNumericalK₀OfNumericallyFinite🔗

If \mathcal{C} is numerically finite, the numerical Grothendieck group N(\mathcal{C}) is a finitely generated abelian group.

Construction: Synthesized from NumericallyFinite.fg.

🔗theorem
CategoryTheory.Triangulated.instFGNumericalK₀OfNumericallyFinite.{w, v,
    u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)]
  [CategoryTheory.Triangulated.NumericallyFinite k C] :
  AddGroup.FG (CategoryTheory.Triangulated.NumericalK₀ k C)
CategoryTheory.Triangulated.instFGNumericalK₀OfNumericallyFinite.{w,
    v, u}
  (k : Type w) [Field k] (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.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)]
  [CategoryTheory.Triangulated.NumericallyFinite
      k C] :
  AddGroup.FG
    (CategoryTheory.Triangulated.NumericalK₀
      k C)

Something wrong, better idea? Suggest a change

3.19. NumericalStabilityCondition🔗

A numerical stability condition on \mathcal{C}: a stability condition whose central charge Z : K_0(\mathcal{C}) \to \mathbb{C} factors through the numerical quotient N(\mathcal{C}) = K_0(\mathcal{C}) / \operatorname{rad}(\chi).

Construction: An abbreviation for StabilityCondition.WithClassMap C (numericalQuotientMap k C), packaging the requirement that the central charge respects the Euler-form radical.

🔗def
CategoryTheory.Triangulated.NumericalStabilityCondition.{w, v, u}
  (k : Type w) [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  Type u
CategoryTheory.Triangulated.NumericalStabilityCondition.{w,
    v, u}
  (k : Type w) [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  Type u

Something wrong, better idea? Suggest a change

3.20. CentralChargeIsLocalHomeomorphOnConnectedComponents🔗

The proposition that on each connected component of \operatorname{Stab}_N(\mathcal{C}), the map sending a numerical stability condition to its central charge Z : N(\mathcal{C}) \to \mathbb{C} is a local homeomorphism. This is the content of Bridgeland's Corollary 1.3.

Construction: An abbreviation for StabilityCondition.WithClassMap.CentralChargeIsLocalHomeomorphOnConnectedComponents instantiated to the numerical quotient N(\mathcal{C}).

🔗def
CategoryTheory.Triangulated.NumericalStabilityCondition.CentralChargeIsLocalHomeomorphOnConnectedComponents.{w,
    v, u}
  (k : Type w) [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)] :
  Prop
CategoryTheory.Triangulated.NumericalStabilityCondition.CentralChargeIsLocalHomeomorphOnConnectedComponents.{w,
    v, u}
  (k : Type w) [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)] :
  Prop

Something wrong, better idea? Suggest a change

3.21. NumericalComponent🔗

A connected component of the space of numerical stability conditions, i.e., a connected component of \operatorname{Stab}_N(\mathcal{C}) where the central charge factors through N(\mathcal{C}) = K_0 / \operatorname{rad}(\chi).

Construction: An abbreviation for the component type of StabilityCondition.WithClassMap indexed by a component index, instantiated to the numerical quotient map K_0(\mathcal{C}) \to N(\mathcal{C}).

🔗def
CategoryTheory.Triangulated.NumericalComponent.{w, v, u} (k : Type w)
  [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType k C]
  [CategoryTheory.Functor.Linear k (CategoryTheory.shiftFunctor C 1)]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C (CategoryTheory.Triangulated.numericalQuotientMap k C)) :
  Type u
CategoryTheory.Triangulated.NumericalComponent.{w,
    v, u}
  (k : Type w) [Field k] (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.IsTriangulated C]
  [CategoryTheory.Linear k C]
  [CategoryTheory.Triangulated.IsFiniteType
      k C]
  [CategoryTheory.Functor.Linear k
      (CategoryTheory.shiftFunctor C 1)]
  (cc :
    CategoryTheory.Triangulated.StabilityCondition.WithClassMap.ComponentIndex
      C
      (CategoryTheory.Triangulated.numericalQuotientMap
        k C)) :
  Type u

Something wrong, better idea? Suggest a change