Transporting a polarised threefold class to the (α, β) plane

CentralCharge/Numerical/Threefold.lean does its charge arithmetic on NumClass, a quadruple of reals, and says of it: "It is not ch(E) for a sheaf E." This file supplies the map that makes it one, exactly as WallTransport.lean does in the surface case, and on the same side of the geometry boundary.

The rank slot carries ∫H³

Matching the surface file, where it carries ∫H². The four coordinates are

∫H³·ch₀,   ∫H²·ch₁,   ∫H·ch₂,   ∫ch₃,

and the first is weighted because that is what the charge polynomial requires.

The compressed twist is the ring twist

betaTwist_toNumClass is the theorem the file turns on: the four-coordinate betaTwist of Walls/Threefold/ agrees with the twisted degrees degH1Beta, degH2Beta and deg3Beta that BMT.lean reads off chBetaComp. It is proved by expanding the truncated exponential in each of codimensions one, two and three; the three helper lemmas below are that expansion and are the only real computation here.

With it, Q_toNumClass and nu_toNumClass identify the compressed Bayer--Macrì--Toda quantity and tilt slope with the ones BMT.lean already defines, so there is one Q in the library rather than two.

The conjecture is transported, not proved

Q_toNumClass_nonneg takes BMTData — supplied data that is false for some threefolds, see BMT.lean — and restates its inequality on the transported class. Nothing here makes it more true than it was.

The twisted degrees, expanded

The three lemmas below expand the truncated exponential e^{-βH} in codimensions one, two and three. They are the only real computation in the file; everything after them is bookkeeping.

theorem AlgebraicGeometry.Numerical.Threefold.degH1Beta_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (β : ℚ) (E : N) : degH1Beta V P β E = V.ring.degree (V.chComp E 1 * P.cls ^ 2) - β * (V.ring.degree (P.cls ^ 3) * ↑(V.rank E))

∫H²·ch₁^β = ∫H²ch₁ − β·∫H³ch₀.

theorem AlgebraicGeometry.Numerical.Threefold.degH2Beta_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (β : ℚ) (E : N) : degH2Beta V P β E = V.ring.degree (V.chComp E 2 * P.cls) - β * V.ring.degree (V.chComp E 1 * P.cls ^ 2) + β ^ 2 / 2 * (V.ring.degree (P.cls ^ 3) * ↑(V.rank E))

∫H·ch₂^β = ∫H·ch₂ − β·∫H²ch₁ + (β²/2)·∫H³ch₀.

theorem AlgebraicGeometry.Numerical.Threefold.deg3Beta_eq {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (β : ℚ) (E : N) : deg3Beta V P β E = V.ring.degree (V.chComp E 3) - β * V.ring.degree (V.chComp E 2 * P.cls) + β ^ 2 / 2 * V.ring.degree (V.chComp E 1 * P.cls ^ 2) - β ^ 3 / 6 * (V.ring.degree (P.cls ^ 3) * ↑(V.rank E))

∫ch₃^β = ∫ch₃ − β·∫H·ch₂ + (β²/2)·∫H²ch₁ − (β³/6)·∫H³ch₀.

The transport

noncomputable def AlgebraicGeometry.Numerical.Threefold.toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass

A polarised threefold class as a point of the (α, β) charge plane.

The first slot carries ∫H³; see the module docstring.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.toNumClass_deg0 {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : (toNumClass V P E).deg0 = ↑(V.ring.degree (P.cls ^ 3) * ↑(V.rank E))

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.toNumClass_deg1 {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : (toNumClass V P E).deg1 = ↑(V.ring.degree (V.chComp E 1 * P.cls ^ 2))

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.toNumClass_deg2 {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : (toNumClass V P E).deg2 = ↑(V.ring.degree (V.chComp E 2 * P.cls))

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.toNumClass_deg3 {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : (toNumClass V P E).deg3 = ↑(V.ring.degree (V.chComp E 3))

theorem AlgebraicGeometry.Numerical.Threefold.toNumClass_add {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E F : N) : toNumClass V P (E + F) = toNumClass V P E + toNumClass V P F

The transport is additive, because rank and the three degrees all are.

noncomputable def AlgebraicGeometry.Numerical.Threefold.toNumClassHom {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) : N →+ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.NumClass

The transport, bundled additively.

Equations

• AlgebraicGeometry.Numerical.Threefold.toNumClassHom V P = AddMonoidHom.mk' (AlgebraicGeometry.Numerical.Threefold.toNumClass V P) ⋯

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.toNumClassHom_apply {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (E : N) : (toNumClassHom V P) E = toNumClass V P E

noncomputable def AlgebraicGeometry.Numerical.Threefold.wallChargeFamily {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (ℝ × ℝ) N

The threefold charge family of a polarised numerical threefold, as a pullback of the generic (α, β) child.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Threefold.wallChargeFamily_charge {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (p : ℝ × ℝ) (E : N) : ((wallChargeFamily V P).charge p) E = (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge p.1 p.2) (toNumClass V P E)

The compressed twist is the ring twist

theorem AlgebraicGeometry.Numerical.Threefold.betaTwist_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist (↑β) (toNumClass V P E) = (↑(V.ring.degree (P.cls ^ 3) * ↑(V.rank E)), ↑(degH1Beta V P β E), ↑(degH2Beta V P β E), ↑(deg3Beta V P β E))

The identity the bridge turns on. The four-coordinate betaTwist agrees with the twisted degrees BMT.lean reads off chBetaComp.

theorem AlgebraicGeometry.Numerical.Threefold.discr_betaTwist_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.discr (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.betaTwist (↑β) (toNumClass V P E)) = ↑(discrHBeta V P E)

The compressed discriminant is the H-twisted discriminant of BMT.lean.

theorem AlgebraicGeometry.Numerical.Threefold.Q_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q (↑α) (↑β) (toNumClass V P E) = ↑(Q V P α β E)

The compressed Bayer--Macrì--Toda quantity is the one BMT.lean defines. There is one Q in the library, not two.

theorem AlgebraicGeometry.Numerical.Threefold.nu_toNumClass {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (α β : ℚ) (E : N) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.nu (↑α) (↑β) (toNumClass V P E) = ↑(nu V P α β E)

The compressed tilt slope is the one BMT.lean defines.

The conjecture, transported and no more true than before

theorem AlgebraicGeometry.Numerical.Threefold.Q_toNumClass_nonneg {A : Type u} {N : Type v} [CommRing A] [Algebra ℚ A] [AddCommGroup N] (V : NumericalVarietyData 3 A N) (P : Polarization V.ring) (B : BMTData V P) {α β : ℚ} {E : N} (hα : 0 < α) (hE : B.TiltSemistable α β E) : 0 ≤ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q (↑α) (↑β) (toNumClass V P E)

The Bayer--Macrì--Toda inequality on the transported class.

BMTData is supplied data and is false for some threefolds — see BMT.lean. This restates it; it proves nothing about sheaves.