10. NumericalStability🔗

10.1. IsFiniteType🔗

A k-linear pretriangulated category \mathcal{T} is of finite type if every Hom space \operatorname{Hom}(E, F) is finite-dimensional over k and, for each pair of objects E, F, only finitely many shifted Hom spaces \operatorname{Hom}(E, F[n]) are nontrivial.

Construction: The typeclass bundles two conditions: a Module.Finite k (E \longrightarrow F) instance for all pairs (E, F), and a Set.Finite witness that the set \{n \in \mathbb{Z} \mid \operatorname{Hom}(E, F[n]) \neq 0\} is finite.

type class

CategoryTheory.Triangulated.IsFiniteType.{w, v, u} (k : Type w)
  [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] : Prop
CategoryTheory.Triangulated.IsFiniteType.{w,
    v, u}
  (k : Type w) [Field k] (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] : Prop

Instance Constructor

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

Methods

finite_dim : ∀ (E F : C), Module.Finite k (E ⟶ F)

Each Hom space Hom(E, F) is finite-dimensional over k.

finite_support : ∀ (E F : C), {n | Nontrivial (E ⟶ (CategoryTheory.shiftFunctor C n).obj F)}.Finite

For each pair of objects, only finitely many shifted Hom spaces are nontrivial.

Something wrong, better idea? Suggest a change

10.2. eulerFormObj🔗

The object-level Euler form is defined by \chi(E, F) = \sum_{n \in \mathbb{Z}} (-1)^n \dim_k \operatorname{Hom}(E, F[n]). It computes the alternating sum of dimensions of shifted Hom spaces between objects of a finite-type triangulated category.

Construction: Defined as a finsum over \mathbb{Z}, weighting each shifted Hom dimension by (-1)^n via Int.negOnePow. The sum is well-defined because IsFiniteType guarantees only finitely many nonzero terms.

def

CategoryTheory.Triangulated.eulerFormObj.{w, v, u} (k : Type w)
  [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] (E F : C) : ℤ
CategoryTheory.Triangulated.eulerFormObj.{w,
    v, u}
  (k : Type w) [Field k] (C : Type u)
  [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.HasShift C ℤ]
  [CategoryTheory.Preadditive C]
  [CategoryTheory.Linear k C] (E F : C) :
  ℤ

Something wrong, better idea? Suggest a change