Documentation

DerivedAlgGeo.CategoryTheory.Triangulated.StabilityCondition.Weak

Weak stability conditions #

The dependency parent for Bridgeland stability: weak central charges, Harder--Narasimhan theory, support, and tilting. It is the child Weak/ of StabilityCondition/, the way PseudoMetricSpace is MetricSpace/Pseudo/ in Mathlib: the directory is named for the canonical concept and the weakened variant by its adjective, while the dependency runs the other way. Nothing below Weak/ imports the Bridgeland theory, and this umbrella is importable without it. Declaration namespaces remain CategoryTheory.Triangulated.WeakStabilityCondition.

The abelian half of the theory is not here. Stability functions on an abelian category, their Harder--Narasimhan filtrations, and the ClassDatum the charge condition is stated over are owned by CategoryTheory/Abelian/Stability/ since MO1.08 (#1319); Weak/Foundation.lean consumes that owner and re-exports it, so this umbrella still offers the same names. What remains below Weak/ is the triangulated theory: slicings, the heart adapter, support, tilting and the families.