The threefold central charge in the (α, β) half plane

This file owns the four-coordinate numerical class, its β-twist, and the Bayer--Macrì--Toda central charge. It deliberately stops before wall equations and wall-specific numerical quantities.

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass : Type

A numerical class of a polarised threefold, compressed to its four H-degrees (∫H³ch₀, ∫H²ch₁, ∫H·ch₂, ∫ch₃).

A quadruple of reals. It is not ch(E) for a sheaf E, and the first slot is weighted by ∫H³; see the module docstring.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass = (ℝ × ℝ × ℝ × ℝ)

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass.deg0 (v : NumClass) : ℝ

The weighted rank coordinate, standing for ∫H³·ch₀.

Equations

• v.deg0 = v.1

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass.deg1 (v : NumClass) : ℝ

The coordinate standing for ∫H²·ch₁.

Equations

• v.deg1 = v.2.1

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass.deg2 (v : NumClass) : ℝ

The coordinate standing for ∫H·ch₂.

Equations

• v.deg2 = v.2.2.1

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass.deg3 (v : NumClass) : ℝ

The coordinate standing for ∫ch₃.

Equations

• v.deg3 = v.2.2.2

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.threefoldVec : Threefold.NumClass ≃+ Exp.HDeg 3

The threefold tuple and the kernel's compressed degrees hold the same four reals. Slot 0 is the weighted rank ∫H³·ch₀ on both sides.

Equations

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

The β-twist on compressed coordinates

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist (β : ℝ) (v : NumClass) : NumClass

The compressed β-twist: the four H-degrees of ch^{βH} = e^{-βH}ch.

deg0 is fixed, because the twist sums over j ≤ 0 in codimension zero.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_deg0 (β : ℝ) (v : NumClass) : (betaTwist β v).deg0 = v.deg0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_deg1 (β : ℝ) (v : NumClass) : (betaTwist β v).deg1 = v.deg1 - β * v.deg0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_deg2 (β : ℝ) (v : NumClass) : (betaTwist β v).deg2 = v.deg2 - β * v.deg1 + β ^ 2 / 2 * v.deg0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_deg3 (β : ℝ) (v : NumClass) : (betaTwist β v).deg3 = v.deg3 - β * v.deg2 + β ^ 2 / 2 * v.deg1 - β ^ 3 / 6 * v.deg0

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_zero (v : NumClass) : betaTwist 0 v = v

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_eq_exp (β : ℝ) (v : NumClass) : threefoldVec (betaTwist β v) = Exp.twist 3 β (threefoldVec v)

The four-coordinate twist is the exponential kernel's action at degree three.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist_betaTwist (β₁ β₂ : ℝ) (v : NumClass) : betaTwist β₁ (betaTwist β₂ v) = betaTwist (β₁ + β₂) v

The group law: twisting by β₁ + β₂ is twisting by β₂ and then by β₁. This is e^{-(β₁+β₂)H} = e^{-β₁H}e^{-β₂H} on the four degrees, and it is what makes the name betaTwist honest.

The charge

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.reZ (α β : ℝ) (v : NumClass) : ℝ

The real part of the threefold charge at (α, β).

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.reZ α β v = -v.deg3 + β * v.deg2 - (β ^ 2 - α ^ 2) / 2 * v.deg1 + (β ^ 3 - 3 * β * α ^ 2) / 6 * v.deg0

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.imZ (α β : ℝ) (v : NumClass) : ℝ

The imaginary part of the threefold charge at (α, β).

The outer factor of α is the one the expansion of -∫exp(-(β+iα)H)ch produces. Some presentations divide it out; alignmentValue is unchanged by that, because dropping it rescales the imaginary part by α > 0 and alignmentValue_div_alpha records the resulting proportionality.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.imZ α β v = α * (v.deg2 - β * v.deg1 + (3 * β ^ 2 - α ^ 2) / 6 * v.deg0)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.reZ_eq_betaTwist (α β : ℝ) (v : NumClass) : reZ α β v = reZ α 0 (betaTwist β v)

β is a twist, not a coordinate: the charge at (α, β) is the charge at (α, 0) of the β-twisted class. This is the consistency check that ties the two polynomials to the exponential they came from.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.imZ_eq_betaTwist (α β : ℝ) (v : NumClass) : imZ α β v = imZ α 0 (betaTwist β v)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge (α β : ℝ) : NumClass →+ ℂ

The complex charge whose real and imaginary parts are reZ and imZ.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge_re (α β : ℝ) (v : NumClass) : ((charge α β) v).re = reZ α β v

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge_im (α β : ℝ) (v : NumClass) : ((charge α β) v).im = imZ α β v

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.chargeFamily : ChargeFamily (ℝ × ℝ) NumClass

The threefold charge family, a child of the dimension-independent charge root. Its parameter space is the whole (α, β) plane: positivity α > 0 stays attached to the statements that need it, exactly as in the surface child.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.chargeFamily_charge (p : ℝ × ℝ) (v : NumClass) : (chargeFamily.charge p) v = (charge p.1 p.2) v