Twisted Chern characters

For a numerical divisor class B, the twisted Chern character is ch^B = e^{−B}·ch, component by component. A rational scalar β and a polarisation H give the familiar specialization B = βH:

ch^β_i(E) = ∑_{j ≤ i} ((−β)^(i−j) / (i−j)!) · ch_j(E) · H^(i−j)

Nothing of the sort existed in the numerical layer, so the tilt slope ν_{α,β} and the BMT quantity Q_{α,β} could not previously be written down at all.

What makes the name honest

The exponential notation is a claim, and twist_add_beta is the theorem that earns it: twisting by β₁ + β₂ is twisting by β₂ and then by β₁. That is e^{−(β₁+β₂)H} = e^{−β₁H}·e^{−β₂H} read off the graded components, and it is the only real proof in this file.

It reduces to the scalar identity twistCoeff_add,

(x + y)^m / m! = ∑_{a ≤ m} (x^a / a!) · (y^(m−a) / (m−a)!)

— the binomial theorem divided through by m! — plus a triangular reindexing of the double sum. The reindexing is where the work is: the two sums run in opposite directions, so a reflection (Finset.sum_range_reflect) sits between them.

Stated on a bare graded ring first

twistCoeff and twist mention no variety, no polarisation and no Chern character: twist convolves an arbitrary family c : ℕ → A against the exponential coefficients of an arbitrary ring element H. The group law is a fact about that convolution and is proved there. chBetaComp is then the specialisation at H = P.cls and c = V.chComp E, and inherits it.

This is deliberate. The group law has nothing to do with geometry, and proving it against NumericalVarietyData would have hidden that behind hypotheses it never uses.

Main results

• twistCoeff, twistCoeff_add — the scalar exponential coefficients.
• twist, twist_add_beta — the convolution and the group law.
• BField and chBComp — an arbitrary rational numerical B-field and ch^B_i(E);
• chBetaComp — the Picard-rank-one notation ch^(βH)_i(E), with chBComp_along_eq_chBetaComp proving that the two notations agree.

The scalar coefficients

noncomputable def AlgebraicGeometry.Numerical.twistCoeff (β : ℚ) (m : ℕ) : ℚ

The coefficient of H^m in e^{−βH}.

Equations

• AlgebraicGeometry.Numerical.twistCoeff β m = (-β) ^ m / ↑m.factorial

@[simp]

theorem AlgebraicGeometry.Numerical.twistCoeff_zero_beta (m : ℕ) : twistCoeff 0 m = if m = 0 then 1 else 0

theorem AlgebraicGeometry.Numerical.twistCoeff_add (β₁ β₂ : ℚ) (m : ℕ) : twistCoeff (β₁ + β₂) m = ∑ a ∈ Finset.range (m + 1), twistCoeff β₁ a * twistCoeff β₂ (m - a)

The exponential functional equation, at the level of coefficients. The binomial theorem divided through by m!.

The twist on a bare graded ring

noncomputable def AlgebraicGeometry.Numerical.twist {A : Type u} [CommRing A] [Algebra ℚ A] (H : A) (β : ℚ) (c : ℕ → A) (i : ℕ) : A

Convolution against e^{−βH}, for an arbitrary family c : ℕ → A and an arbitrary H : A. No variety and no polarisation appear.

Equations

• AlgebraicGeometry.Numerical.twist H β c i = ∑ j ∈ Finset.range (i + 1), (algebraMap ℚ A) (AlgebraicGeometry.Numerical.twistCoeff β (i - j)) * c j * H ^ (i - j)

theorem AlgebraicGeometry.Numerical.twist_add_beta {A : Type u} [CommRing A] [Algebra ℚ A] (H : A) (β₁ β₂ : ℚ) (c : ℕ → A) (i : ℕ) : twist H (β₁ + β₂) c i = twist H β₁ (twist H β₂ c) i

The group law: e^{−(β₁+β₂)H} = e^{−β₁H}·e^{−β₂H}, read on components.

This is what makes the exponential notation honest rather than decorative.

theorem AlgebraicGeometry.Numerical.twist_algebraMap_mul {A : Type u} [CommRing A] [Algebra ℚ A] (H : A) (β : ℚ) (c : ℕ → A) (i : ℕ) : twist ((algebraMap ℚ A) β * H) 1 c i = twist H β c i

Absorbing a scalar into the twisting class does not change the twist: e^{-(βH)} = e^{-βH}.

The twisted Chern character

structure AlgebraicGeometry.Numerical.BField {A : Type u} [CommRing A] [Algebra ℚ A] {n : ℕ} (R : NumericalRingData n A) : Type u

A numerical B-field: an arbitrary rational codimension-one class.

No positivity is required. The rational scalar restriction comes from the current NumericalRingData, whose intersection ring and degree map are over ℚ; it is not a mathematical restriction on the usual real B-field.

• cls : A

  The numerical divisor class B.

• cls_mem : self.cls ∈ R.piece 1

  The class lies in codimension one.

theorem AlgebraicGeometry.Numerical.BField.pow_mem {A : Type u} [CommRing A] [Algebra ℚ A] {n : ℕ} {R : NumericalRingData n A} (B : BField R) (i : ℕ) : B.cls ^ i ∈ R.piece i

