4. NumericalStability.Defs
Module BridgelandStability.NumericalStability.Defs — 2 declarations (Structure, Definition)
4.1. CategoryTheory.Triangulated.IsFiniteType
Structure | BridgelandStability.NumericalStability.Defs | Source | Open Issue
/-- A `k`-linear pretriangulated category is of finite type if all Hom spaces are
finite-dimensional over `k` and for each pair of objects, only finitely many shifted
Hom spaces are nonzero. -/
class IsFiniteType [Linear k C] : Prop where
/-- Each Hom space `Hom(E, F)` is finite-dimensional over `k`. -/
finite_dim : ∀ (E F : C), Module.Finite k (E ⟶ F)
/-- For each pair of objects, only finitely many shifted Hom spaces are nontrivial. -/
finite_support : ∀ (E F : C), Set.Finite {n : ℤ | Nontrivial (E ⟶ (shiftFunctor C n).obj F)}
4.2. CategoryTheory.Triangulated.eulerFormObj
Definition | BridgelandStability.NumericalStability.Defs | Source | Open Issue
/-- The Euler form on objects: `χ(E,F) = Σₙ (-1)ⁿ dim_k Hom(E, F[n])`.
This is defined as a finitely-supported sum using `finsum`. -/
def eulerFormObj [Linear k C] (E F : C) : ℤ :=
∑ᶠ n : ℤ, (n.negOnePow : ℤ) * (Module.finrank k (E ⟶ (shiftFunctor C n).obj F) : ℤ)