Euler form on K₀

We prove that the Euler form χ(E,F) = Σₙ (-1)ⁿ dim_k Hom(E, F[n]) is triangle-additive in both arguments, then lift it to a bilinear form on K₀.

The proof uses the long exact Hom sequence from the homological Yoneda functor and the rank-nullity theorem for finite-dimensional vector spaces.

theorem CategoryTheory.Triangulated.finrank_mid_of_exact (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)

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

theorem CategoryTheory.Triangulated.eulerSum_of_rank_identity (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Preadditive C] [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))

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

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

theorem CategoryTheory.Triangulated.linearMap_range_eq_ker_of_addMonoidHom (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

instance CategoryTheory.Triangulated.linearCoyonedaObjIsHomological (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] (E : C) : ((linearCoyoneda k C).obj (Opposite.op E)).IsHomological

theorem CategoryTheory.Triangulated.eulerFormObj_contravariant_triangleAdditive (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] (E : C) : IsTriangleAdditive fun (F : C) => eulerFormObj k C E F

theorem CategoryTheory.Triangulated.eulerFormObj_covariant_triangleAdditive (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] (F : C) [Functor.Linear k (shiftFunctor C 1)] : IsTriangleAdditive fun (E : C) => eulerFormObj k C E F

Euler form on K₀

noncomputable def CategoryTheory.Triangulated.eulerFormInner (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] (E : C) : K₀ C →+ ℤ

For fixed E, lift F ↦ χ(E, F) to a group homomorphism K₀ C →+ ℤ using the universal property of K₀.

Equations

• CategoryTheory.Triangulated.eulerFormInner k C E = CategoryTheory.Triangulated.K₀.lift C fun (F : C) => CategoryTheory.Triangulated.eulerFormObj k C E F

instance CategoryTheory.Triangulated.eulerFormInner_isTriangleAdditive (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : IsTriangleAdditive (eulerFormInner k C)

The outer function E ↦ eulerFormInner E is triangle-additive, so the Euler form descends to a bilinear form on K₀.

noncomputable def CategoryTheory.Triangulated.eulerForm (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : K₀ C →+ K₀ C →+ ℤ

The Euler form on K₀, obtained by applying the universal property of K₀ twice to eulerFormObj.

Equations

• CategoryTheory.Triangulated.eulerForm k C = CategoryTheory.Triangulated.K₀.lift C (CategoryTheory.Triangulated.eulerFormInner k C)

noncomputable def CategoryTheory.Triangulated.eulerFormRad (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : AddSubgroup (K₀ C)

The left radical of the Euler form on K₀ C.

Equations

• CategoryTheory.Triangulated.eulerFormRad k C = (CategoryTheory.Triangulated.eulerForm k C).ker

def CategoryTheory.Triangulated.NumericalK₀ (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : Type u

The numerical Grothendieck group attached to the Euler form on K₀.

Equations

• CategoryTheory.Triangulated.NumericalK₀ k C = (CategoryTheory.Triangulated.K₀ C ⧸ CategoryTheory.Triangulated.eulerFormRad k C)

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.NumericalK₀.instAddCommGroup (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : AddCommGroup (NumericalK₀ k C)

The AddCommGroup instance on NumericalK₀ k C.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.numericalQuotientMap (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : K₀ C →+ NumericalK₀ k C

The quotient map K₀(C) → N(C).

Equations

• CategoryTheory.Triangulated.numericalQuotientMap k C = QuotientAddGroup.mk' (CategoryTheory.Triangulated.eulerFormRad k C)

class CategoryTheory.Triangulated.NumericallyFinite (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : Prop

The category C is numerically finite if the numerical Grothendieck group attached to the Euler form is finitely generated as an abelian group.

• fg : AddGroup.FG (NumericalK₀ k C)

  The Euler-form numerical Grothendieck group is finitely generated.

instance CategoryTheory.Triangulated.instFGNumericalK₀OfNumericallyFinite (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] [NumericallyFinite k C] : AddGroup.FG (NumericalK₀ k C)

Instance synthesis for the finite generation of the numerical Grothendieck group.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.NumericalStabilityCondition (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : Type u

Numerical stability conditions are stability conditions whose central charge factors through the canonical numerical quotient map K₀(C) → N(C).

Equations

• CategoryTheory.Triangulated.NumericalStabilityCondition k C = CategoryTheory.Triangulated.StabilityCondition.WithClassMap C (CategoryTheory.Triangulated.numericalQuotientMap k C)

Corollary 1.3 packaging

@[reducible, inline]

abbrev CategoryTheory.Triangulated.NumericalStabilityCondition.CentralChargeIsLocalHomeomorphOnConnectedComponents (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] : Prop

The local-homeomorphism package for connected components of numerical stability conditions. This is the proposition-object behind Bridgeland's Corollary 1.3.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.NumericalComponent (k : Type w) [Field k] (C : Type u) [Category.{v, u} C] [Limits.HasZeroObject C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] [IsTriangulated C] [Linear k C] [IsFiniteType k C] [Functor.Linear k (shiftFunctor C 1)] (cc : StabilityCondition.WithClassMap.ComponentIndex C (numericalQuotientMap k C)) : Type u

A connected component of numerical stability conditions.

Equations

• CategoryTheory.Triangulated.NumericalComponent k C cc = CategoryTheory.Triangulated.StabilityCondition.WithClassMap.Component C (CategoryTheory.Triangulated.numericalQuotientMap k C) cc