Riemann--Roch for the exhaustive finite-extension place model

This file identifies the exhaustive finite and infinite places used by the BGS function-field development with the two-chart place model of the vendored Riemann--Roch library. The identification transports residue degrees, divisors, divisor degree, normalized valuations, and Riemann spaces. It then applies the axiom-clean Riemann--Roch theorem to discharge the eventual uniform Riemann formula required by the divisor-class recurrence.

The only non-definitional chart issue is at infinity: the two developments construct the same valuation subring using different DecidableEq instances. We therefore record the identity-on-elements ring equivalence explicitly and transport the integral closure and its height-one primes across it.

@[instance_reducible]

noncomputable def BGS.HasseWeil.riemannRochConstantAlgebra (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 finite extension riemann roch construction.

Equations

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

theorem BGS.HasseWeil.riemannRochConstantRatFuncTower (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.riemannRochPolynomialAlgebra (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 finite extension riemann roch construction.

Equations

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

theorem BGS.HasseWeil.riemannRochPolynomialRatFuncTower (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.riemannRochConstantPolynomialTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.riemannRochInfinityBaseConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegers K)

The algebra structure from K to (RatFuncInfinityIntegers K) used in the finite extension riemann roch construction.

Equations

• BGS.HasseWeil.riemannRochInfinityBaseConstantAlgebra K = (BGS.CorvajaZannier.ratFuncInfinityConstantRingHom K).toAlgebra

theorem BGS.HasseWeil.riemannRochInfinityClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.riemannRochInfinityClosureIsIntegral (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

theorem BGS.HasseWeil.riemannRochInfinityBaseTorsionFreeTop (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (↥(CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.HasseWeil.riemannRochInfinityClosureIsTorsionFree (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

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

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.riemannRochInfinityClosureConstantAlgebra (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

The algebra structure from K to (RatFuncInfinityIntegralClosure K L) used in the finite extension riemann roch construction.

Equations

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

theorem BGS.HasseWeil.riemannRochInfinityClosureConstantTower (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

def BGS.HasseWeil.finiteExtensionInfinityBaseRingEquiv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : ↥(CorvajaZannier.RatFuncInfinityIntegers K) ≃+* ↥(MarkoffRiemannRoch.FunctionField.Chart.inftyValuationSubring K)

The BGS and Riemann--Roch infinity valuation subrings are the same subring of RatFunc K; this equivalence makes the harmless instance-level difference explicit.

Equations

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

@[simp]

theorem BGS.HasseWeil.finiteExtensionInfinityBaseRingEquiv_apply_coe (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (x : ↥(CorvajaZannier.RatFuncInfinityIntegers K)) : ↑((finiteExtensionInfinityBaseRingEquiv K) x) = ↑x

def BGS.HasseWeil.finiteExtensionInfinityIntegralClosureRingEquiv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L) ≃+* ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K L)

Identity-on-L equivalence between the two infinity integral closures.

Equations

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

@[simp]

theorem BGS.HasseWeil.finiteExtensionInfinityIntegralClosureRingEquiv_apply_coe (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (x : ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)) : ↑((finiteExtensionInfinityIntegralClosureRingEquiv K L) x) = ↑x

def BGS.HasseWeil.finiteExtensionInfinityIntegralClosureAlgEquiv (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L) ≃ₐ[K] ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K L)

Constant-field-linear form of the infinity integral-closure equivalence.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionInfinityPrimesOverEquivHeightOne (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L) ≃ IsDedekindDomain.HeightOneSpectrum ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

Places above the BGS infinity place are exactly the height-one primes of the BGS infinity integral closure.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionInfinityPlaceEquivChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L) ≃ IsDedekindDomain.HeightOneSpectrum ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K L)

Infinity places in the exhaustive BGS model and in the Riemann--Roch chart.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionPlaceEquivChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : CorvajaZannier.FiniteExtensionPlace K L ≃ MarkoffRiemannRoch.FunctionField.Chart.PlaceA K L

Equivalence from the exhaustive BGS place type to the Riemann--Roch two-chart place type.

Equations

• BGS.HasseWeil.finiteExtensionPlaceEquivChart K L = (Equiv.refl (BGS.CorvajaZannier.FiniteExtensionFinitePlace K L)).sumCongr (BGS.HasseWeil.finiteExtensionInfinityPlaceEquivChart K L)

noncomputable def BGS.HasseWeil.finiteExtensionFiniteQuotientResidueAlgEquiv (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] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) : (↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L) ⧸ q.asIdeal) ≃ₐ[K] q.asIdeal.ResidueField

The residue-field equivalence for the finite quotient in Riemann–Roch.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionInfinityQuotientResidueAlgEquiv (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (q : IsDedekindDomain.HeightOneSpectrum ↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K L)) : (↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers K L) ⧸ q.asIdeal) ≃ₐ[K] q.asIdeal.ResidueField

The residue-field equivalence for the infinity quotient in Riemann–Roch.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionInfinityResidueAlgEquiv (K : Type u_1) [Field 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.FiniteExtensionInfinityPlace K L)) : (↑P).ResidueField ≃ₐ[K] ((finiteExtensionInfinityPlaceEquivChart K L) P).asIdeal.ResidueField

The residue-field equivalence at infinity used in the Riemann–Roch comparison.

Equations

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

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_eq_chart (K : Type u_1) [Field 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] (v : CorvajaZannier.FiniteExtensionPlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L v = MarkoffRiemannRoch.FunctionField.Chart.placeDegree K L ((finiteExtensionPlaceEquivChart K L) v)

The exhaustive place degree agrees with the Riemann--Roch chart degree.

theorem BGS.HasseWeil.finiteExtensionInfinityPlaceValuation_eq_chart (K : Type u_1) [Field 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.FiniteExtensionInfinityPlace K L)) : IsDedekindDomain.HeightOneSpectrum.valuation L (CorvajaZannier.primeOverHeightOne (CorvajaZannier.ratFuncInfinityPlace K) P) = IsDedekindDomain.HeightOneSpectrum.valuation L ((finiteExtensionInfinityPlaceEquivChart K L) P)

The normalized infinity valuation is unchanged by the identity-on-L integral-closure transport.

noncomputable def BGS.HasseWeil.finiteExtensionPlaceValuation (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : CorvajaZannier.FiniteExtensionPlace K L → Valuation L (WithZero (Multiplicative ℤ))

The normalized valuation attached to an exhaustive BGS place.

Equations

• One or more equations did not get rendered due to their size.
• BGS.HasseWeil.finiteExtensionPlaceValuation K L (Sum.inl q) = IsDedekindDomain.HeightOneSpectrum.valuation L q

theorem BGS.HasseWeil.finiteExtensionPlaceValuation_eq_chart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (v : CorvajaZannier.FiniteExtensionPlace K L) : finiteExtensionPlaceValuation K L v = MarkoffRiemannRoch.FunctionField.Chart.placeValuation K L ((finiteExtensionPlaceEquivChart K L) v)

Every exhaustive BGS place carries exactly the normalized valuation of its corresponding Riemann--Roch chart place.

noncomputable def BGS.HasseWeil.finiteExtensionDivisorEquivChart (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : CorvajaZannier.FiniteExtensionDivisor K L ≃+ MarkoffRiemannRoch.FunctionField.Chart.DivisorA K L

Transport of exhaustive divisors to the two-chart Riemann--Roch model.

Equations

• BGS.HasseWeil.finiteExtensionDivisorEquivChart K L = Finsupp.domCongr (BGS.HasseWeil.finiteExtensionPlaceEquivChart K L)

theorem BGS.HasseWeil.finiteExtensionDivisorDegree_eq_chart (K : Type u_1) [Field 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) : CorvajaZannier.finiteExtensionDivisorDegree K L D = MarkoffRiemannRoch.FunctionField.Chart.deg K L ((finiteExtensionDivisorEquivChart K L) D)

Divisor degree is preserved by the exhaustive-place/chart equivalence.

theorem BGS.HasseWeil.finiteExtensionPlaceValuation_eq_exp_neg_principalDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) (v : CorvajaZannier.FiniteExtensionPlace K L) : (finiteExtensionPlaceValuation K L v) x = WithZero.exp (-(CorvajaZannier.finiteExtensionPrincipalDivisor K L x) v)

The valuation of a nonzero function is the exponential of the negative coefficient of its exhaustive principal divisor.

theorem BGS.HasseWeil.finiteExtensionRiemannSpace_eq_chart (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) : CorvajaZannier.finiteExtensionRiemannSpace K L D = MarkoffRiemannRoch.FunctionField.Chart.RRspace K L ((finiteExtensionDivisorEquivChart K L) D)

The BGS all-place Riemann space is the Riemann--Roch chart space after transporting its divisor.

theorem BGS.HasseWeil.hasFiniteExtensionUniformEventualRiemannFormula_of_fullConstantField (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] [MarkoffRiemannRoch.FunctionField.IsFullConstantField K L] : HasFiniteExtensionUniformEventualRiemannFormula K L (MarkoffRiemannRoch.FunctionField.Chart.genus K L) (2 * MarkoffRiemannRoch.FunctionField.Chart.genus K L)

Riemann--Roch supplies the uniform eventual formula with genus g and threshold 2g once the chosen finite constant field is full in L.

theorem BGS.HasseWeil.exists_hasFiniteExtensionUniformEventualRiemannFormula_of_constants (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] (hconstants : algebraicClosure K L = ⊥) : ∃ (genus : ℕ) (threshold : ℕ), HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold

If the algebraic closure of the finite constant field inside L is exactly the constants, the uniform eventual Riemann formula holds for a canonical genus and threshold.