The threefold wall transport, on the quintic

Examples/Threefold/ProjectiveSpaceWalls.lean connected the transport of Stability/ThreefoldWallTransport.lean to the ℙ³ model. This file does the same for the quintic Calabi--Yau threefold, which was in the same position: a model referenced only inside its own file, with no polarization defined for it.

Why the second threefold is worth doing

ℙ³ and the quintic differ in exactly the two places the transport touches.

• The degree. ∫H³ = 5 rather than 1, so every one of the four degrees carries a factor the ℙ³ computation could not see. A transport that silently assumed unit degree would pass on ℙ³ and fail here.
• The Todd class. The quintic has td₁ = 0 and ∫td₃ = χ(O) = 0, where ℙ³ has every coefficient nonzero. The transport does not read the Todd class, and these statements are the check that it does not: the four degrees below depend on the Chern coefficients and the degree alone.

The coordinates

With ∫H³ = 5 and linear-section coordinates (a, b, c, e),

∫H³ch₀ = 5a,   ∫H²ch₁ = 5b,   ∫H·ch₂ = 5(-b/2 + c),   ∫ch₃ = 5b/6 - 5c + e,

the last because threefoldChCoeff 5 divides the point coordinate by the degree, which the integral then undoes. That cancellation is the one place the quintic computation is not the ℙ³ one with a factor of five.

No second sanity witness

ProjectiveSpaceWalls.p3BMTSanity already shows BMTData is inhabitable, and a second tautological witness would add nothing. quintic_Q_toNumClass_nonneg therefore takes a supplied BMTData as a hypothesis, which is the honest shape: the Bayer--Macrì--Toda inequality is not proved here for the quintic or for anything else, and it is false for some threefolds.

The polarization

theorem AlgebraicGeometry.Numerical.Examples.quintic_degree_H_pow_three : quinticNumericalVariety.ring.degree (rankOneH 3 ^ 3) = 5

∫_X H³ = 5 on the quintic.

noncomputable def AlgebraicGeometry.Numerical.Examples.quinticPolarization : Polarization quinticNumericalVariety.ring

The hyperplane class as a polarization of the quintic.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.quinticPolarization_cls : quinticPolarization.cls = rankOneH 3

The transported class

The four degrees of a class on the quintic

The transport of (a, b, c, e) is (5a, 5b, 5(-b/2 + c), 5b/6 - 5c + e).

theorem AlgebraicGeometry.Numerical.Examples.quintic_toNumClass_deg0 (E : ThreefoldNum) : (Threefold.toNumClass quinticNumericalVariety quinticPolarization E).deg0 = ↑(5 * ↑(E 0))

Not a simp lemma: the generic Threefold.toNumClass_deg* projections are already simp and rewrite the left-hand side first, so the normal-form linter rejects the attribute. quintic_reZ and quintic_imZ name these explicitly.

theorem AlgebraicGeometry.Numerical.Examples.quintic_toNumClass_deg1 (E : ThreefoldNum) : (Threefold.toNumClass quinticNumericalVariety quinticPolarization E).deg1 = ↑(5 * ↑(E 1))

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

theorem AlgebraicGeometry.Numerical.Examples.quintic_toNumClass_deg2 (E : ThreefoldNum) : (Threefold.toNumClass quinticNumericalVariety quinticPolarization E).deg2 = ↑(5 * (-↑(E 1) / 2 + ↑(E 2)))

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

theorem AlgebraicGeometry.Numerical.Examples.quintic_toNumClass_deg3 (E : ThreefoldNum) : (Threefold.toNumClass quinticNumericalVariety quinticPolarization E).deg3 = ↑(5 * ↑(E 1) / 6 - 5 * ↑(E 2) + ↑(E 3))

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

The degree cancels the /5 that threefoldChCoeff 5 puts on the point coordinate, which is why this one is not the ℙ³ answer times five.

The charge family on the model

noncomputable def AlgebraicGeometry.Numerical.Examples.quinticWallChargeFamily : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (ℝ × ℝ) ThreefoldNum

The threefold charge family of the quintic, indexed by (α, β).

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.quinticWallChargeFamily_charge (p : ℝ × ℝ) (E : ThreefoldNum) : (quinticWallChargeFamily.charge p) E = (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.charge p.1 p.2) (Threefold.toNumClass quinticNumericalVariety quinticPolarization E)

theorem AlgebraicGeometry.Numerical.Examples.quintic_reZ (α β : ℝ) (E : ThreefoldNum) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.reZ α β (Threefold.toNumClass quinticNumericalVariety quinticPolarization E) = -↑(5 * ↑(E 1) / 6 - 5 * ↑(E 2) + ↑(E 3)) + β * ↑(5 * (-↑(E 1) / 2 + ↑(E 2))) - (β ^ 2 - α ^ 2) / 2 * ↑(5 * ↑(E 1)) + (β ^ 3 - 3 * β * α ^ 2) / 6 * ↑(5 * ↑(E 0))

The real part of the quintic charge, in linear-section coordinates.

theorem AlgebraicGeometry.Numerical.Examples.quintic_imZ (α β : ℝ) (E : ThreefoldNum) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.imZ α β (Threefold.toNumClass quinticNumericalVariety quinticPolarization E) = α * (↑(5 * (-↑(E 1) / 2 + ↑(E 2))) - β * ↑(5 * ↑(E 1)) + (3 * β ^ 2 - α ^ 2) / 6 * ↑(5 * ↑(E 0)))

The imaginary part of the quintic charge, in linear-section coordinates.

The transported Bayer--Macrì--Toda inequality

theorem AlgebraicGeometry.Numerical.Examples.quintic_Q_toNumClass_nonneg (B : Threefold.BMTData quinticNumericalVariety quinticPolarization) {α β : ℚ} {E : ThreefoldNum} (hα : 0 < α) (hE : B.TiltSemistable α β E) : 0 ≤ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Threefold.Q (↑α) (↑β) (Threefold.toNumClass quinticNumericalVariety quinticPolarization E)

The transported inequality on the quintic, taking the datum as a hypothesis.

No witness is constructed here. ProjectiveSpaceWalls.p3BMTSanity already shows the structure is inhabitable, and a second tautological witness would add nothing. The inequality itself is not proved for the quintic or for anything else, and it is false for some threefolds.