The Mukai charge, as a second child rather than an overload #

Charge.lean builds the divisorial central charge out of a ChernCharacter whose third coordinate is the ordinary ch₂. Bridgeland's K3 construction (arXiv:math/0307164, §6) instead pairs exp(B + iω) with the Mukai vector

v(E) = ch(E) √td_X,   v(E) = (r, c₁, s) with s = ch₂ + r on a K3,

whose third coordinate is ch₂ + rank, not ch₂. Writing that vector into a ChernCharacter would put a Todd-corrected number into a field whose contract says it holds the ordinary Chern character, so this file gives the Mukai presentation its own name and relates the two by a proved comparison.

What `√td_X` contributes, and why two numbers suffice #

On a surface only two components of √td_X can reach the charge: the codimension-one class √td₁ and the number ∫√td₂. SqrtTodd carries exactly those two, so the Mukai vector is

v(E) = (r, c₁ + r √td₁, ch₂ + √td₁ · c₁ + r ∫√td₂).

SqrtTodd.trivial is (0, 0) and SqrtTodd.k3 is (0, 1), the latter being the formal content of √td = 1 + [pt] on a K3. The two presentations are then two values of one parameter rather than two constructions: mukaiCharge_trivial says the ordinary divisorial charge is the Mukai charge at SqrtTodd.trivial, and mukaiCharge_k3 says the K3 Mukai charge is the ordinary charge minus the rank.

The charge is the existing exponential charge #

CentralCharge/Mukai/Charge.lean already owns Mukai.expChargeHom, the additive Z(β,ω) on a real Mukai extension. Nothing is rebuilt here: mukaiCharge is that homomorphism composed with the Mukai class map, and centralCharge_eq_expChargeHom records that the ordinary divisorial charge is the same homomorphism composed with the ordinary triple. So the divisorial layer and the Mukai lattice layer share one charge formula.

Walls are not preserved #

The Mukai and ordinary charges differ by a term that is real-linear in the class but is not a scalar multiple of the charge, so wall_smul does not apply and the two families have different walls in general. That is the point of keeping them apart, and mukaiCharge_k3 makes the difference explicit.

Nothing here is a stability condition, wall, heart, or K3 surface; SqrtTodd is supplied by Todd.lean, and no theorem below claims it comes from a geometric √td.

source

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiVector {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (t : SqrtTodd D) :

N →+ Mukai.RealExtension D

The Mukai vector v(E) = ch(E) √td_X, as an additive map into the real Mukai extension of the divisor space.

Its third coordinate is deliberately not ch₂: it is ch₂ + √td₁·c₁ + r∫√td₂, which on a K3 is ch₂ + r.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiVector_apply {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (t : SqrtTodd D) (E : N) :

(ch.mukaiVector S t) E = (ch.rank E, ch.chOne E + ch.rank E • t.divisor, ch.chTwo E + S.pair t.divisor (ch.chOne E) + ch.rank E * t.number)

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiVector_trivial {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (E : N) :

(ch.mukaiVector S SqrtTodd.trivial) E = ch.toRealExtension E

At the trivial square root the Mukai vector is the ordinary Chern-character triple.

Not a simp lemma: with pair_zero_left the left-hand side already reduces to the right-hand side, so simp proves it and the normal-form linter rejects the attribute. It is stated because it is the identification that makes the ordinary charge a value of the Mukai parameter.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiVector_k3 {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (E : N) :

(ch.mukaiVector S SqrtTodd.k3) E = (ch.rank E, ch.chOne E, ch.chTwo E + ch.rank E)

On a K3 square root the Mukai vector is (r, c₁, ch₂ + r), which is Bridgeland's v(E) = (r, c₁, s) with s = ch₂ + rank.

Not a simp lemma, for the reason given at mukaiVector_trivial.

source

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

(ch.centralCharge S P) E = (Mukai.expChargeHom S.intersection P.B P.omega) (ch.toRealExtension E)

The ordinary divisorial charge is the exponential charge of the Mukai lattice layer, composed with the ordinary triple.

This is centralCharge_eq_realPairing restated against the additive homomorphism Mukai.expChargeHom, and it is what lets the two layers share one charge formula.

source

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

N →+ ℂ

The Mukai central charge: Bridgeland's Z(E) = (exp(B + iω), v(E)).

It is the same Mukai.expChargeHom the ordinary charge uses, composed with the Mukai class map instead of the ordinary triple.

Equations

ch.mukaiCharge S t P = (Mukai.expChargeHom S.intersection P.B P.omega).comp (ch.mukaiVector S t)

Instances For

source

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiCharge_apply {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (t : SqrtTodd D) (P : StabilityParameters D) (E : N) :

(ch.mukaiCharge S t P) E = Mukai.expCharge S.intersection P.B P.omega ((ch.mukaiVector S t) E)

source

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

(ch.mukaiCharge S SqrtTodd.trivial P) E = (ch.centralCharge S P) E

At the trivial square root the Mukai charge is the ordinary divisorial charge. The two presentations are two values of one parameter.

source

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.ChernCharacter.mukaiCharge_eq_centralCharge_add {N : Type v} {D : Type w} [AddCommGroup N] [AddCommGroup D] [Module ℝ D] (ch : ChernCharacter N D) (S : DivisorSpace D) (t : SqrtTodd D) (P : StabilityParameters D) (E : N) :

(ch.mukaiCharge S t P) E = (ch.centralCharge S P) E + ↑(ch.rank E * S.pair P.B t.divisor - S.pair t.divisor (ch.chOne E) - ch.rank E * t.number) + Complex.I * ↑(ch.rank E * S.pair P.omega t.divisor)

The exact comparison. The Mukai charge exceeds the ordinary divisorial charge by a term linear in the class and determined by √td_X.

source

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

(ch.mukaiCharge S SqrtTodd.k3 P) E = (ch.centralCharge S P) E - ↑(ch.rank E)

On a K3 the Mukai charge is the ordinary charge minus the rank.

This is the whole numerical difference between Bridgeland's presentation and the Arcara--Bertram / Macrì--Schmidt one on a K3, and it is why the two have different walls: the shift is not a scalar multiple of the charge.

source