Powers of a B-field have their expected codimension.

noncomputable def AlgebraicGeometry.Numerical.BField.along {A : Type u} [CommRing A] [Algebra ℚ A] {n : ℕ} {R : NumericalRingData n A} (P : Polarization R) (β : ℚ) : BField R

The B-field βH determined by a polarisation and a rational scalar.

Equations

• AlgebraicGeometry.Numerical.BField.along P β = { cls := (algebraMap ℚ A) β * P.cls, cls_mem := ⋯ }

@[simp]

theorem AlgebraicGeometry.Numerical.BField.along_cls {A : Type u} [CommRing A] [Algebra ℚ A] {n : ℕ} {R : NumericalRingData n A} (P : Polarization R) (β : ℚ) : (along P β).cls = (algebraMap ℚ A) β * P.cls

The class underlying the scalar B-field is literally βH.

noncomputable def AlgebraicGeometry.Numerical.chBComp {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) (i : ℕ) : A

The B-twisted Chern-character component ch^B_i(E).

Equations

• AlgebraicGeometry.Numerical.chBComp V B E i = AlgebraicGeometry.Numerical.twist B.cls 1 (V.chComp E) i

theorem AlgebraicGeometry.Numerical.chBComp_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) (i : ℕ) : chBComp V B E i = ∑ j ∈ Finset.range (i + 1), (algebraMap ℚ A) (twistCoeff 1 (i - j)) * V.chComp E j * B.cls ^ (i - j)

The component formula obtained by expanding the truncated exponential e^{-B}.

theorem AlgebraicGeometry.Numerical.chBComp_mem {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) (i : ℕ) : chBComp V B E i ∈ V.ring.piece i

ch^B_i(E) remains in codimension i.

theorem AlgebraicGeometry.Numerical.chBComp_add {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E F : N) (i : ℕ) : chBComp V B (E + F) i = chBComp V B E i + chBComp V B F i

The B-twisted Chern character is additive in the numerical class.

theorem AlgebraicGeometry.Numerical.chBComp_zero {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) : chBComp V B E 0 = V.chComp E 0

The codimension-zero component is unchanged by a B-field twist.

theorem AlgebraicGeometry.Numerical.chBComp_one {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) : chBComp V B E 1 = V.chComp E 1 - V.chComp E 0 * B.cls

The first twisted component is ch₁^B = ch₁ - B ch₀.

theorem AlgebraicGeometry.Numerical.chBComp_two {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (B : BField V.ring) (E : N) : chBComp V B E 2 = V.chComp E 2 - V.chComp E 1 * B.cls + (algebraMap ℚ A) (1 / 2) * V.chComp E 0 * B.cls ^ 2

The second twisted component is ch₂^B = ch₂ - B ch₁ + (B²/2) ch₀.

noncomputable def AlgebraicGeometry.Numerical.chBetaComp {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β : ℚ) (E : N) (i : ℕ) : A

The β-twisted Chern character ch^β_i(E).

Equations

• AlgebraicGeometry.Numerical.chBetaComp V P β E i = AlgebraicGeometry.Numerical.twist P.cls β (V.chComp E) i

theorem AlgebraicGeometry.Numerical.chBetaComp_eq {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β : ℚ) (E : N) (i : ℕ) : chBetaComp V P β E i = ∑ j ∈ Finset.range (i + 1), (algebraMap ℚ A) (twistCoeff β (i - j)) * V.chComp E j * P.cls ^ (i - j)

theorem AlgebraicGeometry.Numerical.chBetaComp_mem {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β : ℚ) (E : N) (i : ℕ) : chBetaComp V P β E i ∈ V.ring.piece i

ch^β_i(E) lives in codimension i, like ch_i(E): each summand is piece 0 · piece j · piece (i−j), and j + (i−j) = i inside the sum's range.

theorem AlgebraicGeometry.Numerical.chBetaComp_add {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β : ℚ) (E F : N) (i : ℕ) : chBetaComp V P β (E + F) i = chBetaComp V P β E i + chBetaComp V P β F i

The twisted Chern character is additive in the class, because ch is.

theorem AlgebraicGeometry.Numerical.chBetaComp_zero_beta {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (E : N) (i : ℕ) : chBetaComp V P 0 E i = V.chComp E i

At β = 0 the twist is the identity: ch^0 = ch.

theorem AlgebraicGeometry.Numerical.chBetaComp_add_beta {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β₁ β₂ : ℚ) (E : N) (i : ℕ) : chBetaComp V P (β₁ + β₂) E i = twist P.cls β₁ (chBetaComp V P β₂ E) i

The group law on the twisted Chern character, inherited from twist.

theorem AlgebraicGeometry.Numerical.chBComp_along_eq_chBetaComp {A : Type u} [CommRing A] [Algebra ℚ A] {N : Type v} [AddCommGroup N] {n : ℕ} (V : NumericalVarietyData n A N) (P : Polarization V.ring) (β : ℚ) (E : N) (i : ℕ) : chBComp V (BField.along P β) E i = chBetaComp V P β E i

The arbitrary-class notation and the scalar notation agree at B = βH.