10. EulerForm.Basic
Module BridgelandStability.EulerForm.Basic — 8 declarations (Definition, Structure)
10.1. CategoryTheory.Triangulated.eulerFormInner
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- For fixed `E`, lift `F ↦ χ(E, F)` to a group homomorphism `K₀ C →+ ℤ`
using the universal property of `K₀`. -/
def eulerFormInner (E : C) : K₀ C →+ ℤ := k:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:C⊢ K₀ C →+ ℤ
k:Type winst✝⁹:Field kC:Type uinst✝⁸:Category.{v, u} Cinst✝⁷:HasZeroObject Cinst✝⁶:HasShift C ℤinst✝⁵:Preadditive Cinst✝⁴:∀ (n : ℤ), (shiftFunctor C n).Additiveinst✝³:Pretriangulated Cinst✝²:IsTriangulated Cinst✝¹:Linear k Cinst✝:IsFiniteType k CE:Cthis:IsTriangleAdditive fun F => eulerFormObj k C E F := ···⊢ K₀ C →+ ℤ
All goals completed! 🐙
10.2. CategoryTheory.Triangulated.eulerForm
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The Euler form on `K₀`, obtained by applying the universal property of `K₀`
twice to `eulerFormObj`. -/
def eulerForm [(shiftFunctor C (1 : ℤ)).Linear k] :
K₀ C →+ K₀ C →+ ℤ :=
K₀.lift C (eulerFormInner k C)
10.3. CategoryTheory.Triangulated.eulerFormRad
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The left radical of the Euler form on `K₀ C`. -/
def eulerFormRad [(shiftFunctor C (1 : ℤ)).Linear k] :
AddSubgroup (K₀ C) :=
(eulerForm k C).ker
10.4. CategoryTheory.Triangulated.NumericalK₀
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The numerical Grothendieck group attached to the Euler form on `K₀`. -/
def NumericalK₀ [(shiftFunctor C (1 : ℤ)).Linear k] :
Type _ :=
K₀ C ⧸ eulerFormRad k C
10.5. CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The `AddCommGroup` instance on `NumericalK₀ k C`. -/
instance NumericalK₀.instAddCommGroup [(shiftFunctor C (1 : ℤ)).Linear k] :
AddCommGroup (NumericalK₀ k C) :=
inferInstanceAs (AddCommGroup (K₀ C ⧸ eulerFormRad k C))
10.6. CategoryTheory.Triangulated.numericalQuotientMap
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The quotient map `K₀(C) → N(C)`. -/
abbrev numericalQuotientMap [(shiftFunctor C (1 : ℤ)).Linear k] :
K₀ C →+ NumericalK₀ k C :=
QuotientAddGroup.mk' (eulerFormRad k C)
10.7. CategoryTheory.Triangulated.NumericallyFinite
Structure | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- The category `C` is numerically finite if the numerical Grothendieck group attached to the
Euler form is finitely generated as an abelian group. -/
class NumericallyFinite [Linear k C] [IsFiniteType k C]
[(shiftFunctor C (1 : ℤ)).Linear k] : Prop where
/-- The Euler-form numerical Grothendieck group is finitely generated. -/
fg : AddGroup.FG (NumericalK₀ k C)
10.8. CategoryTheory.Triangulated.NumericalComponent
Definition | BridgelandStability.EulerForm.Basic | Source | Open Issue
/-- A connected component of numerical stability conditions. -/
abbrev NumericalComponent [(shiftFunctor C (1 : ℤ)).Linear k]
(cc : StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)) :=
StabilityCondition.WithClassMap.Component C (numericalQuotientMap k C) cc