The divisorial charge is the exponential kernel

CentralCharge/Exponential/Kernel.lean states the exponential charge once, indexed by truncation degree, and CentralCharge/Exponential/Comparison.lean proves the two compressed H-degree families are it. Those families are Picard rank one. This file does the case that actually decides whether the kernel is worth having: the divisorial charge of CentralCharge/Divisorial/Charge.lean, which takes two independent classes B and omega in the full real divisor space.

Why this is the keystone

The compressed families reach the kernel through a vector of H-degrees. The divisorial charge cannot: the H-compression is not injective once the Picard rank exceeds one, so there is no degree vector to hand it. If the kernel could only be reached that way it would cover the rank-one slice and nothing else, and the unification would be cosmetic.

It is reached instead by keeping the same polynomial and replacing the degree functional with the intersection form. The moments become

mu 0 = ch2(E),   mu 1 = <w, ch1(E)>,   mu 2 = <w, w> * rk(E)

with w = B + i*omega, and Exp.ofMoments 2 of those is the divisorial charge on the nose. That is why ofMoments takes a moment sequence rather than a vector of degrees: the two sources of moments are siblings under it, and neither is a specialization of the other.

Two of the three independent designs of this tree concluded the multi-divisor charge was a sibling that is not a child. They were wrong, and this file is the proof.

Stated on the triple

The keystone is proved on a bare Mukai.RealExtension D, not on a ChernCharacter. That is load-bearing rather than stylistic: mukaiCharge (CentralCharge/Divisorial/Mukai.lean) is the same expCharge on a different triple, so a ChernCharacter-level statement could not reach it, and the correction class the next slice inhabits is exactly that difference. The ChernCharacter forms below follow by toRealExtension.

centralCharge_eq_expCharge is the other half and was not previously recorded: the divisorial charge and Bridgeland's Z(beta, omega) are the same function, not two functions that agree in the cases anyone checked.

What is not here

No correction class, no walls, no tilting. kappa arrives with the polarised transport, where it belongs, because it is a pullback and not a coefficient.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChargeCoordinates.twistByScalar_eq_exp {N : Type u_2} [AddCommGroup N] (D : ChargeCoordinates N) (β : ℝ) (E : N) : ![(D.twistByScalar β).hyperplaneSquare * (D.twistByScalar β).rank E, (D.twistByScalar β).degree E, (D.twistByScalar β).chTwo E] = Exp.twist 2 β ![D.hyperplaneSquare * D.rank E, D.degree E, D.chTwo E]

Scalar twisting commutes with the weighted surface degree presentation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.twist_rankOne_eq_exp {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (β : ℝ) (E : N) : ![S.pair H H * (ch.twist S (β • H)).rank E, S.pair H ((ch.twist S (β • H)).chOne E), (ch.twist S (β • H)).chTwo E] = Exp.twist 2 β ![S.pair H H * ch.rank E, S.pair H (ch.chOne E), ch.chTwo E]

Along B = βH, twisting in the full divisor space commutes with compression. For an arbitrary B, the compressed degrees do not determine the twist.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.cPair {D : Type u_1} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (P : StabilityParameters D) (x : D) : ℂ

<w, x> for w = B + i*omega, as a complex number.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.cPair S P x = ↑(S.pair P.B x) + ↑(S.pair P.omega x) * Complex.I

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.cSelf {D : Type u_1} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (P : StabilityParameters D) : ℂ

<w, w> for w = B + i*omega. The imaginary part carries the factor of two from the cross term.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.cSelf S P = ↑(S.pair P.B P.B - S.pair P.omega P.omega) + ↑(2 * S.pair P.omega P.B) * Complex.I

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.tripleMoments {D : Type u_1} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (P : StabilityParameters D) (v : Mukai.RealExtension D) : ℕ → ℂ

The divisorial moments of an arbitrary Mukai triple (r, c, s): mu 0 = s, mu 1 = <w, c>, mu 2 = <w, w> * r, and zero above.

These are the moments of Exp.ofMoments with the intersection form in place of the degree functional, which is the whole content of the unification.

Equations

• One or more equations did not get rendered due to their size.
• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.tripleMoments S P v 0 = ↑v.2.2
• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.tripleMoments S P v n.succ.succ.succ = 0

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.expCharge_eq_ofMoments {D : Type u_1} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (P : StabilityParameters D) (v : Mukai.RealExtension D) : Mukai.expCharge S.intersection P.B P.omega v = Exp.ofMoments 2 (tripleMoments S P v)

The keystone. Bridgeland's Z(beta, omega) on a Mukai triple is the exponential kernel at truncation degree two.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.expCharge_rankOne_eq_charge {D : Type u_1} [AddCommGroup D] [Module ℝ D] (S : DivisorSpace D) (H : D) (a b : ℝ) (v : Mukai.RealExtension D) : Mukai.expCharge S.intersection (StabilityParameters.rankOne H a b).B (StabilityParameters.rankOne H a b).omega v = (Exp.charge 2 (Exp.alphaBetaChart (a, b))) ![S.pair H H * v.1, S.pair H v.2.1, v.2.2]

The rank-one collapse. On B = b*H, omega = a*H the intersection-form charge of any triple is the scalar kernel on the compressed degrees (H^2 * r, H * c, s), which is how the divisorial branch and the compressed branch meet.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.centralCharge_eq_expCharge {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.centralCharge S P) E = Mukai.expCharge S.intersection P.B P.omega (ch.toRealExtension E)

The divisorial charge is Z(beta, omega) on the Mukai triple of the Chern character. Both sides were already in the tree; that they are one function was not recorded.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.centralCharge_eq_ofMoments {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.centralCharge S P) E = Exp.ofMoments 2 (tripleMoments S P (ch.toRealExtension E))

The keystone in ChernCharacter form, by toRealExtension.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.moments {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : ℕ → ℂ

The divisorial moments of a Chern character: the triple moments of its Mukai triple.

Equations

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

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.moments_apply {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : moments ch S P E = tripleMoments S P (ch.toRealExtension E)

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.moments_rankOne {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (a b : ℝ) (E : N) : moments ch S (StabilityParameters.rankOne H a b) E = Exp.moments 2 (Exp.alphaBetaChart (a, b)) ![S.pair H H * ch.rank E, S.pair H (ch.chOne E), ch.chTwo E]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.centralCharge_rankOne_eq_charge {D : Type u_1} [AddCommGroup D] [Module ℝ D] {N : Type u_2} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (a b : ℝ) (E : N) : (ch.centralCharge S (StabilityParameters.rankOne H a b)) E = (Exp.charge 2 (Exp.alphaBetaChart (a, b))) ![S.pair H H * ch.rank E, S.pair H (ch.chOne E), ch.chTwo E]

The rank-one collapse in ChernCharacter form.