Selecting one-point sections with distinct pole orders

The local jump bound converts a Riemann-space dimension lower bound into many strict levels of the pole filtration. Choosing one section at each strict level, and adjoining the constant section, produces a linearly independent family with distinct pole-order digits in a prescribed range.

@[instance_reducible]

noncomputable def BGS.HasseWeil.sectionSelectionConstantAlgebra (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 section selection construction.

Equations

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

theorem BGS.HasseWeil.sectionSelectionConstantTower (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_zero_finrank (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 = ⊥) : Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P 0) = 1

With exact constants, the initial one-point Riemann space has dimension one.

theorem BGS.HasseWeil.le_card_onePointStrictLevels_of_finrank_lower (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) (N m : ℕ) (hconstants : algebraicClosure K L = ⊥) (hlower : 1 + CorvajaZannier.finiteExtensionPlaceDegree K L P * m ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N)) : m ≤ (strictFiltrationLevels (fun (n : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) N).card

A final dimension lower bound forces the stated number of strict levels in the one-point filtration.

theorem BGS.HasseWeil.exists_onePointSections_of_le_card_strictLevels (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) (N m : ℕ) (hm : m ≤ (strictFiltrationLevels (fun (n : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) N).card) : ∃ (f : Fin m → L) (d : Fin m → ℕ), (∀ (i : Fin m), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N) ∧ (∀ (i : Fin m), f i ≠ 0) ∧ (∀ (i : Fin m), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P = -↑(d i)) ∧ Function.Injective d ∧ (∀ (i : Fin m), 0 < d i ∧ d i ≤ N) ∧ LinearIndependent K f

Select a prescribed number of positive-pole sections from the strict levels below N.

theorem BGS.HasseWeil.exists_onePointSectionsWithConstant_of_le_card_strictLevels (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) (N m : ℕ) (hm : m ≤ (strictFiltrationLevels (fun (n : ℕ) => CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) N).card) : ∃ (f : Option (Fin m) → L) (d : Option (Fin m) → ℕ), (∀ (i : Option (Fin m)), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P N) ∧ (∀ (i : Option (Fin m)), f i ≠ 0) ∧ (∀ (i : Option (Fin m)), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P = -↑(d i)) ∧ Function.Injective d ∧ (∀ (i : Option (Fin m)), d i ≤ N) ∧ LinearIndependent K f

Adjoin the constant section to a selected positive-pole family. The resulting pole digits start at zero and remain pairwise distinct.