Effective increments of exhaustive Riemann spaces

The local finite- and infinity-place residue maps give the same one-place dimension bound. This file first packages those two cases as a bound for an arbitrary exhaustive place, then iterates over the coefficients and support of an effective divisor.

The final statements split an effective divisor at one selected place. They are the linear-algebraic codimension estimates needed to pass from a many-pole auxiliary space to a one-point Riemann space.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_place_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (P : CorvajaZannier.FiniteExtensionPlace K L) [Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)] : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single P 1)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single P 1)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) + CorvajaZannier.finiteExtensionPlaceDegree K L P

The finite- and infinity-place increment lemmas together cover every place in the exhaustive place type.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_natPlace_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) [Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)] : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single P ↑n)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + Finsupp.single P ↑n)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) + n * CorvajaZannier.finiteExtensionPlaceDegree K L P

Adding n copies of one place raises dimension by at most n times the degree of that place.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_add_effective (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] (D E : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (hE : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ E v) [Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)] : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + E)) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (D + E)) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) + (CorvajaZannier.finiteExtensionDivisorDegree K L E).toNat

Adding an effective divisor to an effective starting divisor preserves finite-dimensionality, and its total dimension cost is at most its degree.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_effective_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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) : Module.Finite K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D)

Every effective exhaustive divisor has a finite-dimensional Riemann space.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_finrank_le_onePoint_add_degreeAway (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (P : CorvajaZannier.FiniteExtensionPlace K L) : Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (D P).toNat) + (CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionDivisorAway K L D P)).toNat

Splitting an effective divisor at P, the discarded poles cost at most the degree of the away part.

theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_finrank_lowerBound (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] (D : CorvajaZannier.FiniteExtensionDivisor K L) (hD : ∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D v) (P : CorvajaZannier.FiniteExtensionPlace K L) : Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L D) - (CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionDivisorAway K L D P)).toNat ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (D P).toNat)

Rearranged form of the away-degree estimate: the selected one-point space retains at least the full dimension minus the away degree.