The algebraic stability condition on the bounded derived category of a field

This file constructs the standard, nonzero algebraic stability condition on Dᵇ(FGModuleCat k). Its heart is finite-dimensional vector spaces, every nonzero heart object has phase one, and the unique stable orbit is represented by the one-dimensional vector space in degree zero.

The construction is deliberately categorical. Its central charge is minus the Euler pairing with the degree-zero copy of k; no free lattice is identified with the triangulated Grothendieck group.

theorem CategoryTheory.Triangulated.AlgebraicWitness.moduleCat_isArtinianObject (k : Type u) [Field k] (M : ModuleCat k) [IsArtinian k ↑M] : IsArtinianObject M

Algebraic Artinianness of a module gives categorical Artinianness.

theorem CategoryTheory.Triangulated.AlgebraicWitness.fgModuleCat_isArtinianObject (k : Type u) [Field k] (M : FGModuleCat k) : IsArtinianObject M

A finitely generated vector space is Artinian as an object of FGModuleCat.

theorem CategoryTheory.Triangulated.AlgebraicWitness.fgModuleCat_simple_iff_finrank_eq_one (k : Type u) [Field k] (V : FGModuleCat k) : Simple V ↔ Module.finrank k ↑V = 1

A finite-dimensional vector space is a simple categorical object exactly when it has dimension one.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.AlgebraicWitness.DerivedFiniteVect (k : Type u) [Field k] : Type (u + 1)

The concrete proper triangulated category used by the witness.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.DerivedFiniteVect k = DerivedCategory.Bounded (FGModuleCat k)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.AlgebraicWitness.standardT (k : Type u) [Field k] : TStructure (DerivedFiniteVect k)

The standard bounded t-structure on Dᵇ(FGModuleCat k).

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.standardT k = DerivedCategory.TStructure.t.onBounded

@[reducible, inline]

noncomputable abbrev CategoryTheory.Triangulated.AlgebraicWitness.residueObject (k : Type u) [Field k] : DerivedFiniteVect k

The one-dimensional vector space, placed in cohomological degree zero.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.residueObject k = (DerivedCategory.boundedSingleFunctor (FGModuleCat k)).obj (FGModuleCat.of k k)

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardT_isBounded (k : Type u) [Field k] : (standardT k).IsBounded

Every bounded-derived object is bounded for the induced standard t-structure.

theorem CategoryTheory.Triangulated.AlgebraicWitness.boundedQh_essImage_le_bounded (k : Type u) [Field k] : (boundedQh k).essImage ≤ DerivedCategory.TStructure.t.bounded

The essential image of honest bounded complexes lies in the canonical bounded derived category.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded (k : Type u) [Field k] : Functor (boundedQh k).essImage.FullSubcategory (DerivedFiniteVect k)

The fully faithful restriction from the derived essential image to the canonical bounded derived category.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded k = DerivedCategory.TStructure.t.bounded.lift (CategoryTheory.Triangulated.boundedQh k).essImage.ι ⋯

instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded_additive (k : Type u) [Field k] : (boundedImageToBounded k).Additive

instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded_linear (k : Type u) [Field k] : Functor.Linear k (boundedImageToBounded k)

instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded_full (k : Type u) [Field k] : (boundedImageToBounded k).Full

instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded_faithful (k : Type u) [Field k] : (boundedImageToBounded k).Faithful

@[implicit_reducible]

noncomputable instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBoundedCommShift (k : Type u) [Field k] : (boundedImageToBounded k).CommShift ℤ

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBoundedCommShift k = id inferInstance

instance CategoryTheory.Triangulated.AlgebraicWitness.boundedImageToBounded_essSurj (k : Type u) [Field k] : (boundedImageToBounded k).EssSurj

Every canonically bounded derived object is represented by an honest bounded complex.

instance CategoryTheory.Triangulated.AlgebraicWitness.homFiniteBounded_derivedFiniteVect (k : Type u) [Field k] : HomFiniteBounded k (DerivedFiniteVect k)

The canonical bounded derived category of finite-dimensional vector spaces is Hom-finite with finite shift amplitude.

instance CategoryTheory.Triangulated.AlgebraicWitness.homFinite_derivedFiniteVect (k : Type u) [Field k] : SerreFunctor.HomFinite k (DerivedFiniteVect k)

Properness also supplies ordinary (unshifted) Hom-finiteness.

theorem CategoryTheory.Triangulated.AlgebraicWitness.subsingleton_residue_shiftedHom_of_ne_zero (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) (i : ℤ) (hi : i ≠ 0) : Subsingleton (residueObject k ⟶ (shiftFunctor (DerivedFiniteVect k) i).obj E)

