A square-field Stepanov bound for arbitrary function fields

The one-point Stepanov construction is intrinsic to a finite separable extension of a rational function field. This file applies it to the complete type of degree-one places, rather than to the regular affine points of a chosen plane model.

Choose one rational place as the pole. Every rational finite place away from it is a zero-counting place; at most one rational finite place is omitted. The rational places above infinity contribute at most the degree of the function-field extension, by the fundamental ramification-inertia equality. This gives a uniform estimate suitable for the Frobenius fixed-field twists.

@[instance_reducible]

noncomputable def BGS.HasseWeil.generalSquareFieldConstantAlgebra (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra S L

The algebra structure from S to L used in the general square field stepanov count construction.

Equations

• BGS.HasseWeil.generalSquareFieldConstantAlgebra S L = ((algebraMap (RatFunc S) L).comp (algebraMap S (RatFunc S))).toAlgebra

theorem BGS.HasseWeil.generalSquareFieldConstantTower (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : IsScalarTower S (RatFunc S) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.generalSquareFieldInfinityAlgebra (S : Type u_2) [Field S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra (↥(CorvajaZannier.RatFuncInfinityIntegers S)) L

The algebra structure from (RatFuncInfinityIntegers S) to L used in the general square field stepanov count construction.

Equations

• BGS.HasseWeil.generalSquareFieldInfinityAlgebra S L = Algebra.ofSubsemiring (BGS.CorvajaZannier.RatFuncInfinityIntegers S)

theorem BGS.HasseWeil.generalSquareFieldInfinityModuleFinite (S : Type u_2) [Field S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers S) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)

theorem BGS.HasseWeil.generalSquareFieldInfinityIntegral (S : Type u_2) [Field S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers S) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)

theorem BGS.HasseWeil.generalSquareFieldInfinityTorsionFree (S : Type u_2) [Field S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers S) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)

theorem BGS.HasseWeil.generalSquareFieldInfinityDedekind (S : Type u_2) [Field S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncInfinityIntegralClosure S L)

theorem BGS.HasseWeil.rationalInfinityPlace_card_le_finrank (S : Type u_2) [Field S] [DecidableEq S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] : Nat.card (FiniteExtensionRationalInfinityPlace S L) ≤ Module.finrank (RatFunc S) L

The number of rational places above infinity is at most the function-field degree.

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_le_squareFieldStepanov_of_finitePlaceRiemann (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Fintype S] [DecidableEq S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] (g : ℕ) (hcard : Fintype.card S = Fintype.card K ^ 2) (hconstants : algebraicClosure S L = ⊥) (hriemann : ∀ (Q : FiniteExtensionRationalFinitePlace S L) (N : ℕ), N + 1 ≤ Module.finrank S ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace S L (Sum.inl ↑Q) N) + g) (hlarge : (g + 1) * (g + 2) ≤ Fintype.card K) : finiteExtensionRationalPlaceCount S L ≤ Fintype.card S + (2 * g + 1) * Fintype.card K + Module.finrank (RatFunc S) L

The intrinsic one-point square-field Stepanov bound for all degree-one places of a finite separable function field, using Riemann's inequality only at rational finite places.

If a rational finite place exists, it is chosen as the pole in the Stepanov construction. If none exists, all rational places lie above infinity and the fundamental ramification--inertia equality gives the required bound directly. Thus no Riemann inequality at an infinity place is needed.

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_le_squareFieldStepanov (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Fintype S] [DecidableEq S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] (g : ℕ) (hcard : Fintype.card S = Fintype.card K ^ 2) (hconstants : algebraicClosure S L = ⊥) (hriemann : ∀ (P : CorvajaZannier.FiniteExtensionPlace S L), CorvajaZannier.finiteExtensionPlaceDegree S L P = 1 → ∀ (N : ℕ), N + 1 ≤ Module.finrank S ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P N) + g) (hlarge : (g + 1) * (g + 2) ≤ Fintype.card K) : finiteExtensionRationalPlaceCount S L ≤ Fintype.card S + (2 * g + 1) * Fintype.card K + Module.finrank (RatFunc S) L

The intrinsic one-point square-field Stepanov bound for all degree-one places of a finite separable function field.

This compatibility wrapper preserves the original API. Its stronger hypothesis supplies the finite-place Riemann inequalities required by finiteExtensionRationalPlaceCount_le_squareFieldStepanov_of_finitePlaceRiemann.