A nontrivial orthogonal slice, and the first IsGeometric witness

Walls/Divisorial/Slice.lean builds the basis-free orthogonal slice and attaches two certificates to it: IsHodge, which asks the distinguished direction to have positive square and every nonzero transverse direction negative square, and IsGeometric, which adds that the direction is ample.

Before this file the tree had two slices and one and a half certificates.

• The rank-one slice has transverse space Fin 0 → ℝ, so it is the classical (s, t) plane and rankOne_isHodge is vacuous in its second clause.
• SmoothQuadricCharge.wallSlice has a one-dimensional transverse space but no certificate.
• IsGeometric had no witness at all. Not for want of an ample cone: SmoothQuadricCharge.ampleCone is one, and carries a DivisorialParameters over it. What was missing was anyone proving the certificate for a slice. The blow-up had no cone either way, recording ampleness only as IsAmpleCoefficients, a predicate on rational coefficients that nothing consumes.

This file supplies a slice whose transverse space is a genuine plane, both certificates for it, and the ample cone the second needs.

The slice

The anticanonical class -K = 3H - E₁ - E₂ has square 7, and its orthogonal complement in the rank-three space is two-dimensional:

x ⊥ -K  ↔  3x₀ + x₁ + x₂ = 0,

spanned by E₁ - E₂ and H - E₁ - 2E₂. transverse is that parameterization. IsHodge is then immediate from hodgeDefinite, which this model proves rather than assumes, and injectivity of transverse is what turns u ≠ 0 into transverse u ≠ 0.

The ample cone

ampleCone is the real cone aH + bE₁ + cE₂ with b < 0, c < 0 and -b - c < a, which is IsAmpleCoefficients written for the realized coordinates; mem_ampleCone_of_isAmpleCoefficients is the bridge, so the file does not introduce a second unrelated notion of ampleness.

divisorialParameters then bundles that cone into the core DivisorialParameters, which until now had a single inhabitant, at the smooth quadric. A structure written to accept any geometry-specific ample cone had been carrying one geometry; the blow-up is the second.

What is not claimed

No scheme and no ample line bundle appear. ampleCone is a subset of ℝ³ chosen to match the classical description of the ample cone of a two-point blow-up; nothing here proves that it is that cone for a geometric surface, and IsGeometric asks only that the direction lie in the supplied set.

The ample cone, as a set of real divisors

def AlgebraicGeometry.Numerical.Examples.BlowUpPlane.ampleCone : Set Divisor

The ample cone of the two-point blow-up, in the realized coordinates aH + bE₁ + cE₂: both exceptional coefficients negative, and the hyperplane coefficient exceeding their sum in absolute value.

Equations

• AlgebraicGeometry.Numerical.Examples.BlowUpPlane.ampleCone = {x : AlgebraicGeometry.Numerical.Examples.BlowUpPlane.Divisor | x.2.1 < 0 ∧ x.2.2 < 0 ∧ -x.2.1 - x.2.2 < x.1}

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.mem_ampleCone_iff (x : Divisor) : x ∈ ampleCone ↔ x.2.1 < 0 ∧ x.2.2 < 0 ∧ -x.2.1 - x.2.2 < x.1

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.mem_ampleCone_of_isAmpleCoefficients {a b c : ℚ} (h : IsAmpleCoefficients a b c) : (↑a, ↑(-b), ↑(-c)) ∈ ampleCone

The rational ample condition lands in the real cone. This is what keeps ampleCone from being a second, unrelated notion of ampleness: it is IsAmpleCoefficients read in the realized coordinates, where aH - bE₁ - cE₂ becomes (a, -b, -c).

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.antiCanonical_mem_ampleCone : numericalRealization.realizePolarization antiCanonicalPolarization ∈ ampleCone

The realized anticanonical class is ample.

The transverse plane

def AlgebraicGeometry.Numerical.Examples.BlowUpPlane.transverseMap : ℝ × ℝ →ₗ[ℝ] Divisor

