Divisor degree and order on a function field

This file completes the coordinate divisor API needed for Riemann–Roch spaces and adeles: place degrees, global degree, and the partial order on DivisorA.

Main definitions

• FunctionField.placeDegree: residue field dimension of a coordinate place.
• FunctionField.deg: global degree of a divisor.

The partial order on DivisorA is the pointwise order on Finsupp from Mathlib (Finsupp.le_def); no new order instance is introduced here.

@[instance_reducible]

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncDivisorFile (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

The classical decidable equality on k(X) used by the coordinate places.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.instDecidableEqRatFuncDivisorFile k = Classical.decEq (RatFunc k)

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.placeDegree (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (v : PlaceA k K) : ℕ

The degree of a coordinate place: the residue field dimension over k.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.placeDegree k K (Sum.inl w) = Module.finrank k (↥(FunctionField.ringOfIntegers k K) ⧸ w.asIdeal)
• MarkoffRiemannRoch.FunctionField.Chart.placeDegree k K (Sum.inr w) = Module.finrank k (↥(MarkoffRiemannRoch.FunctionField.Chart.infiniteIntegers k K) ⧸ w.asIdeal)

theorem MarkoffRiemannRoch.FunctionField.Chart.placeDegree_pos (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : PlaceA k K) : 0 < placeDegree k K v

Every coordinate place has strictly positive degree.

theorem MarkoffRiemannRoch.FunctionField.Chart.placeDegree_infinite_eq_inertiaDeg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : placeDegree k K (Sum.inr v) = v.asIdeal.inertiaDeg ↥(inftyValuationSubring k)

At an infinite coordinate place, the place degree is its inertia degree over the unique place at infinity of k(X).

theorem MarkoffRiemannRoch.FunctionField.Chart.placeDegree_finite_eq_base_mul_inertiaDeg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : placeDegree k K (Sum.inl v) = Module.finrank k (Polynomial k ⧸ Ideal.under (Polynomial k) v.asIdeal) * v.asIdeal.inertiaDeg (Polynomial k)

At a finite coordinate place, the place degree is the degree of the prime below times its inertia degree.

theorem MarkoffRiemannRoch.FunctionField.Chart.relNorm_asIdeal_finite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) : (Ideal.relNorm (Polynomial k)) v.asIdeal = Ideal.under (Polynomial k) v.asIdeal ^ v.asIdeal.inertiaDeg (Polynomial k)

The relative ideal norm of a finite coordinate prime has exponent equal to its inertia degree; unlike Mathlib's perfect-field version, this uses only the standing separability hypothesis.

theorem MarkoffRiemannRoch.FunctionField.Chart.relNorm_asIdeal_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : (Ideal.relNorm ↥(inftyValuationSubring k)) v.asIdeal = Ideal.under (↥(inftyValuationSubring k)) v.asIdeal ^ v.asIdeal.inertiaDeg ↥(inftyValuationSubring k)

The corresponding relative-norm formula on the infinity chart.

theorem MarkoffRiemannRoch.FunctionField.Chart.finite_factorDegree_eq_relNorm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (I : Ideal ↥(FunctionField.ringOfIntegers k K)) (hI : I ≠ ⊥) : (Multiset.map (fun (P : Ideal ↥(FunctionField.ringOfIntegers k K)) => Module.finrank k (Polynomial k ⧸ Ideal.under (Polynomial k) P) * P.inertiaDeg (Polynomial k)) (UniqueFactorizationMonoid.normalizedFactors I)).sum = (Multiset.map (fun (p : Ideal (Polynomial k)) => Module.finrank k (Polynomial k ⧸ p)) (UniqueFactorizationMonoid.normalizedFactors ((Ideal.relNorm (Polynomial k)) I))).sum

Weighted factor degree on the finite chart is preserved by relative ideal norm.

theorem MarkoffRiemannRoch.FunctionField.Chart.infinite_factorDegree_eq_relNorm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (I : Ideal ↥(infiniteIntegers k K)) (hI : I ≠ ⊥) : (Multiset.map (fun (P : Ideal ↥(infiniteIntegers k K)) => P.inertiaDeg ↥(inftyValuationSubring k)) (UniqueFactorizationMonoid.normalizedFactors I)).sum = (Multiset.map (fun (x : Ideal ↥(inftyValuationSubring k)) => 1) (UniqueFactorizationMonoid.normalizedFactors ((Ideal.relNorm ↥(inftyValuationSubring k)) I))).sum

The analogous relative-norm identity on the infinity chart.

theorem MarkoffRiemannRoch.FunctionField.Chart.polynomial_factorDegree_span (k : Type u_1) [Field k] (p : Polynomial k) (hp : p ≠ 0) : (Multiset.map (fun (P : Ideal (Polynomial k)) => Module.finrank k (Polynomial k ⧸ P)) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {p}))).sum = p.natDegree

Over the finite chart of k(X), the weighted prime-factor degree of a principal polynomial ideal is the polynomial degree.

theorem MarkoffRiemannRoch.FunctionField.Chart.infinity_factorDegree_span (k : Type u_1) [Field k] (a : ↥(inftyValuationSubring k)) (ha : a ≠ 0) : ↑(Multiset.map (fun (x : Ideal ↥(inftyValuationSubring k)) => 1) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {a}))).sum = -(↑a).intDegree

Over the infinity chart of k(X), the number of prime factors of a nonzero principal ideal is the negative rational-function degree of its generator.

