Divisorial surface charges over a real Neron--Severi space

The intrinsic parameters of a divisorial stability condition on a surface are two independent real divisor classes: a B-field and an ample class omega. They are not, in general, scalar multiples of one chosen generator. This file therefore keeps the following data in separate, composable layers:

• DivisorSpace, from the neutral Hodge-index module, supplies the real vector space and its symmetric pairing;
• ChernCharacter supplies additive maps rank, chOne, and chTwo;
• StabilityParameters supplies independent classes B and omega;
• DivisorialParameters optionally records membership of omega in a geometry-specific ample cone.

The charge is

`Z_(omega,B)(E) = -chTwo^B(E) + omega^2 rank(E) / 2

• i (omega . chOne^B(E))`.

Equivalently, it is the Mukai pairing of ch(E) with the real and imaginary parts of exp(B + i omega). The implementation reuses the repository's real Mukai extension for this comparison, but does not assume that the numerical class is a Mukai vector. Here its third component is genuinely chTwo. A K3-specific charge uses the Todd-corrected third Mukai component and therefore requires a separate, explicitly named adapter rather than overloading this structure.

Rank-one families such as B = beta H, omega = alpha H, and orthogonal slices such as B = s H + u G, omega = t H are constructors downstream of the intrinsic definition. They are deliberately not fields of the core data.

This file contains only numerical arithmetic. It does not construct the tilted heart, prove ampleness, or establish the support property.

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter (N : Type v) (D : Type u) [AddCommGroup N] [AddCommGroup D] [Module ℝ D] : Type (max u v)

Additive Chern-character coordinates with an uncompressed first Chern class in the full real divisor space.

• rank : N →+ ℝ

  The rank coordinate.

• chOne : N →+ D

  The full first Chern-character coordinate in N^1(X)_R.

• chTwo : N →+ ℝ

  The integrated second Chern-character coordinate.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.toRealExtension {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) : N →+ Mukai.RealExtension D

The Chern-character triple as an element of the real Mukai extension.

This is an additive packaging device; it does not assert that ch is the Todd-corrected Mukai vector.

Equations

