Riemann's inequality at finite plane-curve places

Weak approximation lifts a basis of the principal parts at one finite place to global functions regular at every other finite place. A common effective divisor above infinity absorbs the remaining poles. The resulting principal-part map is surjective, so rank-nullity contributes exactly N * degree(q) new dimensions over the infinity-supported Riemann space.

The infinity-supported bidegree Riemann inequality and the effective-divisor increment upper bound then cancel the auxiliary infinity divisor. This gives Riemann's inequality for L(N q) at every finite exhaustive place.

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteRiemannConstantAlgebra (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 plane finite place riemann lower construction.

Equations

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteRiemannPolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the plane finite place riemann lower construction.

Equations

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

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

theorem BGS.HasseWeil.finiteRiemannClosureIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteRiemannClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteRiemannPolynomialTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.finiteRiemannClosureTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteRiemannClosureDedekind (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteRiemannClosureFractionRing (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)) L

theorem BGS.HasseWeil.mem_finiteExtensionLocalPoleSpace_zero_of_valuation_le_one (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] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (x : L) (hx : (IsDedekindDomain.HeightOneSpectrum.valuation L q) x ≤ 1) : x ∈ finiteExtensionLocalPoleSpace K L (Sum.inl q) 0

theorem BGS.HasseWeil.exists_global_finitePrincipalPart_representative (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] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (N : ℕ) (p : ↥(finiteExtensionLocalPoleSpace K L (Sum.inl q) N) ⧸ relativeSubmodule (finiteExtensionLocalPoleSpace K L (Sum.inl q) 0) (finiteExtensionLocalPoleSpace K L (Sum.inl q) N)) : ∃ (z : ↥(finiteExtensionLocalPoleSpace K L (Sum.inl q) N)), Submodule.Quotient.mk z = p ∧ ∀ (q' : CorvajaZannier.FiniteExtensionFinitePlace K L), q' ≠ q → ↑z ∈ finiteExtensionLocalPoleSpace K L (Sum.inl q') 0

noncomputable def BGS.HasseWeil.finiteExtensionDivisorInfinityPart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) : CorvajaZannier.FiniteExtensionDivisor K L

The part of an exhaustive divisor supported at infinity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorInfinityPart_inl (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (q : CorvajaZannier.FiniteExtensionFinitePlace K L) : (finiteExtensionDivisorInfinityPart K L D) (Sum.inl q) = 0

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorInfinityPart_inr (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : CorvajaZannier.FiniteExtensionDivisor K L) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : (finiteExtensionDivisorInfinityPart K L D) (Sum.inr P) = D (Sum.inr P)

theorem BGS.HasseWeil.exists_infinityDivisor_finitePlacePrincipalParts_rank (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] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (N : ℕ) (hN : 0 < N) : ∃ (E : CorvajaZannier.FiniteExtensionDivisor K L), (∀ (v : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ E v) ∧ (∀ (q' : CorvajaZannier.FiniteExtensionFinitePlace K L), E (Sum.inl q') = 0) ∧ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L E) + N * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q) ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionRiemannSpace K L (Finsupp.single (Sum.inl q) ↑N + E))

theorem BGS.HasseWeil.planeCurve_finitePlace_riemann_lower {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : have hx := ⋯; ∀ (q : CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)) (N : ℕ), N * CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl q) + 1 ≤ Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl q) N) + planeCurveBidegreeGenusBudget f

Bidegree Riemann inequality at an arbitrary finite exhaustive place of an irreducible plane curve.