A sharp one-point Stepanov auxiliary over a square constant field #
The function field is defined over the full square field S, so an
S-rational normalization point is a place of degree one. The integer
s = #K, for a quadratic subfield K, is used only as the half-Frobenius
scale. This keeps both the Riemann-space dimension count and the final pole
height sharp.
@[instance_reducible]
noncomputable def
BGS.HasseWeil.squareFieldAuxiliaryConstantAlgebra
(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 square field stepanov auxiliary
construction.
Equations
- BGS.HasseWeil.squareFieldAuxiliaryConstantAlgebra S L = ((algebraMap (RatFunc S) L).comp (algebraMap S (RatFunc S))).toAlgebra
Instances For
theorem
BGS.HasseWeil.squareFieldAuxiliaryConstantTower
(S : Type u_2)
[Field S]
(L : Type u_3)
[Field L]
[Algebra (RatFunc S) L]
:
IsScalarTower S (RatFunc S) L
theorem
BGS.HasseWeil.exists_squareField_onePointStepanovAuxiliary_of_degree_one
(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]
(P : CorvajaZannier.FiniteExtensionPlace S L)
(g : ℕ)
(hconstants : algebraicClosure S L = ⊥)
(hdegree : CorvajaZannier.finiteExtensionPlaceDegree S L P = 1)
(hriemann : ∀ (N : ℕ), N + 1 ≤ Module.finrank S ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P N) + g)
(hlarge : (g + 1) * (g + 2) ≤ Fintype.card K)
:
have s := Fintype.card K;
have ell := stepanovEll s;
have m := stepanovM g s;
∃ (u : Option (Fin (ell - g)) → L) (du : Option (Fin (ell - g)) → ℕ) (v : Option (Fin (m - g)) → L) (dv :
Option (Fin (m - g)) → ℕ) (c : Option (Fin (ell - g)) × Option (Fin (m - g)) →₀ S),
onePointSectionFamilySpec S L P ell u du ∧ onePointSectionFamilySpec S L P m v dv ∧ c ≠ 0 ∧ (onePointStepanovSecondRestrictionMap S L u v s) c = 0 ∧ squareFieldStepanovFirstRestriction K S L u v c ≠ 0
Riemann's inequality at a degree-one place, together with the standard large-square-field condition, produces the semilinear Stepanov auxiliary.