Riemann spaces for finite extensions of a rational function field

This file supplies the elementary divisor-linear-algebra layer needed by a Bombieri--Stepanov proof of Hasse--Weil. For a divisor D on the exhaustive finite and infinite places of a finite separable extension L / K(X), it defines the Riemann space

L(D) = {x : L | x = 0 or div(x) + D is effective}

as a K-submodule of L. It also proves the order-theoretic and multiplicative properties of these spaces, together with their specialization to the one-point filtration L(nP).

The integer-valued principal-divisor API is defined only for nonzero elements, so zero is an explicit branch of the carrier predicate. Scalar closure uses that a nonzero constant over the finite constant field has trivial principal divisor.

Two substantive stages are deliberately not postulated here:

• finite-dimensionality of every L(D) over K;
• the Riemann--Roch lower bound, which can be stated without introducing genus as 2 * deg D - deg K_can <= 2 * finrank_K L(D).

The ambient function field L is not finite-dimensional over K, so the first item is a genuine theorem and cannot be obtained by typeclass inference from the ambient space. Both stages must be proved before finrank is used in the Hasse--Weil argument.

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.finiteExtensionRiemannSpaceConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the finite extension riemann space construction.

Equations

• BGS.CorvajaZannier.finiteExtensionRiemannSpaceConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.CorvajaZannier.finiteExtensionRiemannSpaceConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

@[reducible, inline]

abbrev BGS.CorvajaZannier.FiniteExtensionDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Type u_2

A finitely supported divisor on all finite and infinite places of L / K(X).

Equations

• BGS.CorvajaZannier.FiniteExtensionDivisor K L = (BGS.CorvajaZannier.FiniteExtensionPlace K L →₀ ℤ)

theorem BGS.CorvajaZannier.finiteExtensionDivisorDegree_add (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D E : FiniteExtensionDivisor K L) : finiteExtensionDivisorDegree K L (D + E) = finiteExtensionDivisorDegree K L D + finiteExtensionDivisorDegree K L E

Divisor degree is additive.

theorem BGS.CorvajaZannier.finiteExtensionDivisorDegree_principal (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : finiteExtensionDivisorDegree K L (finiteExtensionPrincipalDivisor K L x) = 0

The product formula says that every nonzero principal divisor has degree zero.

theorem BGS.CorvajaZannier.finiteExtensionDivisorDegree_nonnegative_of_effective (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionDivisor K L) (hD : ∀ (v : FiniteExtensionPlace K L), 0 ≤ D v) : 0 ≤ finiteExtensionDivisorDegree K L D

An effective divisor has nonnegative degree.

theorem BGS.CorvajaZannier.finiteExtensionPrincipalDivisor_algebraMap_constant (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (c : K) (hc : c ≠ 0) : finiteExtensionPrincipalDivisor K L ((algebraMap K L) c) = 0

Nonzero elements of the finite constant field have trivial exhaustive principal divisor.

def BGS.CorvajaZannier.finiteExtensionRiemannSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (D : FiniteExtensionDivisor K L) : Submodule K L

The all-place Riemann space L(D). Zero is handled separately because the existing principal-divisor API assigns integer coefficients only to nonzero functions.

Equations

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

theorem BGS.CorvajaZannier.mem_finiteExtensionRiemannSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D : FiniteExtensionDivisor K L} {x : L} : x ∈ finiteExtensionRiemannSpace K L D ↔ x = 0 ∨ x ≠ 0 ∧ ∀ (v : FiniteExtensionPlace K L), 0 ≤ (finiteExtensionPrincipalDivisor K L x) v + D v

theorem BGS.CorvajaZannier.finiteExtensionRiemannSpace_mono (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D E : FiniteExtensionDivisor K L} (hDE : D ≤ E) : finiteExtensionRiemannSpace K L D ≤ finiteExtensionRiemannSpace K L E

Increasing the allowed divisor enlarges the Riemann space.

theorem BGS.CorvajaZannier.algebraMap_mem_finiteExtensionRiemannSpace_of_effective (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D : FiniteExtensionDivisor K L} (hD : ∀ (v : FiniteExtensionPlace K L), 0 ≤ D v) (c : K) : (algebraMap K L) c ∈ finiteExtensionRiemannSpace K L D

Every constant belongs to L(D) when D is effective.

theorem BGS.CorvajaZannier.finiteExtensionRiemannSpace_mul_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D E : FiniteExtensionDivisor K L} {x y : L} (hx : x ∈ finiteExtensionRiemannSpace K L D) (hy : y ∈ finiteExtensionRiemannSpace K L E) : x * y ∈ finiteExtensionRiemannSpace K L (D + E)

The Riemann spaces form a multiplicative divisor filtration.

theorem BGS.CorvajaZannier.finiteExtensionRiemannSpace_pow_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D : FiniteExtensionDivisor K L} {x : L} (hx : x ∈ finiteExtensionRiemannSpace K L D) (n : ℕ) : x ^ n ∈ finiteExtensionRiemannSpace K L (n • D)

Powers respect the multiplicative divisor filtration.

theorem BGS.CorvajaZannier.finiteExtensionRiemannSpace_eq_bot_of_divisorDegree_neg (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {D : FiniteExtensionDivisor K L} (hD : finiteExtensionDivisorDegree K L D < 0) : finiteExtensionRiemannSpace K L D = ⊥

The elementary vanishing half of Riemann--Roch: a divisor of negative degree has no nonzero section. This uses only effectiveness and the product formula, not Riemann--Roch.

noncomputable def BGS.CorvajaZannier.finiteExtensionOnePointRiemannSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (n : ℕ) : Submodule K L

Functions whose only permitted pole is at P, with order at most n.

Equations

• BGS.CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n = BGS.CorvajaZannier.finiteExtensionRiemannSpace K L (Finsupp.single P ↑n)

theorem BGS.CorvajaZannier.mem_finiteExtensionOnePointRiemannSpace_iff (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (n : ℕ) (x : L) : x ∈ finiteExtensionOnePointRiemannSpace K L P n ↔ x = 0 ∨ x ≠ 0 ∧ -↑n ≤ (finiteExtensionPrincipalDivisor K L x) P ∧ ∀ (v : FiniteExtensionPlace K L), v ≠ P → 0 ≤ (finiteExtensionPrincipalDivisor K L x) v

Membership in L(nP) is the expected pole bound at P, together with regularity at every other place.

theorem BGS.CorvajaZannier.algebraMap_mem_finiteExtensionOnePointRiemannSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) (n : ℕ) (c : K) : (algebraMap K L) c ∈ finiteExtensionOnePointRiemannSpace K L P n

Every constant belongs to every one-point Riemann space.

theorem BGS.CorvajaZannier.finiteExtensionOnePointRiemannSpace_mono (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) {m n : ℕ} (hmn : m ≤ n) : finiteExtensionOnePointRiemannSpace K L P m ≤ finiteExtensionOnePointRiemannSpace K L P n

The one-point Riemann spaces are nested by pole order.

theorem BGS.CorvajaZannier.finiteExtensionOnePointRiemannSpace_mul_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : FiniteExtensionPlace K L) {m n : ℕ} {x y : L} (hx : x ∈ finiteExtensionOnePointRiemannSpace K L P m) (hy : y ∈ finiteExtensionOnePointRiemannSpace K L P n) : x * y ∈ finiteExtensionOnePointRiemannSpace K L P (m + n)

Products add the allowed pole orders in the one-point filtration.