Riemann–Roch spaces L(D)

This file defines the Riemann–Roch space of a divisor on a function field and its dimension ℓ(D).

theorem FunctionField.Chart.exp_neg_mul_lt_one_iff_le (x : WithZero (Multiplicative ℤ)) (n : ℤ) : WithZero.exp (-n) * x < 1 ↔ x ≤ WithZero.exp (n - 1)

@[instance_reducible]

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

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

Equations

• FunctionField.Chart.instDecidableEqRatFuncRRspace k = Classical.decEq (RatFunc k)

theorem FunctionField.Chart.nonempty_placeA (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] : Nonempty (PlaceA k K)

def FunctionField.Chart.memRRspace (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) (f : K) : Prop

A function belongs to the Riemann–Roch space of D when its valuation at every place v is at most WithZero.exp (D v), i.e. ord_v f ≥ -D v in additive notation. The zero function belongs trivially since its valuation is 0.

Equations

• FunctionField.Chart.memRRspace k K D f = ∀ (v : FunctionField.Chart.PlaceA k K), (FunctionField.Chart.placeValuation k K v) f ≤ WithZero.exp (D v)

theorem FunctionField.Chart.memRRspace.zero_mem (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) : memRRspace k K D 0

theorem FunctionField.Chart.memRRspace.add_mem (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} {f g : K} (hf : memRRspace k K D f) (hg : memRRspace k K D g) : memRRspace k K D (f + g)

theorem FunctionField.Chart.memRRspace.smul_mem (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D : DivisorA k K} (c : k) {f : K} (hf : memRRspace k K D f) : memRRspace k K D (c • f)

theorem FunctionField.Chart.memRRspace.one_mem (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] : memRRspace k K 0 1

theorem FunctionField.Chart.memRRspace.mul_mem (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 E : DivisorA k K} {f g : K} (hf : memRRspace k K D f) (hg : memRRspace k K E g) : memRRspace k K (D + E) (f * g)

theorem FunctionField.Chart.memRRspace.memRRspace_mono (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 E : DivisorA k K} (h : D ≤ E) {f : K} (hf : memRRspace k K D f) : memRRspace k K E f

theorem FunctionField.Chart.memRRspace.pow_mem (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} {f : K} (hf : memRRspace k K D f) (n : ℕ) : memRRspace k K (n • D) (f ^ n)

def FunctionField.Chart.RRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : Submodule k K

The Riemann–Roch space L(D).

Equations