From the degree-zero residue object to an object of the standard heart, all nonzero shifted Hom spaces vanish. Positive shifts vanish because every finite-dimensional vector space is projective; negative shifts vanish by the standard t-structure.

theorem CategoryTheory.Triangulated.AlgebraicWitness.chiHom_residue_eq_finrank (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) : chiHom k (DerivedFiniteVect k) (residueObject k) E = ↑(Module.finrank k (residueObject k ⟶ E))

On the standard heart, the Euler pairing with the residue object is the ordinary dimension of the degree-zero Hom space.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.centralCharge (k : Type u) [Field k] : K₀ (DerivedFiniteVect k) →+ ℂ

The honest central charge of the witness: minus the Euler pairing with the degree-zero copy of the ground field.

Equations

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

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.residueHomEquiv (k : Type u) [Field k] (Y : FGModuleCat k) : (residueObject k ⟶ (DerivedCategory.boundedSingleFunctor (FGModuleCat k)).obj Y) ≃ₗ[k] ↑Y

A morphism from the residue object to a degree-zero vector space is the same thing as a vector in that space.

Equations

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

theorem CategoryTheory.Triangulated.AlgebraicWitness.finrank_residueHom_pos (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) (hE₀ : ¬Limits.IsZero E) : 0 < Module.finrank k (residueObject k ⟶ E)

A nonzero object of the standard heart receives a genuinely negative, rather than merely nonpositive, charge.

theorem CategoryTheory.Triangulated.AlgebraicWitness.centralCharge_of_heart (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) : (centralCharge k) (K₀.of (DerivedFiniteVect k) E) = -↑↑(Module.finrank k (residueObject k ⟶ E))

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityFunction (k : Type u) [Field k] : WeakStabilityCondition.StabilityFunction (standardT k)

The standard stability function: every nonzero heart object lies on the negative real axis.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityFunction k = { Z := CategoryTheory.Triangulated.AlgebraicWitness.centralCharge k, nonzero_mem := ⋯ }

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.standardWeakStabilityFunction (k : Type u) [Field k] : WeakStabilityCondition.WeakStabilityFunction (standardT k)

The weak stability function used by the heart-to-slicing construction.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.standardWeakStabilityFunction k = (CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityFunction k).toWeak

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardWeak_slope_eq_top (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) : (standardWeakStabilityFunction k).slope E = ⊤

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardWeak_isSemistable (k : Type u) [Field k] (E : DerivedFiniteVect k) (hE : (standardT k).heart E) : (standardWeakStabilityFunction k).IsSemistable E

Since all nonzero heart objects have the same phase, every heart object is weak-semistable.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardWeak_hasHNProperty (k : Type u) [Field k] : (standardWeakStabilityFunction k).HasHNProperty

The standard weak stability function has one-step HN filtrations.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardWeak_ambientHN (k : Type u) [Field k] (E : DerivedFiniteVect k) : Nonempty (HNFiltration (DerivedFiniteVect k) (standardWeakStabilityFunction k).ambientPhasePredicate E)

Ambient HN existence follows from boundedness of the standard t-structure.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing (k : Type u) [Field k] : Slicing (DerivedFiniteVect k)

The slicing reconstructed from the constant-phase standard heart.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing k = ⋯.toSlicing

theorem CategoryTheory.Triangulated.AlgebraicWitness.centralCharge_ne_zero_of_ambientPhasePredicate (k : Type u) [Field k] (phi : ℝ) (E : DerivedFiniteVect k) (hP : (standardWeakStabilityFunction k).ambientPhasePredicate phi E) (hE₀ : ¬Limits.IsZero E) : (centralCharge k) (K₀.of (DerivedFiniteVect k) E) ≠ 0

The Euler charge cannot vanish on a nonzero object in one of the reconstructed slices.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.standardPreStabilityCondition (k : Type u) [Field k] : PreStabilityCondition (DerivedFiniteVect k)

The ordinary pre-stability condition underlying the algebraic witness.

Equations

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

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing_phase_integer (k : Type u) [Field k] {phi : ℝ} {E : DerivedFiniteVect k} (hP : (standardSlicing k).P phi E) (hE₀ : ¬Limits.IsZero E) : ∃ (n : ℤ), phi = ↑n

Nonzero semistable objects in the standard slicing occur only at integral phases.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardDualHeart_heart_iff (k : Type u) [Field k] (r : ℝ) (E : DerivedFiniteVect k) : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) r)).heart E ↔ (standardSlicing k).P (↑⌈r⌉) E

