Pole divisors and Stichtenoth 1.4.11

This file develops the pole divisor (x)_∞ and the key degree identity: deg (polarDivisor x) = finrank k(X) K for transcendental x.

theorem FunctionField.Chart.linearIndependent_fin_pow_of_transcendental (k : Type u_1) (L : Type u_2) [Field k] [Field L] [Algebra k L] {x : L} (hx : Transcendental k x) (r : ℕ) : LinearIndependent k fun (j : Fin (r + 1)) => x ^ ↑j

Powers x^j with j ≤ r are k-linearly independent when x is transcendental.

@[instance_reducible]

noncomputable def FunctionField.Chart.instDecidableEqPlaceAPolar (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : DecidableEq (PlaceA k K)

Decidable equality on coordinate places for polar divisor proofs.

Equations

• FunctionField.Chart.instDecidableEqPlaceAPolar k K = Classical.decEq (FunctionField.Chart.PlaceA k K)

@[instance_reducible]

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

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

Equations

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

noncomputable def FunctionField.Chart.polarDivisor (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) : DivisorA k K

The pole divisor (x)_∞ of a nonzero function.

Equations

• FunctionField.Chart.polarDivisor k K x = if hx : x = 0 then 0 else -(FunctionField.Chart.principalDivisorA k K) (Additive.ofMul (Units.mk0 x hx)) ⊔ 0

theorem FunctionField.Chart.polarDivisor_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] : polarDivisor k K 0 = 0

theorem FunctionField.Chart.polarDivisor_nonneg (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) : 0 ≤ polarDivisor k K x

theorem FunctionField.Chart.polarDivisor_eq_zero_of_algebraic (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] {x : K} (hx : IsAlgebraic k x) : polarDivisor k K x = 0

theorem FunctionField.Chart.exists_placeValuation_gt_one_of_not_algebraic (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] {x : K} (_hx : x ≠ 0) (hnt : ¬IsAlgebraic k x) : ∃ (v : PlaceA k K), 1 < (placeValuation k K v) x

theorem FunctionField.Chart.polarDivisor_pos (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] {x : K} (hx : x ≠ 0) (hnt : ¬IsAlgebraic k x) : 0 < deg k K (polarDivisor k K x)

theorem FunctionField.Chart.not_isAlgebraic_iff_transcendental (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (x : K) : ¬IsAlgebraic k x ↔ Transcendental k x

¬IsAlgebraic is equivalent to Transcendental over a field.

theorem FunctionField.Chart.le_of_forall_nat_mul_le {n d c : ℕ} (_hd : 0 < d) (h : ∀ (r : ℕ), n * (r + 1) ≤ d * r + c) : n ≤ d

If n(r + 1) ≤ dr + c for all natural r and 0 < d, then n ≤ d. Used in the finrank ≤ deg B half of Stichtenoth 1.4.11.

theorem FunctionField.Chart.memRRspace_polarDivisor_of_ne_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} (hxne : x ≠ 0) : memRRspace k K (polarDivisor k K x) x

theorem FunctionField.Chart.memRRspace_smul_polar (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} (hxne : x ≠ 0) (n : ℕ) : memRRspace k K (n • polarDivisor k K x) (x ^ n)

theorem FunctionField.Chart.nsmul_le_nsmul_polar (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 : 0 ≤ D) {j r : ℕ} (hjr : j ≤ r) : j • D ≤ r • D

noncomputable def FunctionField.Chart.basisPoleBound (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] {ι : Type u_3} [Fintype ι] (f : ι → K) : DivisorA k K

A uniform pole bound for a finite family of functions.

Equations

• FunctionField.Chart.basisPoleBound k K f = ∑ i : ι, FunctionField.Chart.polarDivisor k K (f i)

theorem FunctionField.Chart.polarDivisor_le_basisPoleBound (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] {ι : Type u_3} [Fintype ι] (f : ι → K) (i : ι) : polarDivisor k K (f i) ≤ basisPoleBound k K f

theorem FunctionField.Chart.basisPoleBound_nonneg (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] {ι : Type u_3} [Fintype ι] (f : ι → K) : 0 ≤ basisPoleBound k K f

theorem FunctionField.Chart.memRRspace_basisPoleBound (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] {ι : Type u_3} [Fintype ι] (f : ι → K) (i : ι) : memRRspace k K (basisPoleBound k K f) (f i)

theorem FunctionField.Chart.memRRspace_basis_smul_x_pow (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] {ι : Type u_3} [Fintype ι] (f : ι → K) (x : K) (hxne : x ≠ 0) (r : ℕ) (i : ι) (j : ℕ) (hj : j ≤ r) : memRRspace k K (basisPoleBound k K f + r • polarDivisor k K x) (f i * x ^ j)

theorem FunctionField.Chart.instIsScalarTowerChart (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] : IsScalarTower k (RatFunc k) K

Scalar tower k → k⟮X⟯ → K for chart-variable arguments.

noncomputable def FunctionField.Chart.XK (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : K

The chart variable X_K in K.

Equations

• FunctionField.Chart.XK k K = (algebraMap (RatFunc k) K) RatFunc.X

theorem FunctionField.Chart.transcendental_XK (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] : Transcendental k (XK k K)

theorem FunctionField.Chart.not_algebraic_XK (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] : ¬IsAlgebraic k (XK k K)

theorem FunctionField.Chart.XK_ne_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] : XK k K ≠ 0

