The degree-one plane Stepanov auxiliary #

This file assembles the one-point ingredients of the Bombieri--Stepanov construction for an absolutely irreducible bivariate plane curve.

The plane monomial theorem initially gives the coarse Riemann lower bound only along an explicit arithmetic progression of pole levels. Since the progression has positive step, every level lies below a later progression level. The one-place increment estimate therefore transports the lower bound back to every level. Exact constants then force enough strict levels to select the two section families prescribed by stepanovEll and stepanovM.

At a degree-one selected place, the target Riemann space has dimension at most its pole budget plus one. The existing numerical parameter inequality then gives a nonzero coefficient grid killed by the second Frobenius restriction and detected by the first.

The degree-one hypothesis is deliberately an implication in the final theorem. This module does not assert that the controlled infinity place has degree one, and it does not count square-extension points.

source

@[instance_reducible]

noncomputable def BGS.HasseWeil.planeStepanovConstantAlgebra (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 plane stepanov auxiliary construction.

Equations

BGS.HasseWeil.planeStepanovConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

Instances For

source

theorem BGS.HasseWeil.planeStepanovConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] :

IsScalarTower K (RatFunc K) L

source

def BGS.HasseWeil.onePointSectionFamilySpec (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] {α : Type u_3} (P : CorvajaZannier.FiniteExtensionPlace K L) (N : ℕ) (f : α → L) (d : α → ℕ) :

Prop

The data furnished by strict-level section selection at pole budget N: nonzero sections with distinct exact pole orders, bounded digits, and linear independence.

Equations

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

Instances For

source

def BGS.HasseWeil.onePointStepanovAuxiliarySpec (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) (c : α × β →₀ K) :

Prop

A coefficient grid is a Stepanov auxiliary when it is nonzero, is killed by the swapped restriction, and gives a nonzero function under the first restriction.

Equations

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

Instances For

source

theorem BGS.HasseWeil.exists_planeCurve_onePointStepanovAuxiliary_of_degree_one (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {F : MvPolynomial (Fin 2) K} (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) F)) (hpartialFirst : (MvPolynomial.pderiv 0) F ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) F ≠ 0) (hlarge : have genusBudget := planeCurveBidegreeGenusBudget F; (genusBudget + 1) * (genusBudget + 2) ≤ Fintype.card K) :

Conditional degree-one Stepanov auxiliary for a plane curve.

For an absolutely irreducible bivariate plane equation with both coordinate partials nonzero, this theorem chooses the controlled infinity place from the plane monomial argument and retains its positive pole coefficient and degree bound. If that selected place has degree one, then for

g = (degreeOf 0 F - 1) * (degreeOf 1 F - 1), s = #K, ell = s - 1, and m = s + 2g,

it produces two strict-level section families and a nonzero coefficient grid whose second Stepanov restriction vanishes while its first restriction is a nonzero function.

The implication on the degree-one equality is essential: no existence of a degree-one place is claimed here.

Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.PlaneStepanovAuxiliary

The degree-one plane Stepanov auxiliary #