Every half-open unit heart of the discrete standard slicing is exactly the slice at the unique integral phase it contains.

theorem CategoryTheory.Triangulated.AlgebraicWitness.phaseBase_int (q : ℤ) : WeakStabilityCondition.phaseBase ↑q = 1

The normalized representative of an integral phase is the endpoint 1 of the standard half-open interval.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing_mem_integer_iff (k : Type u) [Field k] (q : ℤ) (E : DerivedFiniteVect k) : (standardSlicing k).P (↑q) E ↔ (standardT k).heart ((shiftFunctor (DerivedFiniteVect k) (-WeakStabilityCondition.phaseIndex ↑q)).obj E)

At an integral phase, membership in the standard slice is exactly membership in the standard heart after the normalizing shift.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardCanonicalHeart_heart_iff (k : Type u) [Field k] (E : DerivedFiniteVect k) : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart E ↔ (standardSlicing k).P 1 E

The canonical heart of the reconstructed discrete slicing is its unique slice in (0, 1], namely phase one.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.dualHeartToStandardEquivalence (k : Type u) [Field k] (r : ℝ) : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) r)).heart.FullSubcategory ≌ (standardT k).heart.FullSubcategory

Shifting by the normalizing degree identifies every half-open unit heart with the standard bounded heart.

Equations

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

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.dualHeartEquivalence (k : Type u) [Field k] (r : ℝ) : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) r)).heart.FullSubcategory ≌ FGModuleCat k

Every half-open unit heart of the standard slicing is equivalent to finite-dimensional vector spaces.

Equations

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

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.canonicalHeartEquivalence (k : Type u) [Field k] : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart.FullSubcategory ≌ FGModuleCat k

The canonical slicing heart is equivalent to finite-dimensional vector spaces.

Equations

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

theorem CategoryTheory.Triangulated.AlgebraicWitness.dualHeart_isStableAt_iff_simple (k : Type u) [Field k] (q : ℤ) (E : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) ↑q)).heart.FullSubcategory) : (standardSlicing k).IsStableAt (↑q) E.obj ↔ Simple E

In an integral half-open heart, whose every object has one phase, stability is exactly categorical simplicity.

theorem CategoryTheory.Triangulated.AlgebraicWitness.dualHeart_isArtinianObject (k : Type u) [Field k] (r : ℝ) (E : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) r)).heart.FullSubcategory) : IsArtinianObject E

Objects of every half-open unit heart of the standard slicing are Artinian.

theorem CategoryTheory.Triangulated.AlgebraicWitness.dualHeart_isNoetherianObject (k : Type u) [Field k] (r : ℝ) (E : (Slicing.toDualTStructure (DerivedFiniteVect k) (Slicing.phaseShift (DerivedFiniteVect k) (standardSlicing k) r)).heart.FullSubcategory) : IsNoetherianObject E

Objects of every half-open unit heart of the standard slicing are Noetherian.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing_isLocallyFinite (k : Type u) [Field k] : Slicing.IsLocallyFinite (DerivedFiniteVect k) (standardSlicing k)

The discrete standard slicing is locally finite.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition (k : Type u) [Field k] : StabilityCondition (DerivedFiniteVect k)

The genuine locally finite stability condition carried by the standard heart of finite-dimensional vector spaces.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition k = { toWithClassMap := CategoryTheory.Triangulated.AlgebraicWitness.standardPreStabilityCondition k, locallyFinite := ⋯ }

theorem CategoryTheory.Triangulated.AlgebraicWitness.canonicalHeart_isArtinianObject (k : Type u) [Field k] (E : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart.FullSubcategory) : IsArtinianObject E

Objects of the canonical slicing heart are Artinian.

theorem CategoryTheory.Triangulated.AlgebraicWitness.canonicalHeart_isNoetherianObject (k : Type u) [Field k] (E : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart.FullSubcategory) : IsNoetherianObject E

Objects of the canonical slicing heart are Noetherian.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.simpleHeartObject (k : Type u) [Field k] : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart.FullSubcategory

The unique simple object of the canonical heart, transported from the one-dimensional vector space.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.simpleHeartObject k = (CategoryTheory.Triangulated.AlgebraicWitness.canonicalHeartEquivalence k).inverse.obj (FGModuleCat.of k k)

theorem CategoryTheory.Triangulated.AlgebraicWitness.simpleHeartObject_simple (k : Type u) [Field k] : Simple (simpleHeartObject k)

The distinguished one-dimensional object of the canonical heart is simple.