theorem FunctionField.Chart.linearIndependent_fin_pow_XK (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] (r : ℕ) : LinearIndependent k fun (j : Fin (r + 1)) => XK k K ^ ↑j

Powers X_K^j with j ≤ r are k-linearly independent.

theorem FunctionField.Chart.linearIndependent_basis_smul_XK_pow (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] {n r : ℕ} (b : Module.Basis (Fin n) (RatFunc k) K) : LinearIndependent k fun (p : Fin n × Fin (r + 1)) => b p.1 * XK k K ^ ↑p.2

The family {b i · X_K^j} is k-linearly independent over a k⟮X⟯-basis b.

theorem FunctionField.Chart.ell_family_ge (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] {n r : ℕ} (b : Module.Basis (Fin n) (RatFunc k) K) : n * (r + 1) ≤ ell k K (basisPoleBound k K ⇑b + r • polarDivisor k K (XK k K))

Growth along the pole family: n(r+1) ≤ ℓ(C + r•B).

theorem FunctionField.Chart.finrank_le_deg_polarX (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] : ↑(Module.finrank (RatFunc k) K) ≤ deg k K (polarDivisor k K (XK k K))

Stichtenoth 1.4.11 counting half for the chart variable: [K : k⟮X⟯] ≤ deg (X_K)_∞.

noncomputable def FunctionField.Chart.rationalSubfield (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] (x : K) : IntermediateField k K

The rational function field k(x) ⊆ K generated by a transcendental element.

Equations

• FunctionField.Chart.rationalSubfield k K x = k⟮x⟯

theorem FunctionField.Chart.linearIndependent_basis_smul_x_pow (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] {n r : ℕ} {x : K} (hx : Transcendental k x) (b : Module.Basis (Fin n) (↥(rationalSubfield k K x)) K) : LinearIndependent k fun (p : Fin n × Fin (r + 1)) => b p.1 * x ^ ↑p.2

The family {b i * x^j} is k-linearly independent over a k(x)-basis b.

theorem FunctionField.Chart.algebraMap_polynomial_eq_aeval_XK (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] (p : Polynomial k) : (algebraMap (Polynomial k) K) p = (Polynomial.aeval (XK k K)) p

The structure map k[X] → K is evaluation of polynomials at the chart variable X_K.

theorem FunctionField.Chart.algebraMap_ratFunc_eq_div (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] (c : RatFunc k) : (algebraMap (RatFunc k) K) c = (Polynomial.aeval (XK k K)) c.num / (Polynomial.aeval (XK k K)) c.denom

The structure map k⟮X⟯ → K sends a rational function to the quotient of the evaluations of its numerator and denominator at X_K.

theorem FunctionField.Chart.coe_aeval_adjoinSimple_gen_XK (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (RatFunc k) K] (p : Polynomial k) : ↑((Polynomial.aeval (IntermediateField.AdjoinSimple.gen k (XK k K))) p) = (Polynomial.aeval (XK k K)) p

Coercion of aeval at the adjoined generator of k(X_K).

theorem FunctionField.Chart.coe_ratFuncAlgEquiv_XK (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] (c : RatFunc k) : ↑((RatFunc.algEquivOfTranscendental (XK k K) ⋯) c) = (algebraMap (RatFunc k) K) c

The canonical k-embedding k⟮X⟯ ≃ₐ k(X_K) ⊆ K agrees with the structure map.

Target 2: finrank bridge

theorem FunctionField.Chart.finrank_eq_finrank_rationalSubfield_XK (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] : Module.finrank (RatFunc k) K = Module.finrank (↥(rationalSubfield k K ((algebraMap (RatFunc k) K) RatFunc.X))) K

Target 1: finite dimensionality over k(x)

theorem FunctionField.Chart.isAlgebraic_adjoin_XK (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] [Algebra.IsSeparable (RatFunc k) K] (z : K) : IsAlgebraic (↥k[XK k K]) z

Every element of K is algebraic over the polynomial subalgebra k[X_K].

theorem FunctionField.Chart.isAlgebraic_adjoin_x_XK (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] [Algebra.IsSeparable (RatFunc k) K] {x : K} (hx : Transcendental k x) : IsAlgebraic (↥k[x]) (XK k K)

Exchange: if x is transcendental over k, then X_K is algebraic over k[x].

theorem FunctionField.Chart.isAlgebraic_rationalSubfield_XK (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] [Algebra.IsSeparable (RatFunc k) K] {x : K} (hx : Transcendental k x) : IsAlgebraic (↥(rationalSubfield k K x)) (XK k K)

X_K is algebraic over the rational subfield k(x).

theorem FunctionField.Chart.finiteDimensional_rationalSubfield (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] {x : K} (hx : Transcendental k x) : FiniteDimensional (↥(rationalSubfield k K x)) K

A function field is finite over the rational subfield generated by a transcendental element.

theorem FunctionField.Chart.finrankAdjoin_le_deg_polar (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] {x : K} (hx : ¬IsAlgebraic k x) : ↑(Module.finrank (↥(rationalSubfield k K x)) K) ≤ deg k K (polarDivisor k K x)

Stichtenoth 1.4.11 (≤) for general transcendental x.

theorem FunctionField.Chart.deg_polar_le_finrank (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] {x : K} (hx : ¬IsAlgebraic k x) (hxgen : x = (algebraMap (RatFunc k) K) RatFunc.X) : ↑(Module.finrank (RatFunc k) K) ≤ deg k K (polarDivisor k K x)

Coordinate-base specialization via the adjoin bridge.