Stepanov auxiliaries at places of degree at most two

At a degree-two place the strict-level filtration can jump by two. Choosing one section per strict level for both tensor factors therefore loses the factor of two needed by the Stepanov dimension count. The first factor still uses bounded distinct pole-order digits, while the second factor is now a full basis of its one-point Riemann space. The basis-grid theorem proves that the first restriction remains injective.

With ell = #K - 1 and m = #K + 2g, the same large-field hypothesis as in the degree-one construction makes the coefficient dimension exceed the second restriction target for every place degree r ≤ 2.

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreeTwoAuxiliaryConstantAlgebra (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 one point stepanov degree two auxiliary construction.

Equations

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

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

theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_finrank_upper (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 : CorvajaZannier.FiniteExtensionPlace K L) (hconstants : algebraicClosure K L = ⊥) (N : ℕ) : Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N) ≤ N * CorvajaZannier.finiteExtensionPlaceDegree K L P + 1

The one-point Riemann space at level N has dimension at most N * degree(P) + 1 when the constants are exactly K.

theorem BGS.HasseWeil.stepanov_dimension_inequality_degree_le_two {g s r : ℕ} (hlarge : (g + 1) * (g + 2) ≤ s) (hrpos : 0 < r) (hrle : r ≤ 2) : r * (s * stepanovEll s + stepanovM g s) + 1 < (stepanovEll s + 1 - g) * (r * stepanovM g s + 1 - g)

The full-basis Stepanov coefficient space beats the target dimension at every positive place degree at most two.

theorem BGS.HasseWeil.exists_onePointStepanovBasisAuxiliary_of_degree_le_two (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 : CorvajaZannier.FiniteExtensionPlace K L) (g : ℕ) (hconstants : algebraicClosure K L = ⊥) (hdegreeLe : CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ 2) (hriemann : ∀ (N : ℕ), N * CorvajaZannier.finiteExtensionPlaceDegree K L P + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K 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; have V := CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m; ∃ (u : Option (Fin (ell - g)) → L) (du : Option (Fin (ell - g)) → ℕ) (v : Fin (Module.finrank K ↥V) → L) (c : Option (Fin (ell - g)) × Fin (Module.finrank K ↥V) →₀ K), (∀ (i : Option (Fin (ell - g))), u i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) ∧ (∀ (i : Option (Fin (ell - g))), u i ≠ 0) ∧ (∀ (i : Option (Fin (ell - g))), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (u i)) P = -↑(du i)) ∧ Function.Injective du ∧ (∀ (i : Option (Fin (ell - g))), du i ≤ ell) ∧ LinearIndependent K u ∧ (∀ (j : Fin (Module.finrank K ↥V)), v j ∈ V) ∧ LinearIndependent K v ∧ c ≠ 0 ∧ (onePointStepanovSecondRestrictionMap K L u v s) c = 0 ∧ (onePointStepanovFirstRestrictionMap K L u v s) c ≠ 0

A Riemann lower bound at a place of degree at most two produces a nonzero Stepanov coefficient grid. The first family has bounded distinct pole orders; the second family is a full basis of L(mP).

The returned second restriction equality is in the ambient function field, so it can be consumed directly by the local square-Frobenius vanishing argument.