Charges on the free lattice of simples

Bridgeland's worked example (§5) says that for an abelian category A of finite length with n simple objects, a stability function on A is exactly a choice of Z(Sᵢ) in the semi-closed upper half plane, one for each simple — so that component of the stability manifold is ℍ̄ⁿ.

This file formalizes the lattice half of that statement, and only that.

What is proved, and what it is a statement about

The carrier is Fin n → ℤ, exactly as LinearAlgebra/Lattice/Numerical.lean uses Fin 2 → ℤ. It is not K₀(A). Identifying the two is the Jordan–Hölder theorem for a finite-length abelian category — that K₀(A) is free abelian on the classes of the simples — and:

• Mathlib does not have it. There is no Jordan–Hölder or composition series for abelian categories at the pin; Mathlib/Order/JordanHolder.lean is about modular lattices and is not connected to K₀ of a category.
• This repository does not have it either. CategoryTheory/Triangulated/GrothendieckGroup/ builds K₀ as a quotient of a free abelian group by a relation subgroup, and nothing there or anywhere else in the library says that quotient is free on the simples.

So the identification is an unrealized assumption, exactly like the one LinearAlgebra/Lattice/Numerical.lean records, and it is never discharged here. Every theorem below is a theorem about Fin n → ℤ and would hold if no abelian category existed.

Relation to the stability-function foundation

semiClosedUpperHalfPlane and its basic API are defined in Abelian/Stability/Charge.lean. What that module does not carry, and what is added here, is closure under positive scaling and closure under a nonempty finite sum — the two facts a positive-integer combination of simple charges needs.

Those two live in this file's own namespace rather than extending the foundation module's, because nothing else needs to find them by dot notation and the foundation module is the one every stability-function consumer imports.

Main results

• mem_cone_sum — a nonempty finite sum of cone elements is in the cone.
• mem_cone_natCombination — the key one: if every simple charge is in the cone, so is every nonzero ℕ-combination of them.
• existsUnique_charge — the parametrization. Charges of the simples are exactly the additive maps out of the lattice, freely and uniquely.

Two closure properties the stability-function foundation does not carry

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.mem_cone_smul {r : ℝ} (hr : 0 < r) {z : ℂ} (hz : z ∈ semiClosedUpperHalfPlane) : ↑r * z ∈ semiClosedUpperHalfPlane

The cone is closed under multiplication by a positive real.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.mem_cone_sum {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {f : ι → ℂ} (hf : ∀ i ∈ s, f i ∈ semiClosedUpperHalfPlane) : ∑ i ∈ s, f i ∈ semiClosedUpperHalfPlane

The cone is closed under nonempty finite sums.

The lattice model

Fin n → ℤ stands in for K₀(A); see the module docstring for why that is a model and not an identification.

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf {n : ℕ} (w : Fin n → ℂ) : (Fin n → ℤ) →+ ℂ

The additive charge determined by a choice of charge for each simple.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf w = { toFun := fun (m : Fin n → ℤ) => ∑ i : Fin n, ↑(m i) * w i, map_zero' := ⋯, map_add' := ⋯ }

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf_apply {n : ℕ} (w : Fin n → ℂ) (m : Fin n → ℤ) : (chargeOf w) m = ∑ i : Fin n, ↑(m i) * w i

Not @[simp]: it would rewrite the left-hand side of chargeOf_single into a sum before that lemma could fire, and simpNF rejects the pair. It is the unfolding lemma, used by explicit rw.

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf_single {n : ℕ} (w : Fin n → ℂ) (i : Fin n) : (chargeOf w) (Pi.single i 1) = w i

The charge of the i-th basis vector is the i-th chosen value: the lattice-model form of "Z restricted to the simples is the chosen data".

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.eq_chargeOf {n : ℕ} (Z : (Fin n → ℤ) →+ ℂ) : Z = chargeOf fun (i : Fin n) => Z (Pi.single i 1)

Every additive map out of the lattice is the charge of its values on the basis. This is the surjectivity half of the parametrization.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.existsUnique_charge {n : ℕ} (w : Fin n → ℂ) : ∃! Z : (Fin n → ℤ) →+ ℂ, ∀ (i : Fin n), Z (Pi.single i 1) = w i

The parametrization. A choice of charge for each simple determines a unique additive charge on the lattice, and every additive charge arises this way. This is the lattice-model form of Bridgeland's ℍ̄ⁿ count; the half-plane constraint is imposed separately by mem_cone_natCombination.

The half-plane constraint

The content of "any choice of charges in ℍ̄ gives a stability function" is that the cone absorbs positive integer combinations. On the lattice side that is the following statement, and it is the whole of it.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.mem_cone_natCombination {n : ℕ} {w : Fin n → ℂ} (hw : ∀ (i : Fin n), w i ∈ semiClosedUpperHalfPlane) {m : Fin n → ℕ} (hm : m ≠ 0) : ∑ i : Fin n, ↑(m i) * w i ∈ semiClosedUpperHalfPlane

If every simple charge lies in the cone, so does every nonzero ℕ-combination of them.

In the intended reading m i is the multiplicity of the i-th simple in a Jordan–Hölder filtration, so this says a nonzero object has charge in the half plane. That reading is not formalized — see the module docstring.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf_mem_cone {n : ℕ} {w : Fin n → ℂ} (hw : ∀ (i : Fin n), w i ∈ semiClosedUpperHalfPlane) {m : Fin n → ℕ} (hm : m ≠ 0) : ((chargeOf w) fun (i : Fin n) => ↑(m i)) ∈ semiClosedUpperHalfPlane

The ℕ-combination statement in the form the parametrization produces.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.FiniteLength.chargeOf_ne_zero {n : ℕ} {w : Fin n → ℂ} (hw : ∀ (i : Fin n), w i ∈ semiClosedUpperHalfPlane) {m : Fin n → ℕ} (hm : m ≠ 0) : ((chargeOf w) fun (i : Fin n) => ↑(m i)) ≠ 0

A nonzero ℕ-combination of cone elements is nonzero. The lattice-model form of "a nonzero object has nonzero charge", which is what makes the phase well defined.