• ch.toRealExtension = { toFun := fun (E : N) => (ch.rank E, ch.chOne E, ch.chTwo E), map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.toRealExtension_apply {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (E : N) : ch.toRealExtension E = (ch.rank E, ch.chOne E, ch.chTwo E)

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.twist {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (B : D) : ChernCharacter N D

Twist by an arbitrary real divisor class B.

On a surface this is the degree-at-most-two expansion of ch^B = exp(-B) ch.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.twist_rank {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (B : D) (E : N) : (ch.twist S B).rank E = ch.rank E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.twist_chOne {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (B : D) (E : N) : (ch.twist S B).chOne E = ch.chOne E - ch.rank E • B

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.twist_chTwo {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (B : D) (E : N) : (ch.twist S B).chTwo E = ch.chTwo E - S.pair B (ch.chOne E) + S.pair B B * ch.rank E / 2

Maps between presentations of the same surface character

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.Pullback {D : Type u} [AddCommGroup D] [Module ℝ D] {L : Type u_1} {M : Type u_2} [AddCommGroup L] [AddCommGroup M] (source : ChernCharacter L D) (target : ChernCharacter M D) : Type (max u_1 u_2)

An additive map preserving the full Chern-character coordinates.

Unlike ChargeCoordinates.Pullback, this comparison happens before choosing B and omega, so one witness transports every divisorial central charge on the fixed divisor space.

• map : L →+ M

  The map between numerical class carriers.

• rank_eq (E : L) : source.rank E = target.rank (self.map E)

  Preservation of rank.

• chOne_eq (E : L) : source.chOne E = target.chOne (self.map E)

  Preservation of the full first Chern class.

• chTwo_eq (E : L) : source.chTwo E = target.chTwo (self.map E)

  Preservation of the integrated second Chern character.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.Pullback.twist {D : Type u} [AddCommGroup D] [Module ℝ D] {L : Type u_1} {M : Type u_2} [AddCommGroup L] [AddCommGroup M] {source : ChernCharacter L D} {target : ChernCharacter M D} (h : source.Pullback target) (S : DivisorSpace D) (B : D) : (source.twist S B).Pullback (target.twist S B)

A full-character comparison remains valid after twisting by any real B-field.

Equations

• h.twist S B = { map := h.map, rank_eq := ⋯, chOne_eq := ⋯, chTwo_eq := ⋯ }

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters (D : Type u) : Type u

The two independent divisor-class parameters used by the central charge.

The arithmetic definition does not need a positivity proof. Consumers that construct geometric stability conditions should use DivisorialParameters to attach their chosen ample-cone predicate.

• B : D

  The real B-field.

• omega : D

  The real ample class, including any desired volume scaling.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters.rankOne {D : Type u} [AddCommGroup D] [Module ℝ D] (H : D) (alpha beta : ℝ) : StabilityParameters D

The familiar Picard-rank-one slice B = beta H, omega = alpha H.

This constructor remains meaningful in higher Picard rank, but describes only the two-dimensional slice along the chosen ray H.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters.rankOne H alpha beta = { B := beta • H, omega := alpha • H }

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters.orthogonalSlice {D : Type u} [AddCommGroup D] [Module ℝ D] (H G : D) (s u t : ℝ) : StabilityParameters D

The three-parameter slice used in higher-Picard-rank wall calculations: B = s H + u G and omega = t H.

Orthogonality H.G = 0 and positivity t > 0 are geometric hypotheses on a particular use of this constructor, not data needed to form the charge.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters.orthogonalSlice H G s u t = { B := s • H + u • G, omega := t • H }

structure CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorialParameters {D : Type u} (ample : Set D) extends CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.StabilityParameters D : Type u

Stability parameters together with a proof that omega lies in a supplied ample cone. The ample cone stays geometry-specific rather than being confused with the weaker numerical condition omega^2 > 0.

• B : D
• omega : D
• omega_ample : self.omega ∈ ample

  The chosen omega is ample in the supplied geometric model.

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) : ChargeCoordinates N

Untwisted charge coordinates measured against one divisor class H.

This is the lossy rank-one view used by the pre-existing surface charge API: it retains H.chOne and H^2, but not the full first Chern class.

Equations

• ch.coordinatesAt S H = { rank := ch.rank, degree := (S.intersection H).toAddMonoidHom.comp ch.chOne, chTwo := ch.chTwo, hyperplaneSquare := S.pair H H }

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt_rank {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (E : N) : (ch.coordinatesAt S H).rank E = ch.rank E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt_degree {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (E : N) : (ch.coordinatesAt S H).degree E = S.pair H (ch.chOne E)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt_chTwo {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (E : N) : (ch.coordinatesAt S H).chTwo E = ch.chTwo E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.coordinatesAt_hyperplaneSquare {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) : (ch.coordinatesAt S H).hyperplaneSquare = S.pair H H

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeCoordinates {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) : ChargeCoordinates N

The terminal charge coordinates obtained after twisting in the full divisor space. This is the bridge to the surface charge polynomial already used by rank-one examples.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeCoordinates_rank {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.chargeCoordinates S P).rank E = ch.rank E

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeCoordinates_degree {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.chargeCoordinates S P).degree E = S.pair P.omega (ch.chOne E - ch.rank E • P.B)

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeCoordinates_chTwo {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.chargeCoordinates S P).chTwo E = ch.chTwo E - S.pair P.B (ch.chOne E) + S.pair P.B P.B * ch.rank E / 2

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.chargeCoordinates_hyperplaneSquare {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) : (ch.chargeCoordinates S P).hyperplaneSquare = S.pair P.omega P.omega

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.Pullback.coordinatesAt {D : Type u} [AddCommGroup D] [Module ℝ D] {L : Type u_1} {M : Type u_2} [AddCommGroup L] [AddCommGroup M] {source : ChernCharacter L D} {target : ChernCharacter M D} (h : source.Pullback target) (S : DivisorSpace D) (H : D) : (source.coordinatesAt S H).Pullback (target.coordinatesAt S H)

A full-character comparison induces the old rank-one coordinate comparison at every chosen divisor class H.

Equations

• h.coordinatesAt S H = { map := h.map, rank_eq := ⋯, degree_eq := ⋯, chTwo_eq := ⋯, hyperplaneSquare_eq := ⋯ }

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.Pullback.chargeCoordinates {D : Type u} [AddCommGroup D] [Module ℝ D] {L : Type u_1} {M : Type u_2} [AddCommGroup L] [AddCommGroup M] {source : ChernCharacter L D} {target : ChernCharacter M D} (h : source.Pullback target) (S : DivisorSpace D) (P : StabilityParameters D) : (source.chargeCoordinates S P).Pullback (target.chargeCoordinates S P)

A full-character comparison induces a comparison of every derived charge view.

Equations

• h.chargeCoordinates S P = { map := h.map, rank_eq := ⋯, degree_eq := ⋯, chTwo_eq := ⋯, hyperplaneSquare_eq := ⋯ }

noncomputable def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.centralCharge {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) : N →+ ℂ

The intrinsic divisorial surface central charge.

Equations

• ch.centralCharge S P = (ch.chargeCoordinates S P).centralCharge 1

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.Pullback.centralCharge_eq {D : Type u} [AddCommGroup D] [Module ℝ D] {L : Type u_1} {M : Type u_2} [AddCommGroup L] [AddCommGroup M] {source : ChernCharacter L D} {target : ChernCharacter M D} (h : source.Pullback target) (S : DivisorSpace D) (P : StabilityParameters D) (E : L) : (source.centralCharge S P) E = (target.centralCharge S P) (h.map E)

A full-character comparison intertwines the intrinsic central charge for every choice of B and omega.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.centralCharge_apply_twisted {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.centralCharge S P) E = -↑((ch.twist S P.B).chTwo E) + ↑(S.pair P.omega P.omega * ch.rank E / 2) + Complex.I * ↑(S.pair P.omega ((ch.twist S P.B).chOne E))

Expansion in twisted Chern-character notation.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.centralCharge_apply {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.centralCharge S P) E = ↑(-ch.chTwo E + S.pair P.B (ch.chOne E) - (S.pair P.B P.B - S.pair P.omega P.omega) * ch.rank E / 2) + Complex.I * ↑(S.pair P.omega (ch.chOne E) - S.pair P.omega P.B * ch.rank E)

Expansion in untwisted Chern-character coordinates.

This is the formula used for divisorial stability conditions in arbitrary Picard rank.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.centralCharge_rankOne_eq {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (H : D) (alpha beta : ℝ) (E : N) : (ch.centralCharge S (StabilityParameters.rankOne H alpha beta)) E = (((ch.coordinatesAt S H).twistByScalar beta).centralCharge alpha) E

The intrinsic charge restricts to the existing scalar-twist formula on the rank-one slice B = beta H, omega = alpha H.

Thus the old compressed coordinates remain a valid downstream interface; they are no longer asked to represent an arbitrary B-field.

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.centralCharge_eq_realPairing {D : Type u} [AddCommGroup D] [Module ℝ D] {N : Type v} [AddCommGroup N] (ch : ChernCharacter N D) (S : DivisorSpace D) (P : StabilityParameters D) (E : N) : (ch.centralCharge S P) E = ↑(Mukai.realPairing S.intersection (Mukai.expRe S.intersection P.B P.omega) (ch.toRealExtension E)) + Complex.I * ↑(Mukai.realPairing S.intersection (Mukai.expIm S.intersection P.B P.omega) (ch.toRealExtension E))

The same charge written as the Mukai pairing with exp(B + i omega). This makes the relation with the period-domain layer explicit without baking Mukai-specific geometry into ChernCharacter.