Documentation

LeanPool.MarkoffModP.BGS.HasseWeil.OnePointIncrement

Successive growth of one-point Riemann spaces #

The local residue argument bounds the jump from L(nP) to L((n+1)P) by the degree of P. Iterating from L(0) also supplies finite-dimensionality at every level of the one-point filtration.

source
theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_increment (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 : ℕ) [Module.Finite K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n)] :
Module.Finite K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (n + 1)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (n + 1)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) + CorvajaZannier.finiteExtensionPlaceDegree K L P

One step in the one-point filtration is finite-dimensional and has dimension jump at most the degree of the distinguished place.

source
theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_moduleFinite (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 : ℕ) :
Module.Finite K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n)

Every member of a one-point Riemann filtration is finite-dimensional.

source
theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_finrank_succ_le (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 : ℕ) :
Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (n + 1)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) + CorvajaZannier.finiteExtensionPlaceDegree K L P

Uniform dimension-jump bound for the one-point filtration.