The two-dimensional orthogonal complement of -K, spanned by E₁ - E₂ and H - E₁ - 2E₂.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.transverseMap_apply (u : ℝ × ℝ) : transverseMap u = (u.2, u.1 - u.2, -u.1 - 2 * u.2)

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.pair_antiCanonical_transverse (u : ℝ × ℝ) : divisorSpace.pair (numericalRealization.realizePolarization antiCanonicalPolarization) (transverseMap u) = 0

Every transverse direction is orthogonal to -K. The defining equation of the complement is 3x₀ + x₁ + x₂ = 0.

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.transverseMap_injective : Function.Injective ⇑transverseMap

The parameterization is injective, which is what turns u ≠ 0 into transverse u ≠ 0.

The slice, and its two certificates

noncomputable def AlgebraicGeometry.Numerical.Examples.BlowUpPlane.antiCanonicalSlice : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice divisorSpace (ℝ × ℝ)

An orthogonal slice whose transverse space is a plane.

The rank-one slice has transverse space Fin 0 → ℝ and the quadric's has a line; this is the first with a two-dimensional one, which is what Picard rank three buys.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.antiCanonicalSlice_H : antiCanonicalSlice.H = numericalRealization.realizePolarization antiCanonicalPolarization

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.antiCanonicalSlice_isHodge : antiCanonicalSlice.IsHodge

The slice is Hodge, and not vacuously: the second clause quantifies over a plane of transverse directions, and is discharged by hodgeDefinite, which this model proves.

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.antiCanonicalSlice_isGeometric : antiCanonicalSlice.IsGeometric ampleCone

The first IsGeometric witness in the repository.

IsGeometric adds ampleness of the distinguished direction to the Hodge data. Nothing inhabited it before. SmoothQuadricCharge.ampleCone shows the missing piece was not a cone but the certificate itself: no slice in the tree had one.

Charge parameters over the cone

noncomputable def AlgebraicGeometry.Numerical.Examples.BlowUpPlane.divisorialParameters (b : Divisor) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DivisorialParameters ampleCone

The second DivisorialParameters in the repository, over the blow-up's own ample cone.

SmoothQuadricCharge.divisorialParameters was the only one, so the structure that was written to carry any geometry-specific ample cone was carrying exactly one. Nothing mathematical was missing here: ampleCone and antiCanonical_mem_ampleCone are already above, and the bundling is what the core API asks a geometric consumer to do. omega is the anticanonical direction of antiCanonicalSlice, so these parameters and the slice describe the same polarization; the B-field stays arbitrary, because ampleness constrains omega alone.

Equations

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

The wall family of the slice

noncomputable def AlgebraicGeometry.Numerical.Examples.BlowUpPlane.sliceChargeFamily : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.ChargeFamily (CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point (ℝ × ℝ)) NumericalClass

The wall family of the two-point blow-up along the anticanonical slice, indexed by (s, u, t) with u in a plane.

Equations

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

@[simp]

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.sliceChargeFamily_charge (p : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point (ℝ × ℝ)) (E : NumericalClass) : (sliceChargeFamily.charge p) E = (numericalRealization.chernCharacter.centralCharge divisorSpace (antiCanonicalSlice.parameters p)) E

theorem AlgebraicGeometry.Numerical.Examples.BlowUpPlane.alignmentLocus_ofST_iff_circle (uu : ℝ × ℝ) {p : ℝ × ℝ} (ht : p.2 ≠ 0) (v w : NumericalClass) : CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.OrthogonalSlice.Point.ofST uu p ∈ antiCanonicalSlice.alignmentLocus numericalRealization.chernCharacter v w ↔ CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.minA ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass v) ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass w) * (p.1 ^ 2 + p.2 ^ 2) + 2 * CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.minB ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass v) ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass w) * p.1 + 2 * CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.minC ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass v) ((antiCanonicalSlice.sliceCoordinates numericalRealization.chernCharacter uu).toNumClass w) = 0

The circle description of walls fires on this slice.

For each fixed transverse parameter the wall of two classes in the (s, t) half-plane is a circle or a line, by alignmentLocus_ofST_iff_circle. On the rank-one slice that statement has one such half-plane; here it has a plane's worth.