theorem CategoryTheory.Triangulated.AlgebraicWitness.canonicalHeart_simple_iso (k : Type u) [Field k] (T : (Slicing.toTStructure (DerivedFiniteVect k) (standardSlicing k)).heart.FullSubcategory) (hT : Simple T) : Nonempty (T ≅ simpleHeartObject k)

Every simple object of the canonical heart is isomorphic to the distinguished one-dimensional object.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition_hasFiniteLengthHeart (k : Type u) [Field k] : StabilityCondition.WithClassMap.HasFiniteLengthHeart (standardStabilityCondition k)

The canonical heart of the standard stability condition has finite length and exactly one simple isomorphism class.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardHeart_simple_iso_residue (k : Type u) [Field k] (H : (standardT k).heart.FullSubcategory) (hH : Simple H) : Nonempty (H.obj ≅ residueObject k)

A simple object of the standard bounded heart is isomorphic, in the ambient derived category, to the degree-zero one-dimensional vector space.

noncomputable def CategoryTheory.Triangulated.AlgebraicWitness.stableRepresentative (k : Type u) [Field k] : DerivedFiniteVect k

A fixed stable representative, obtained by transporting the one-dimensional vector space into the phase-one half-open heart.

Equations

• CategoryTheory.Triangulated.AlgebraicWitness.stableRepresentative k = ((CategoryTheory.Triangulated.AlgebraicWitness.dualHeartEquivalence k ↑1).inverse.obj (FGModuleCat.of k k)).obj

theorem CategoryTheory.Triangulated.AlgebraicWitness.stableRepresentative_isStable (k : Type u) [Field k] : (standardSlicing k).IsStableAt 1 (stableRepresentative k)

The fixed representative is genuinely stable at phase one.

theorem CategoryTheory.Triangulated.AlgebraicWitness.stable_iso_residue_shift (k : Type u) [Field k] {phi : ℝ} {F : DerivedFiniteVect k} (hF : (standardSlicing k).IsStableAt phi F) : ∃ (q : ℤ), phi = ↑q ∧ Nonempty (F ≅ (shiftFunctor (DerivedFiniteVect k) (WeakStabilityCondition.phaseIndex ↑q)).obj (residueObject k))

Every stable object is a shift of the degree-zero one-dimensional vector space, with the normalizing shift made explicit.

theorem CategoryTheory.Triangulated.AlgebraicWitness.phaseIndex_int_eq (q : ℤ) : WeakStabilityCondition.phaseIndex ↑q = q - 1

The phase index of an integral phase is the preceding integer.

theorem CategoryTheory.Triangulated.AlgebraicWitness.stableRepresentative_iso_residue (k : Type u) [Field k] : Nonempty (stableRepresentative k ≅ residueObject k)

The fixed stable representative is isomorphic to the degree-zero residue object.

theorem CategoryTheory.Triangulated.AlgebraicWitness.stable_iso_representative_shift (k : Type u) [Field k] {phi : ℝ} {F : DerivedFiniteVect k} (hF : (standardSlicing k).IsStableAt phi F) : ∃ (m : ℤ), Nonempty (F ≅ (shiftFunctor (DerivedFiniteVect k) m).obj (stableRepresentative k))

Stable objects in the standard slicing form one shift orbit.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardSlicing_hasJordanHolderFiltrations (k : Type u) [Field k] : (standardSlicing k).HasJordanHolderFiltrations

The locally finite standard slicing has Jordan--Hölder filtrations.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition_hasFiniteStableOrbits (k : Type u) [Field k] : StabilityCondition.WithClassMap.HasFiniteStableOrbits (standardStabilityCondition k)

The standard stability condition has exactly one stable shift orbit.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition_isAlgebraic (k : Type u) [Field k] : StabilityCondition.WithClassMap.IsAlgebraic (standardStabilityCondition k)

The standard stability condition on Dᵇ(FGModuleCat k) is algebraic.

theorem CategoryTheory.Triangulated.AlgebraicWitness.standardStabilityCondition_hasGlobalMassHomBound (k : Type u) [Field k] : StabilityCondition.WithClassMap.HasGlobalMassHomBound (standardStabilityCondition k)

The abstract algebraic theorem therefore gives a genuine global mass--Hom bound on this nonzero example.

theorem CategoryTheory.Triangulated.AlgebraicWitness.centralCharge_residue (k : Type u) [Field k] : (centralCharge k) (K₀.of (DerivedFiniteVect k) (residueObject k)) = -1

The witness charge takes the value -1 on the residue class.

theorem CategoryTheory.Triangulated.AlgebraicWitness.centralCharge_ne_zero (k : Type u) [Field k] : centralCharge k ≠ 0

In particular, the central charge of the algebraic witness is nonzero.