Every numbered result from Stability conditions on triangulated categories by Tom Bridgeland (2007), joined with @[informal]-tagged Lean declarations rendered via Verso + SubVerso. Click any row to expand.
entries36complete16incomplete3missing17
Def 1.1
complete
A stability condition (Z, 𝒫) on a triangulated category 𝒟 consists of a group …
L57–L69
›
§1. Introduction
A stability condition (Z, 𝒫) on a triangulated category 𝒟 consists of a group homomorphism Z : K(𝒟) → ℂ called the central charge, and full additive subcategories 𝒫(φ) ⊂ 𝒟 for each φ ∈ ℝ, satisfying the following axioms: (a) if E ∈ 𝒫(φ) then Z(E) = m(E) · exp(iπφ) for some m(E) ∈ ℝ_{>0}; (b) for all φ ∈ ℝ, 𝒫(φ + 1) = 𝒫(φ)[1]; (c) if φ₁ > φ₂ and Aⱼ ∈ 𝒫(φⱼ) then Hom_𝒟(A₁, A₂) = 0; (d) for each nonzero object E ∈ 𝒟 there is a finite sequence of real numbers φ₁ > φ₂ > ⋯ > φₙ and objects E₀, E₁, …, Eₙ ∈ 𝒟 with E₀ = 0, Eₙ = E, together with distinguished triangles Eⱼ₋₁ → Eⱼ → Aⱼ → Eⱼ₋₁[1] for 1 ≤ j ≤ n in which Aⱼ ∈ 𝒫(φⱼ). The same definition is restated more compactly as Definition 5.1 in §5, after slicings (Definition 3.3) are introduced to package axioms (b)–(d).
@[informal"Definition 1.1""restated as Def 5.1"complete,informal"Definition 5.1"complete]structureWithClassMap(v:K₀C→+Λ)where/-- The underlying slicing. -/slicing:SlicingC/-- The central charge on the class lattice `Λ`. -/Z:Λ→+ℂ/-- Compatibility (raw). Use `σ.compat` instead. -/compat':∀(φ:ℝ)(E:C),slicing.PφE→¬IsZeroE→∃(m:ℝ),0<m∧Z(v(K₀.ofCE))=↑m*Complex.exp(↑(Real.pi*φ)*Complex.I)
Thm 1.2
complete
Let 𝒟 be a triangulated category. For each connected component Σ ⊂ Stab(𝒟) …
L214–L657
›
§1. Introduction
Let 𝒟 be a triangulated category. For each connected component Σ ⊂ Stab(𝒟) there is a linear subspace V(Σ) ⊂ Hom_ℤ(K(𝒟), ℂ) with a well-defined linear topology and a local homeomorphism Z : Σ → V(Σ) which maps a stability condition (Z, 𝒫) to its central charge Z.
Suppose 𝒟 is numerically finite. For each connected component Σ ⊂ Stab_N(𝒟) …
L172–L219
›
§1. Introduction
Suppose 𝒟 is numerically finite. For each connected component Σ ⊂ Stab_N(𝒟) there is a subspace V(Σ) ⊂ Hom_ℤ(N(𝒟), ℂ) and a local homeomorphism Z : Σ → V(Σ) which maps a stability condition to its central charge. In particular Σ is a finite-dimensional complex manifold.
@[informal"Corollary 1.3""class-map generalization; manifold consequence only"complete]theoremStabilityCondition.WithClassMap.existsComplexManifoldOnConnectedComponent{Λ:Typeu'}[AddCommGroupΛ][AddGroup.FGΛ]{v:K₀C→+Λ}[Fact(Function.Surjectivev)](cc:StabilityCondition.WithClassMap.ComponentIndexCv):∃(E:Typeu')(_:NormedAddCommGroupE)(_:NormedSpaceℂE)(_:FiniteDimensionalℂE)(_:ChartedSpaceE(StabilityCondition.WithClassMap.ComponentCvcc)),IsManifold(𝓘(ℂ,E))(⊤:WithTopℕ∞)(StabilityCondition.WithClassMap.ComponentCvcc):=C:Type uinst✝⁹:Category.{v, u}Cinst✝⁸:HasZeroObjectCinst✝⁷:HasShiftCℤinst✝⁶:PreadditiveCinst✝⁵:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝⁴:PretriangulatedCinst✝³:IsTriangulatedCΛ:Type u'inst✝²:AddCommGroupΛinst✝¹:AddGroup.FGΛv:K₀C→+Λinst✝:Fact(Function.Surjective⇑v)cc:ComponentIndexCv⊢ ∃Exx_1,∃(_:FiniteDimensionalℂE),∃x_3,IsManifold𝓘(ℂ,E)⊤(ComponentCvcc)-- The local model from Theorem 1.2C:Type uinst✝⁹:Category.{v, u}Cinst✝⁸:HasZeroObjectCinst✝⁷:HasShiftCℤinst✝⁶:PreadditiveCinst✝⁵:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝⁴:PretriangulatedCinst✝³:IsTriangulatedCΛ:Type u'inst✝²:AddCommGroupΛinst✝¹:AddGroup.FGΛv:K₀C→+Λinst✝:Fact(Function.Surjective⇑v)cc:ComponentIndexCvM:ComponentTopologicalLinearLocalModelCcc:=componentTopologicalLinearLocalModelCcc⊢ ∃Exx_1,∃(_:FiniteDimensionalℂE),∃x_3,IsManifold𝓘(ℂ,E)⊤(ComponentCvcc)-- V(Σ) is finite-dimensional: it's a submodule of Hom(Λ, ℂ) which has finite rankTry this: haveI̵The goal is a proposition, so `have` is preferred over `haveI`.The difference between `have` and `haveI` is that `haveI` inlines the value.But this is not relevant for proofs because of proof irrelevance.Note: This linter can be disabled with `set_option linter.style.haveILetI false`
@[informal"Corollary 1.3""complex manifold conclusion only; local homeomorphism is in componentTopologicalLinearLocalModel"complete]theoremNumericalStabilityCondition.existsComplexManifoldOnConnectedComponent(k:Typew)[Fieldk][LinearkC][IsFiniteTypekC][(shiftFunctorC(1:ℤ)).Lineark][NumericallyFinitekC](cc:StabilityCondition.WithClassMap.ComponentIndexC(numericalQuotientMapkC)):∃(E:Typeu)(_:NormedAddCommGroupE)(_:NormedSpaceℂE)(_:FiniteDimensionalℂE)(_:ChartedSpaceE(NumericalComponent(k:=k)Ccc)),IsManifold(𝓘(ℂ,E))(⊤:WithTopℕ∞)(NumericalComponent(k:=k)Ccc):=C:Type uinst✝¹¹:Category.{v, u}Cinst✝¹⁰:HasZeroObjectCinst✝⁹:HasShiftCℤinst✝⁸:PreadditiveCinst✝⁷:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝⁶:PretriangulatedCinst✝⁵:IsTriangulatedCk:Type winst✝⁴:Fieldkinst✝³:LinearkCinst✝²:IsFiniteTypekCinst✝¹:Functor.Lineark(shiftFunctorC1)inst✝:NumericallyFinitekCcc:StabilityCondition.WithClassMap.ComponentIndexC(numericalQuotientMapkC)⊢ ∃Exx_1,∃(_:FiniteDimensionalℂE),∃x_3,IsManifold𝓘(ℂ,E)⊤(NumericalComponentkCcc)Try this: haveI̵The goal is a proposition, so `have` is preferred over `haveI`.The difference between `have` and `haveI` is that `haveI` inlines the value.But this is not relevant for proofs because of proof irrelevance.Note: This linter can be disabled with `set_option linter.style.haveILetI false`
Def 2.1
complete
A stability function on an abelian category 𝒜 is a group homomorphism Z : K(𝒜) …
L68–L84
›
§2. Stability functions on abelian categories
A stability function on an abelian category 𝒜 is a group homomorphism Z : K(𝒜) → ℂ such that for all 0 ≠ E ∈ 𝒜 the complex number Z(E) lies in the strict upper half-plane H = { r · exp(iπφ) : r > 0 and 0 < φ ≤ 1 } ⊂ ℂ. The phase of a nonzero object E is then φ(E) = (1/π) · arg Z(E) ∈ (0, 1].
@[informal"Definition 2.1"complete]structureStabilityFunction(A:Typeu)[Category.{v}A][AbelianA]where/-- The central charge on objects. -/Zobj:A→ℂ/-- The zero object maps to zero. -/map_zero':∀(X:A),IsZeroX→ZobjX=0/-- Additivity on short exact sequences: `Z(B) = Z(A) + Z(C)` for `0 → A → B → C → 0`. -/additive:∀(S:ShortComplexA),S.ShortExact→ZobjS.X₂=ZobjS.X₁+ZobjS.X₃/-- Every nonzero object maps into the semi-closed upper half plane. -/upper:∀(E:A),¬IsZeroE→ZobjE∈upperHalfPlaneUnion
Def 2.2
complete
Let Z : K(𝒜) → ℂ be a stability function on an abelian category 𝒜. An object 0 …
L114–L120
›
§2. Stability functions on abelian categories
Let Z : K(𝒜) → ℂ be a stability function on an abelian category 𝒜. An object 0 ≠ E ∈ 𝒜 is said to be semistable (with respect to Z) if every subobject 0 ≠ A ⊂ E satisfies φ(A) ≤ φ(E).
Let Z : K(𝒜) → ℂ be a stability function on an abelian category 𝒜. A …
L38–L76
›
§2. Stability functions on abelian categories
Let Z : K(𝒜) → ℂ be a stability function on an abelian category 𝒜. A Harder–Narasimhan filtration of an object 0 ≠ E ∈ 𝒜 is a finite chain of subobjects 0 = E₀ ⊂ E₁ ⊂ ⋯ ⊂ Eₙ₋₁ ⊂ Eₙ = E whose factors Fⱼ = Eⱼ / Eⱼ₋₁ are semistable objects of 𝒜 with φ(F₁) > φ(F₂) > ⋯ > φ(Fₙ). The stability function Z is said to have the Harder–Narasimhan property if every nonzero object of 𝒜 has a Harder–Narasimhan filtration.
@[informal"Definition 2.3""HN filtration for abelian categories"complete]structureAbelianHNFiltration(Z:StabilityFunctionA)(E:A)where/-- The number of semistable factors. -/n:ℕhn:0<n/-- The chain of subobjects, strictly monotone. -/chain:Fin(n+1)→SubobjectEchain_strictMono:StrictMonochainchain_bot:chain⟨0,Nat.zero_lt_succ_⟩=⊥chain_top:chain⟨n,n.lt_succ_iff.mprle_rfl⟩=⊤/-- The phases of the semistable quotients, in strictly decreasing order. -/φ:Finn→ℝφ_anti:StrictAntiφ/-- The phase of each factor equals the given phase. -/factor_phase:∀(j:Finn),Z.phase(cokernel(Subobject.ofLE(chainj.castSucc)(chainj.succ)(le_of_lt(chain_strictMonoj.castSucc_lt_succ))))=φj/-- Each successive quotient is semistable. -/factor_semistable:∀(j:Finn),Z.IsSemistable(cokernel(Subobject.ofLE(chainj.castSucc)(chainj.succ)(le_of_lt(chain_strictMonoj.castSucc_lt_succ))))
Suppose 𝒜 is an abelian category with a stability function Z : K(𝒜) → ℂ …
›
§2. Stability functions on abelian categories
Suppose 𝒜 is an abelian category with a stability function Z : K(𝒜) → ℂ satisfying the chain conditions (a) there are no infinite sequences of subobjects ⋯ ⊂ Eⱼ₊₁ ⊂ Eⱼ ⊂ ⋯ ⊂ E₂ ⊂ E₁ in 𝒜 with φ(Eⱼ₊₁) > φ(Eⱼ) for all j, and (b) there are no infinite sequences of quotients E₁ ↠ E₂ ↠ ⋯ ↠ Eⱼ ↠ Eⱼ₊₁ ↠ ⋯ in 𝒜 with φ(Eⱼ) > φ(Eⱼ₊₁) for all j. Then 𝒜 has the Harder–Narasimhan property.
Not yet formalized in this project.
Def 3.1
complete
A t-structure on a triangulated category 𝒟 is a full subcategory ℱ ⊂ 𝒟, …
L55–L69
›
§3. t-structures and slicings
A t-structure on a triangulated category 𝒟 is a full subcategory ℱ ⊂ 𝒟, satisfying ℱ[1] ⊂ ℱ, such that if one defines ℱ^⊥ = { G ∈ 𝒟 : Hom_𝒟(F, G) = 0 for all F ∈ ℱ }, then for every object E ∈ 𝒟 there is a triangle F → E → G in 𝒟 with F ∈ ℱ and G ∈ ℱ^⊥. The heart of the t-structure is the full subcategory 𝒜 = ℱ ∩ ℱ^⊥[1] ⊂ 𝒟; the t-structure is bounded if 𝒟 = ⋃_{i,j ∈ ℤ} ℱ[i] ∩ ℱ^⊥[j].
Formalized upstream as CategoryTheory.Triangulated.TStructure in Mathlib.CategoryTheory.Triangulated.TStructure.Basic.
Lem 3.2
missing
Let 𝒜 ⊂ 𝒟 be a full additive subcategory of a triangulated category 𝒟. Then 𝒜 …
›
§3. t-structures and slicings
Let 𝒜 ⊂ 𝒟 be a full additive subcategory of a triangulated category 𝒟. Then 𝒜 is the heart of a bounded t-structure ℱ ⊂ 𝒟 if and only if the following two conditions hold: (a) if k₁ > k₂ are integers and A, B are objects of 𝒜 then Hom_𝒟(A[k₁], B[k₂]) = 0; and (b) for every nonzero object E ∈ 𝒟 there is a finite sequence of integers k₁ > k₂ > ⋯ > kₙ and objects E₀, E₁, …, Eₙ ∈ 𝒟 with E₀ = 0, Eₙ = E, together with distinguished triangles Eⱼ₋₁ → Eⱼ → Aⱼ → Eⱼ₋₁[1] for 1 ≤ j ≤ n in which Aⱼ ∈ 𝒜[kⱼ].
Not yet formalized in this project.
Def 3.3
complete
A slicing 𝒫 of a triangulated category 𝒟 consists of full additive …
L63–L96
›
§3. t-structures and slicings
A slicing 𝒫 of a triangulated category 𝒟 consists of full additive subcategories 𝒫(φ) ⊂ 𝒟 for each φ ∈ ℝ satisfying the following axioms: (a) for all φ ∈ ℝ, 𝒫(φ + 1) = 𝒫(φ)[1]; (b) if φ₁ > φ₂ and Aⱼ ∈ 𝒫(φⱼ) then Hom_𝒟(A₁, A₂) = 0; (c) for each nonzero object E ∈ 𝒟 there is a finite sequence of real numbers φ₁ > φ₂ > ⋯ > φₙ and objects E₀, E₁, …, Eₙ ∈ 𝒟 with E₀ = 0, Eₙ = E, together with distinguished triangles Eⱼ₋₁ → Eⱼ → Aⱼ → Eⱼ₋₁[1] for 1 ≤ j ≤ n in which Aⱼ ∈ 𝒫(φⱼ). Writing φ⁺(E) = φ₁ and φ⁻(E) = φₙ for the maximum and minimum phases appearing in this decomposition of E, the full additive subcategory 𝒫(I) ⊂ 𝒟 for an interval I ⊂ ℝ consists of the zero objects together with the 0 ≠ E whose phases satisfy φ⁻(E), φ⁺(E) ∈ I.
@[informal"Definition 3.3""axiom (c): HN decomposition data for triangulated categories"]structureHNFiltration(P:ℝ→ObjectPropertyC)(E:C)extendsPostnikovTowerCEwhere/-- The phases of the semistable factors, in strictly decreasing order. -/φ:Finn→ℝ/-- The phases are strictly decreasing (higher phase factors appear first). -/hφ:StrictAntiφ/-- Each factor is semistable of the given phase. -/semistable:∀j,(P(φj))(toPostnikovTower.factorj)
@[informal"Definition 3.3"complete]structureSlicingwhere/-- For each phase `φ ∈ ℝ`, the property of semistable objects of phase `φ`. -/P:ℝ→ObjectPropertyC/-- Each phase slice is closed under isomorphisms. -/closedUnderIso:∀(φ:ℝ),(Pφ).IsClosedUnderIsomorphisms/-- The zero object satisfies every phase predicate. -/zero_mem:∀(φ:ℝ),(Pφ)(0:C)/-- Shifting by `[1]` increases the phase by 1, and conversely. -/shift_iff:∀(φ:ℝ)(X:C),(Pφ)X↔(P(φ+1))(X⟦(1:ℤ)⟧)/-- Morphisms from higher-phase to lower-phase nonzero semistable objects vanish. -/hom_vanishing:∀(φ₁φ₂:ℝ)(AB:C),φ₂<φ₁→(Pφ₁)A→(Pφ₂)B→∀(f:A⟶B),f=0/-- Every object has a Harder-Narasimhan filtration. -/hn_exists:∀(E:C),Nonempty(HNFiltrationCPE)
Lem 3.4
complete
Let 𝒫 be a slicing of a triangulated category 𝒟 and let I ⊂ ℝ be an interval of …
L444–L459
›
§3. t-structures and slicings
Let 𝒫 be a slicing of a triangulated category 𝒟 and let I ⊂ ℝ be an interval of length at most one. Suppose A → E → B → A[1] is a distinguished triangle in 𝒟 all of whose vertices are nonzero objects of 𝒫(I). Then φ⁺(A) ≤ φ⁺(E) and φ⁻(E) ≤ φ⁻(B).
A quasi-abelian category is an additive category 𝒜 with kernels and cokernels …
L275–L287
›
§4. Quasi-abelian categories
A quasi-abelian category is an additive category 𝒜 with kernels and cokernels such that every pullback of a strict epimorphism is a strict epimorphism, and every pushout of a strict monomorphism is a strict monomorphism. A morphism f in 𝒜 is strict if the canonical map coim f → im f is an isomorphism. A strict short exact sequence in 𝒜 is a sequence 0 → A → B → C → 0 in which A → B is a strict monomorphism with cokernel B → C; equivalently, B → C is a strict epimorphism with kernel A → B.
@[informal"Definition 4.1"complete]classQuasiAbelian:Propwhere/-- The pullback of a strict epimorphism along any morphism is a strict epimorphism. -/pullback_strictEpi:∀{XYZ:C}(f:X⟶Z)(g:Y⟶Z),IsStrictEpig→IsStrictEpi(pullback.fstfg)/-- The pushout of a strict monomorphism along any morphism is a strict monomorphism. -/pushout_strictMono:∀{XYZ:C}(f:Z⟶X)(g:Z⟶Y),IsStrictMonof→IsStrictMono(pushout.inrfg)
Lem 4.2
missing
An additive category 𝒜 is quasi-abelian if and only if there are abelian …
›
§4. Quasi-abelian categories
An additive category 𝒜 is quasi-abelian if and only if there are abelian categories 𝒜^♯ and 𝒜^♭ and fully faithful embeddings 𝒜 ⊂ 𝒜^♯ and 𝒜 ⊂ 𝒜^♭ such that (a) if A → E is a monomorphism in 𝒜^♯ with E ∈ 𝒜 then A ∈ 𝒜, and (b) if E → B is an epimorphism in 𝒜^♭ with E ∈ 𝒜 then B ∈ 𝒜. When these conditions hold, the strict short exact sequences in 𝒜 are precisely the sequences 0 → A → B → C → 0 which are exact in both 𝒜^♯ and 𝒜^♭.
Not yet formalized in this project.
Lem 4.3
missing
Let 𝒫 be a slicing of a triangulated category 𝒟. For any interval I ⊂ ℝ of …
›
§4. Quasi-abelian categories
Let 𝒫 be a slicing of a triangulated category 𝒟. For any interval I ⊂ ℝ of length less than 1, the full subcategory 𝒫(I) ⊂ 𝒟 is quasi-abelian, and its strict short exact sequences are in one-to-one correspondence with distinguished triangles in 𝒟 all of whose vertices are objects of 𝒫(I).
Not yet formalized in this project.
Def 4.4
incomplete
A skewed stability function on a quasi-abelian category 𝒜 is a group …
L671–L691
›
§4. Quasi-abelian categories
A skewed stability function on a quasi-abelian category 𝒜 is a group homomorphism Z : K(𝒜) → ℂ such that there is a strict half-plane H_α = { r · exp(iπφ) : r > 0 and α < φ ≤ α + 1 } ⊂ ℂ, defined by some α ∈ ℝ, with Z(E) ∈ H_α for all objects 0 ≠ E ∈ 𝒜. The phase of 0 ≠ E ∈ 𝒜 is then φ(E) = (1/π) · arg Z(E) ∈ (α, α + 1].
@[informal"Definition 4.4""weaker: only σ-semistable nonvanishing, not all nonzero objects"]structureSkewedStabilityFunction{Λ:Typeu'}[AddCommGroupΛ](v:K₀C→+Λ)(s:SlicingC)(ab:ℝ)where/-- The group homomorphism (typically a perturbation of the central charge). -/W:Λ→+ℂ/-- The skewing parameter, lying in the interval `(a, b)`. -/α:ℝ/-- The skewing parameter lies in the interval. -/hα_mem:a<α∧α<b/-- For every nonzero semistable object of phase `φ ∈ (a, b)`, the central charge
`W(v[E])` is nonzero. -/nonzero:∀(E:C)(φ:ℝ),a<φ→φ<b→(s.Pφ)E→¬IsZeroE→W(clCvE)≠0
Def 5.1
complete
A stability condition σ = (Z, 𝒫) on a triangulated category 𝒟 consists of a …
L57–L69
›
§5. Stability conditions
A stability condition σ = (Z, 𝒫) on a triangulated category 𝒟 consists of a group homomorphism Z : K(𝒟) → ℂ and a slicing 𝒫 of 𝒟 such that if 0 ≠ E ∈ 𝒫(φ) then Z(E) = m(E) · exp(iπφ) for some m(E) ∈ ℝ_{>0}. The linear map Z is called the central charge; the nonzero objects of 𝒫(φ) are the σ-semistable objects of phase φ, and the simple objects of 𝒫(φ) are σ-stable.
@[informal"Definition 1.1""restated as Def 5.1"complete,informal"Definition 5.1"complete]structureWithClassMap(v:K₀C→+Λ)where/-- The underlying slicing. -/slicing:SlicingC/-- The central charge on the class lattice `Λ`. -/Z:Λ→+ℂ/-- Compatibility (raw). Use `σ.compat` instead. -/compat':∀(φ:ℝ)(E:C),slicing.PφE→¬IsZeroE→∃(m:ℝ),0<m∧Z(v(K₀.ofCE))=↑m*Complex.exp(↑(Real.pi*φ)*Complex.I)
Lem 5.2
complete
If σ = (Z, 𝒫) is a stability condition on a triangulated category 𝒟 then each …
L818–L825
›
§5. Stability conditions
If σ = (Z, 𝒫) is a stability condition on a triangulated category 𝒟 then each subcategory 𝒫(φ) ⊂ 𝒟 is abelian.
To give a stability condition on a triangulated category 𝒟 is equivalent to …
L241–L709
›
§5. Stability conditions
To give a stability condition on a triangulated category 𝒟 is equivalent to giving a bounded t-structure on 𝒟 and a stability function on its heart with the Harder–Narasimhan property.
@[informal"Proposition 5.3""reverse: partial, missing central charge construction + HN existence"]defHeartStabilityData.toPhasePackage(h:HeartStabilityDataC):PhasePackageCwhereheartData:=hP:=phasePredicate(C:=C)hclosedUnderIso:=phasePredicate_closedUnderIso(C:=C)hzero_mem:=fun_↦Or.inl(isZero_zeroC)shift_iff:=phasePredicate_shift_iff(C:=C)hhom_vanishing:=fun_φ₁_φ₂_A_BhlthAhBf↦phasePredicate_hom_zero(C:=C)hhAhBhltf
Example 5.4
missing
Let 𝒜 be the category of coherent 𝒪_X-modules on a nonsingular projective curve …
›
§5. Stability conditions
Let 𝒜 be the category of coherent 𝒪_X-modules on a nonsingular projective curve X over an algebraically closed field k of characteristic zero, and set Z(E) = − deg(E) + i · rank(E). Applying Proposition 5.3 gives a stability condition on the bounded derived category D(𝒜).
Not yet formalized in this project.
Example 5.5
missing
Let A be a finite-dimensional algebra over a field k and let 𝒜 be the abelian …
›
§5. Stability conditions
Let A be a finite-dimensional algebra over a field k and let 𝒜 be the abelian category of finite-dimensional left A-modules. Then 𝒜 is a finite-length category whose Grothendieck group K(𝒜) is the free abelian group on the (finite) set of simple A-modules. There is a group homomorphism r : K(𝒜) → ℤ sending an A-module to its dimension over k, and for any homomorphism λ : K(𝒜) → ℝ the formula Z(E) = λ(E) + i · r(E) defines a stability function on 𝒜. Proposition 5.3 then produces a stability condition on the bounded derived category D(𝒜) for each such slope function.
Not yet formalized in this project.
Example 5.6
missing
Let 𝒜 be the category of coherent sheaves on a nonsingular projective curve X …
›
§5. Stability conditions
Let 𝒜 be the category of coherent sheaves on a nonsingular projective curve X as in Example 5.4, and let (Z, 𝒫) be the stability condition defined there. Let 0 < α < 1/2 be such that ζ = tan(πα) is irrational. Then the bounded t-structure 𝒫(> α) = 𝒫(≥ α) ⊂ 𝒟 has heart ℬ = 𝒫((α, α + 1)). Define a stability function on ℬ by W(E) = i · (rank(E) + ζ · deg(E)); all nonzero objects of ℬ are semistable of the same phase. Applying Proposition 5.3 gives a stability condition (W, 𝒬) on 𝒟 with 𝒬(1/2) = ℬ and 𝒬(ψ) = 0 unless ψ − 1/2 ∈ ℤ.
Not yet formalized in this project.
Def 5.7
complete
A slicing 𝒫 of a triangulated category 𝒟 is locally-finite if there exists a …
L124–L295
›
§5. Stability conditions
A slicing 𝒫 of a triangulated category 𝒟 is locally-finite if there exists a real number η > 0 such that for all t ∈ ℝ the quasi-abelian category 𝒫((t − η, t + η)) ⊂ 𝒟 is of finite length. A stability condition (Z, 𝒫) is locally-finite if the corresponding slicing 𝒫 is.
omit[IsTriangulatedC]in/-- A slicing is locally finite if there exists `η > 0` with `η < 1/2` such that every
object in each thin interval category `P((t-η, t+η))` has finite length in the
quasi-abelian sense, i.e. ACC/DCC on strict subobjects.
The extra bound `η < 1/2` is a harmless normalization: any Bridgeland witness may be
shrunk to such an `η`, and then the width `2η` is at most `1`, so the thin interval
category carries the exact / quasi-abelian structure proved above. -/@[informal"Definition 5.7""per-object strict finite length is weaker than finite length of all chains (paper's assumption)"]structureSlicing.IsLocallyFinite(s:SlicingC):PropwhereintervalFinite:∃η:ℝ,∃hη:0<η,∃hη':η<1/2,∀t:ℝ,leta:=t-ηletb:=t+ηletI:Fact(a<b):=⟨C:Type uinst✝⁸:Category.{v, u}Cinst✝⁷:HasZeroObjectCinst✝⁶:HasShiftCℤinst✝⁵:PreadditiveCinst✝⁴:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝³:PretriangulatedCinst✝²:IsTriangulatedCa✝:ℝb✝:ℝinst✝¹:Fact(a✝<b✝)inst✝:Fact(b✝-a✝≤1)s:SlicingCη:ℝhη:0<ηhη':η<1/2t:ℝa:ℝ:=t-ηb:ℝ:=t+η⊢ a<bC:Type uinst✝⁸:Category.{v, u}Cinst✝⁷:HasZeroObjectCinst✝⁶:HasShiftCℤinst✝⁵:PreadditiveCinst✝⁴:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝³:PretriangulatedCinst✝²:IsTriangulatedCa✝:ℝb✝:ℝinst✝¹:Fact(a✝<b✝)inst✝:Fact(b✝-a✝≤1)s:SlicingCη:ℝhη:0<ηhη':η<1/2t:ℝa:ℝ:=t-ηb:ℝ:=t+η⊢ t-η<t+ηAll goals completed! 🐙⟩letI:Fact(b-a≤1):=⟨C:Type uinst✝⁸:Category.{v, u}Cinst✝⁷:HasZeroObjectCinst✝⁶:HasShiftCℤinst✝⁵:PreadditiveCinst✝⁴:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝³:PretriangulatedCinst✝²:IsTriangulatedCa✝:ℝb✝:ℝinst✝¹:Fact(a✝<b✝)inst✝:Fact(b✝-a✝≤1)s:SlicingCη:ℝhη:0<ηhη':η<1/2t:ℝa:ℝ:=t-ηb:ℝ:=t+ηthis:Fact(a<b):=···⊢ b-a≤1C:Type uinst✝⁸:Category.{v, u}Cinst✝⁷:HasZeroObjectCinst✝⁶:HasShiftCℤinst✝⁵:PreadditiveCinst✝⁴:∀(n:ℤ),(shiftFunctorCn).Additiveinst✝³:PretriangulatedCinst✝²:IsTriangulatedCa✝:ℝb✝:ℝinst✝¹:Fact(a✝<b✝)inst✝:Fact(b✝-a✝≤1)s:SlicingCη:ℝhη:0<ηhη':η<1/2t:ℝa:ℝ:=t-ηb:ℝ:=t+ηthis:Fact(a<b):=···⊢ t+η-(t-η)≤1All goals completed! 🐙⟩∀(E:s.IntervalCatCab),IsStrictArtinianObjectE∧IsStrictNoetherianObjectE
@[informal"Definition 5.7"complete]structureWithClassMap(v:K₀C→+Λ)extendsPreStabilityCondition.WithClassMapCvwhere/-- The slicing is locally finite. -/locallyFinite:slicing.IsLocallyFiniteC
Lem 6.1
incomplete
If 𝒫 and 𝒬 are slicings of a triangulated category 𝒟 then d(𝒫, 𝒬) = inf { ε ∈ …
L91–L99
›
§6. The space of stability conditions
If 𝒫 and 𝒬 are slicings of a triangulated category 𝒟 then d(𝒫, 𝒬) = inf { ε ∈ ℝ_{≥0} : 𝒬(φ) ⊂ 𝒫([φ − ε, φ + ε]) for all φ ∈ ℝ }.
For each connected component Σ ⊂ Stab(𝒟) there is a linear subspace V(Σ) ⊂ …
›
§6. The space of stability conditions
For each connected component Σ ⊂ Stab(𝒟) there is a linear subspace V(Σ) ⊂ Hom_ℤ(K(𝒟), ℂ) with a well-defined linear topology and a continuous map Z : Σ → V(Σ) which sends a stability condition (Z, 𝒫) to its central charge Z.
Not yet formalized in this project.
Lem 6.4
complete
Suppose σ = (Z, 𝒫) and τ = (Z, 𝒬) are stability conditions on 𝒟 with the same …
L547–L557
›
§6. The space of stability conditions
Suppose σ = (Z, 𝒫) and τ = (Z, 𝒬) are stability conditions on 𝒟 with the same central charge Z and with d(𝒫, 𝒬) < 1. Then σ = τ.
Let σ = (Z, 𝒫) be a locally-finite stability condition on a triangulated …
L122–L137
›
§7. Deformations of stability conditions
Let σ = (Z, 𝒫) be a locally-finite stability condition on a triangulated category 𝒟. Then there is an ε₀ > 0 such that if 0 < ε < ε₀ and W : K(𝒟) → ℂ is a group homomorphism satisfying |W(E) − Z(E)| < sin(πε) · |Z(E)| for all E ∈ 𝒟 semistable in σ, then there is a locally-finite stability condition τ = (W, 𝒬) on 𝒟 with d(𝒫, 𝒬) < ε.
A thin subcategory of 𝒟 is a full subcategory of the form 𝒫((a, b)) ⊂ 𝒟 where a …
›
§7. Deformations of stability conditions
A thin subcategory of 𝒟 is a full subcategory of the form 𝒫((a, b)) ⊂ 𝒟 where a and b are real numbers with 0 < b − a < 1 − 2ε. Any thin subcategory is quasi-abelian, and W defines a skewed stability function on it.
Not yet formalized in this project.
Lem 7.3
missing
Suppose E is W-semistable in some thin subcategory 𝒜 ⊂ 𝒟, and set ψ = ψ(E). …
›
§7. Deformations of stability conditions
Suppose E is W-semistable in some thin subcategory 𝒜 ⊂ 𝒟, and set ψ = ψ(E). Then E ∈ 𝒫((ψ − ε, ψ + ε)).
Not yet formalized in this project.
Def 7.4
missing
Suppose 𝒜 = 𝒫((a, b)) is a thin subcategory of 𝒟. A nonzero object E ∈ 𝒜 is …
›
§7. Deformations of stability conditions
Suppose 𝒜 = 𝒫((a, b)) is a thin subcategory of 𝒟. A nonzero object E ∈ 𝒜 is said to be enveloped by 𝒜 if a + ε ≤ ψ(E) ≤ b − ε.
Not yet formalized in this project.
Lem 7.5
missing
Suppose an object E ∈ 𝒟 is enveloped by thin subcategories ℬ and 𝒞 of 𝒟. Then E …
›
§7. Deformations of stability conditions
Suppose an object E ∈ 𝒟 is enveloped by thin subcategories ℬ and 𝒞 of 𝒟. Then E is W-semistable in ℬ precisely if it is W-semistable in 𝒞.
Not yet formalized in this project.
Lem 7.6
missing
If E ∈ 𝒬(ψ₁) and F ∈ 𝒬(ψ₂) with ψ₁ > ψ₂, then Hom_𝒟(E, F) = 0.
›
§7. Deformations of stability conditions
If E ∈ 𝒬(ψ₁) and F ∈ 𝒬(ψ₂) with ψ₁ > ψ₂, then Hom_𝒟(E, F) = 0.
Not yet formalized in this project.
Lem 7.7
missing
Let 𝒜 = 𝒫((a, b)) ⊂ 𝒟 be a thin subcategory of finite length. Then every …
›
§7. Deformations of stability conditions
Let 𝒜 = 𝒫((a, b)) ⊂ 𝒟 be a thin subcategory of finite length. Then every nonzero object of 𝒫((a + 2ε, b − 4ε)) has a finite Harder–Narasimhan filtration whose factors are W-semistable objects of 𝒜 which are enveloped by 𝒜.
Not yet formalized in this project.
Prop 8.1
missing
Let 𝒟 be a triangulated category. The function d(σ₁, σ₂) = sup_{0 ≠ E ∈ 𝒟} max( …
›
§8. More on the space of stability conditions
Let 𝒟 be a triangulated category. The function d(σ₁, σ₂) = sup_{0 ≠ E ∈ 𝒟} max( |φ⁻_{σ₂}(E) − φ⁻_{σ₁}(E)|, |φ⁺_{σ₂}(E) − φ⁺_{σ₁}(E)|, |log (m_{σ₂}(E) / m_{σ₁}(E))| ) ∈ [0, ∞] defines a generalised metric on Stab(𝒟). The induced topology is the same as the one defined in §6.
Not yet formalized in this project.
Lem 8.2
missing
The generalised metric space Stab(𝒟) carries a right action of the group …
›
§8. More on the space of stability conditions
The generalised metric space Stab(𝒟) carries a right action of the group GL̃⁺(2, ℝ), the universal covering space of GL⁺(2, ℝ), and a left action by isometries of the group Aut(𝒟) of exact autoequivalences of 𝒟. These two actions commute.
Not yet formalized in this project.
Thm 9.1
missing
Let X be a nonsingular projective curve of genus one over ℂ, and let D(X) …
›
§9. Stability conditions on curves
Let X be a nonsingular projective curve of genus one over ℂ, and let D(X) denote the bounded derived category of coherent 𝒪_X-modules. The action of the group GL̃⁺(2, ℝ) on the space Stab(X) of locally-finite numerical stability conditions is free and transitive, so that Stab(X) ≅ GL̃⁺(2, ℝ).