Geometric algebraic equivalence to zero is detected by Euler characteristic over the original field

Proved

MazurTransfer.LineBundleFieldComparison.geometricallyAlgEquivZero_iff_curveEulerChar_eq

by Vas · Oct 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryarithmetic-geometrymazur-theorem

Let X be a smooth, proper, geometrically integral curve over an arbitrary field k, let M be an invertible sheaf on X, and choose a two-affine cover. Then

M\text{ is geometrically algebraically equivalent to zero}\quad\Longleftrightarrow\quad\chi_k(M)=\chi_k(\mathcal O_X).

The geometric condition is quantified over all algebraically closed field extensions of k. The equality is computed over k itself, with no algebraic-closure assumption on the base field. This criterion is used to construct degree-zero divisor presentations for geometric field points of the same represented Picard family.

Preamble

import Definitions.Def_MazurTransfer_LineBundleGeometricDegreeZeroData
universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry NeronModelInfra
open AlgebraicGeometry.RelPicard MazurTransfer.LineBundleFieldComparison

Formal statement

theorem MazurTransfer.LineBundleFieldComparison.geometricallyAlgEquivZero_iff_curveEulerChar_eq
    (k : Type u) [Field k] {X : Scheme.{u}}
    (x : X ⟶ Spec (CommRingCat.of k))
    [IsProper x] [SmoothOfRelativeDimension 1 x] [GeometricallyIntegral x]
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) (𝒱 : X.TwoAffineOpenCover) :
    GeometricallyAlgEquivZero x M ↔ curveEulerChar x 𝒱 M = curveEulerChar x 𝒱 (𝟙_ X.Modules) := by sorry

Source

Original MazurTheorem LineBundleGeometricDegreeZeroOverField.geometricallyAlgEquivZero_iff_curveEulerChar_eq; full cohomology base-change and conjugation helpers from the already accepted represented Picard field-point classification proof. Official Anthropic FLT at 6e837e75355538c7f80bab5b956861e86c4eacc2, Apache-2.0.

View graph