The diagonal model diag(1, -1, …, -1)

The signature-(1, k) form on ℝ × (Fin k → ℝ), and the proof that every vector of positive square carries a HodgeDefinite certificate for it.

The point of this file

Examples/Surface/BlowUpPlane.lean proves the same statement for k = 2 by destructuring three coordinates and calling nlinarith, and its own docstring calls that the hard part of the model. That proof does not scale: the number of coordinates is fixed in the syntax, and the polynomial arithmetic grows with it. hodgeDefinite_diagonal below is proved for every k at once, by the argument that actually generalises — Cauchy–Schwarz on the negative-definite part:

With w = (a, u) and x = (b, v), positivity of w² reads ‖u‖² < a² and orthogonality reads a·b = ⟪u, v⟫. Cauchy–Schwarz gives a²b² = ⟪u, v⟫² ≤ ‖u‖²‖v‖² < a²‖v‖² once ‖v‖² > 0, and dividing by a² > 0 gives b² < ‖v‖², which is x² < 0. When ‖v‖² = 0 the orthogonality relation forces b = 0 and x is zero, which the hypothesis excludes.

Nothing here is case-split on k, and no coordinate is named.

Transport

hodgeDefinite_of_equiv_diagonal is what makes the proof reusable: a DivisorSpace on any carrier that admits a form-preserving linear equivalence onto this model inherits the certificate. That is the intended route for a concrete surface model to stop proving its own Hodge index inequality.

What is not here

There is no surface. ℝ × (Fin k → ℝ) is a real vector space with a symmetric form; it is not N¹(X) ⊗ ℝ for any X, (1, 0, …, 0) is not claimed to be a hyperplane class, and no anticanonical class, ample cone or (-1)-class appears. The comparison with Examples/Surface/BlowUpPlane.lean cannot live in this file and does not: a module under LinearAlgebra/ may not import AlgebraicGeometry/, so the agreement lemma belongs to the consumer, built on the transport theorem below.

The model

@[reducible, inline]

abbrev CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DiagonalDivisor (k : ℕ) : Type

The carrier of the signature-(1, k) model: one coordinate of positive square and k of negative square.

Equations

• CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.DiagonalDivisor k = (ℝ × (Fin k → ℝ))

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.diagonalForm (k : ℕ) : LinearMap.BilinForm ℝ (DiagonalDivisor k)

The form diag(1, -1, …, -1) in k + 1 variables.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.diagonalForm_apply (k : ℕ) (x y : DiagonalDivisor k) : ((diagonalForm k) x) y = x.1 * y.1 - ∑ i : Fin k, x.2 i * y.2 i

def CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.diagonalSpace (k : ℕ) : DivisorSpace (DiagonalDivisor k)

The signature-(1, k) divisor space.

Equations

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

@[simp]

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.diagonalSpace_pair (k : ℕ) (x y : DiagonalDivisor k) : (diagonalSpace k).pair x y = x.1 * y.1 - ∑ i : Fin k, x.2 i * y.2 i

The Hodge index inequality, at every rank

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.hodgeDefinite_diagonal {k : ℕ} {w : DiagonalDivisor k} (hw : 0 < (diagonalSpace k).pair w w) : (diagonalSpace k).HodgeDefinite w

The reverse Cauchy–Schwarz inequality for diag(1, -1, …, -1). Every vector of positive square carries a Hodge certificate: the form is negative definite on its orthogonal complement.

Proved for all k at once. The one inequality doing the work is Finset.sum_mul_sq_le_sq_mul_sq, Cauchy–Schwarz on the negative-definite coordinates; no coordinate is named and there is no case split on k.

Transport onto the model

theorem CategoryTheory.Triangulated.WeakStabilityCondition.StabilityCondition.Wall.Divisorial.hodgeDefinite_of_equiv_diagonal {D : Type w} [AddCommGroup D] [Module ℝ D] {S : DivisorSpace D} {k : ℕ} (f : D ≃ₗ[ℝ] DiagonalDivisor k) (hf : ∀ (x y : D), (diagonalSpace k).pair (f x) (f y) = S.pair x y) {w : D} (hw : 0 < S.pair w w) : S.HodgeDefinite w

A DivisorSpace that admits a form-preserving linear equivalence onto the diagonal model inherits its Hodge certificates, so a concrete model need not prove its own Hodge index inequality.