• FunctionField.Chart.RRspace k K D = { carrier := {f : K | FunctionField.Chart.memRRspace k K D f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def FunctionField.Chart.ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : ℕ

The dimension ℓ(D).

Equations

• FunctionField.Chart.ell k K D = Module.finrank k ↥(FunctionField.Chart.RRspace k K D)

@[simp]

theorem FunctionField.Chart.mem_RRspace_iff (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (f : K) : f ∈ RRspace k K D ↔ memRRspace k K D f

theorem FunctionField.Chart.RRspace_mono (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : RRspace k K D ≤ RRspace k K D'

noncomputable def FunctionField.Chart.RRspaceAddPrincipalEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (x : Kˣ) : ↥(RRspace k K (D + (principalDivisorA k K) (Additive.ofMul x))) ≃ₗ[k] ↥(RRspace k K D)

Multiplication by a nonzero function identifies L(D + (x)) with L(D).

Equations

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

theorem FunctionField.Chart.ell_add_principal (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (x : Kˣ) : ell k K (D + (principalDivisorA k K) (Additive.ofMul x)) = ell k K D

Riemann–Roch dimensions are invariant under adding a principal divisor.

noncomputable def FunctionField.Chart.finrankRRspaceDiff (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D D' : DivisorA k K) : ℕ

The rank of the quotient L(D') / L(D) (with intersection semantics when unordered).

Equations

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

noncomputable def FunctionField.Chart.finiteLocalResidueMap (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : ↥(RRspace k K (D + Finsupp.single (Sum.inl v) 1)) →ₗ[k] v.asIdeal.ResidueField

One-step local residue map at a finite coordinate place.

Equations

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

theorem FunctionField.Chart.finiteLocalResidueMap_ker (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : (finiteLocalResidueMap k K D v).ker = Submodule.comap (RRspace k K (D + Finsupp.single (Sum.inl v) 1)).subtype (RRspace k K D)

noncomputable def FunctionField.Chart.finiteResidueFieldEquiv (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 ↥(ringOfIntegers k K)) : (↥(ringOfIntegers k K) ⧸ v.asIdeal) ≃ₗ[k] v.asIdeal.ResidueField

The residue field at a finite coordinate place as a k-linear copy of the quotient ringOfIntegers k K ⧸ v.asIdeal.

Equations

• FunctionField.Chart.finiteResidueFieldEquiv k K v = LinearEquiv.ofBijective (↑k (Algebra.linearMap (↥(FunctionField.ringOfIntegers k K) ⧸ v.asIdeal) v.asIdeal.ResidueField)) ⋯

noncomputable def FunctionField.Chart.infiniteResidueFieldEquiv (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)) : (↥(infiniteIntegers k K) ⧸ v.asIdeal) ≃ₗ[k] v.asIdeal.ResidueField

The residue field at an infinite coordinate place as a k-linear copy of the quotient infiniteIntegers k K ⧸ v.asIdeal.

Equations

• FunctionField.Chart.infiniteResidueFieldEquiv k K v = LinearEquiv.ofBijective (↑k (Algebra.linearMap (↥(FunctionField.Chart.infiniteIntegers k K) ⧸ v.asIdeal) v.asIdeal.ResidueField)) ⋯

theorem FunctionField.Chart.finrankRRspaceDiff_single_finite_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : finrankRRspaceDiff k K D (D + Finsupp.single (Sum.inl v) 1) ≤ placeDegree k K (Sum.inl v)

noncomputable def FunctionField.Chart.infiniteLocalResidueMap (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : ↥(RRspace k K (D + Finsupp.single (Sum.inr v) 1)) →ₗ[k] v.asIdeal.ResidueField

One-step local residue map at an infinite coordinate place.

Equations

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

theorem FunctionField.Chart.infiniteLocalResidueMap_ker (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : (infiniteLocalResidueMap k K D v).ker = Submodule.comap (RRspace k K (D + Finsupp.single (Sum.inr v) 1)).subtype (RRspace k K D)

theorem FunctionField.Chart.finrankRRspaceDiff_single_infinite_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : finrankRRspaceDiff k K D (D + Finsupp.single (Sum.inr v) 1) ≤ placeDegree k K (Sum.inr v)

theorem FunctionField.Chart.finiteDimensional_add_single_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) [FiniteDimensional k ↥(RRspace k K D)] : FiniteDimensional k ↥(RRspace k K (D + Finsupp.single v 1))

theorem FunctionField.Chart.finiteDimensional_add_single_nat (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) (n : ℕ) [FiniteDimensional k ↥(RRspace k K D)] : FiniteDimensional k ↥(RRspace k K (D + Finsupp.single v ↑n))

theorem FunctionField.Chart.finrankRRspaceDiff_add_finrank_of_finite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') [FiniteDimensional k ↥(RRspace k K D')] : finrankRRspaceDiff k K D D' + Module.finrank k ↥(RRspace k K D) = Module.finrank k ↥(RRspace k K D')

theorem FunctionField.Chart.finrankRRspaceDiff_single_one_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) : finrankRRspaceDiff k K D (D + Finsupp.single v 1) ≤ placeDegree k K v

theorem FunctionField.Chart.finrankRRspaceDiff_single_nat_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) (v : PlaceA k K) (n : ℕ) [FiniteDimensional k ↥(RRspace k K D)] : finrankRRspaceDiff k K D (D + Finsupp.single v ↑n) ≤ n * placeDegree k K v

theorem FunctionField.Chart.finiteDimensional_add_effective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) (hE : IsEffective k K E) [FiniteDimensional k ↥(RRspace k K D)] : FiniteDimensional k ↥(RRspace k K (D + E))

theorem FunctionField.Chart.finrankRRspaceDiff_add_effective_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D E : DivisorA k K) (hE : IsEffective k K E) [FiniteDimensional k ↥(RRspace k K D)] : finrankRRspaceDiff k K D (D + E) ≤ (deg k K E).toNat

theorem FunctionField.Chart.deg_principalDivisor_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

theorem FunctionField.Chart.RRspace_neg_deg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D : DivisorA k K} (h : deg k K D < 0) : RRspace k K D = ⊥

theorem FunctionField.Chart.RRspace_neg_deg_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D : DivisorA k K} (h : deg k K D < 0) : ell k K D = 0

theorem FunctionField.Chart.finiteDimensional_RRspace_aux (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : FiniteDimensional k ↥(RRspace k K D)

theorem FunctionField.Chart.finrank_RRspace_quotient_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : finrankRRspaceDiff k K D D' ≤ (deg k K (D' - D)).toNat

The local residue-field estimate for an increment of Riemann–Roch spaces.

theorem FunctionField.Chart.isAlgebraic_of_placeValuation_le_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (f : K) (hf : ∀ (v : PlaceA k K), (placeValuation k K v) f ≤ 1) : IsAlgebraic k f

A function integral at every coordinate place is algebraic over the constant field.

theorem FunctionField.Chart.ell_zero (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] : ell k K 0 = 1

instance FunctionField.Chart.finiteDimensional_RRspace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (D : DivisorA k K) : FiniteDimensional k ↥(RRspace k K D)

theorem FunctionField.Chart.finrankRRspaceDiff_add_ell (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : finrankRRspaceDiff k K D D' + ell k K D = ell k K D'

Rank-nullity for an inclusion of Riemann–Roch spaces.

theorem FunctionField.Chart.ell_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] (D : DivisorA k K) : ↑(ell k K D) ≤ deg k K (D ⊔ 0) + 1

theorem FunctionField.Chart.ell_le_nonneg (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [IsFullConstantField k K] {D : DivisorA k K} (hD : 0 ≤ D) : ↑(ell k K D) ≤ deg k K D + 1

theorem FunctionField.Chart.defect_mono (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] {D D' : DivisorA k K} (h : D ≤ D') : deg k K D - ↑(ell k K D) ≤ deg k K D' - ↑(ell k K D')