theorem MarkoffRiemannRoch.FunctionField.Chart.finite_intNorm_div_eq_norm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) (n : ↥(FunctionField.ringOfIntegers k K)) (d : ↥(nonZeroDivisors ↥(FunctionField.ringOfIntegers k K))) (hnd : IsLocalization.mk' K n d = ↑x) : (algebraMap (Polynomial k) (RatFunc k)) ((Algebra.intNorm (Polynomial k) ↥(FunctionField.ringOfIntegers k K)) n) / (algebraMap (Polynomial k) (RatFunc k)) ((Algebra.intNorm (Polynomial k) ↥(FunctionField.ringOfIntegers k K)) ↑d) = (Algebra.norm (RatFunc k)) ↑x

Compatibility of integral norm on the finite chart with the field norm after passing to fraction fields.

theorem MarkoffRiemannRoch.FunctionField.Chart.infinite_intNorm_div_eq_norm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) (n : ↥(infiniteIntegers k K)) (d : ↥(nonZeroDivisors ↥(infiniteIntegers k K))) (hnd : IsLocalization.mk' K n d = ↑x) : (algebraMap (↥(inftyValuationSubring k)) (RatFunc k)) ((Algebra.intNorm ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)) n) / (algebraMap (↥(inftyValuationSubring k)) (RatFunc k)) ((Algebra.intNorm ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)) ↑d) = (Algebra.norm (RatFunc k)) ↑x

Compatibility of integral norm with field norm on the infinity chart.

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.finiteIdealWeight (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] (P : Ideal ↥(FunctionField.ringOfIntegers k K)) : ℕ

The ideal-valued weight whose restriction to finite height-one primes is placeDegree.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.finiteIdealWeight k K P = Module.finrank k (Polynomial k ⧸ Ideal.under (Polynomial k) P) * P.inertiaDeg (Polynomial k)

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.infiniteIdealWeight (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] (P : Ideal ↥(infiniteIntegers k K)) : ℕ

The ideal-valued weight whose restriction to infinite height-one primes is placeDegree.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.infiniteIdealWeight k K P = P.inertiaDeg ↥(MarkoffRiemannRoch.FunctionField.Chart.inftyValuationSubring k)

theorem MarkoffRiemannRoch.FunctionField.Chart.finitePrincipalDegree_eq_intDegree_norm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) : (Finsupp.sum (FractionalIdeal.principalDivisor (Additive.ofMul x)) fun (v : IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K)) (n : ℤ) => n * ↑(placeDegree k K (Sum.inl v))) = ((Algebra.norm (RatFunc k)) ↑x).intDegree

The finite-chart contribution of a principal divisor is the degree at infinity of the field norm.

theorem MarkoffRiemannRoch.FunctionField.Chart.infinitePrincipalDegree_eq_neg_intDegree_norm (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) : (Finsupp.sum (FractionalIdeal.principalDivisor (Additive.ofMul x)) fun (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) (n : ℤ) => n * ↑(placeDegree k K (Sum.inr v))) = -((Algebra.norm (RatFunc k)) ↑x).intDegree

The infinite-chart contribution of a principal divisor is the negative degree at infinity of the field norm.

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.placeValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : PlaceA k K) : ValuationSubring K

The valuation subring at a coordinate place.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.placeValuationSubring k K v = (MarkoffRiemannRoch.FunctionField.Chart.placeValuation k K v).valuationSubring

noncomputable def MarkoffRiemannRoch.FunctionField.Chart.deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : DivisorA k K) : ℤ

The global degree of a divisor.

Equations

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

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_principalDivisorA_eq_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Kˣ) : deg k K ((principalDivisorA k K) (Additive.ofMul x)) = 0

Product formula: the global degree of a principal divisor is zero.

def MarkoffRiemannRoch.FunctionField.Chart.support (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : DivisorA k K) : Finset (PlaceA k K)

The support of a divisor.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.support k K D = D.support

def MarkoffRiemannRoch.FunctionField.Chart.IsEffective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : DivisorA k K) : Prop

A divisor is effective when all coefficients are nonnegative.

Equations

• MarkoffRiemannRoch.FunctionField.Chart.IsEffective k K D = ∀ (v : MarkoffRiemannRoch.FunctionField.Chart.PlaceA k K), 0 ≤ D v

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : deg k K 0 = 0

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_add (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D₁ D₂ : DivisorA k K) : deg k K (D₁ + D₂) = deg k K D₁ + deg k K D₂

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_neg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D : DivisorA k K) : deg k K (-D) = -deg k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_sub (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (D D' : DivisorA k K) : deg k K (D - D') = deg k K D - deg k K D'

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_nsmul (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D : DivisorA k K} (n : ℕ) : deg k K (n • D) = ↑n * deg k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_nsmul_effective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D : DivisorA k K} (n : ℕ) (_hD : IsEffective k K D) : deg k K (n • D) = ↑n * deg k K D

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_nonneg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D : DivisorA k K} (hD : IsEffective k K D) : 0 ≤ deg k K D

Effective divisors have nonnegative degree.

theorem MarkoffRiemannRoch.FunctionField.Chart.eq_zero_of_effective_deg_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D : DivisorA k K} (hD : IsEffective k K D) (hdeg : deg k K D = 0) : D = 0

An effective divisor of degree zero is the zero divisor.

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_single (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] (v : PlaceA k K) (n : ℤ) : deg k K (Finsupp.single v n) = n * ↑(placeDegree k K v)

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_mono (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : deg k K D ≤ deg k K D'

The degree map is monotone for the pointwise order on divisors.

theorem MarkoffRiemannRoch.FunctionField.Chart.deg_nonpos (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D : DivisorA k K} (hD : D ≤ 0) : deg k K D ≤ 0

A nonpositive divisor has nonpositive degree.

theorem MarkoffRiemannRoch.FunctionField.Chart.le_iff_sub_effective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] {D D' : DivisorA k K} : D ≤ D' ↔ IsEffective k K (D' - D)