Generalities on the polynomial structure of rational functions

• Main evaluation properties
• Study of the X-adic valuation

Main definitions

• RatFunc.C is the constant polynomial
• RatFunc.X is the indeterminate
• RatFunc.eval evaluates a rational function given a value for the indeterminate
• idealX is the principal ideal generated by X in the ring of polynomials over a field K, regarded as an element of the height-one-spectrum.

Polynomial structure: C, X, eval

def RatFunc.C {K : Type u} [CommRing K] [IsDomain K] : K →+* RatFunc K

RatFunc.C a is the constant rational function a.

@[simp]

theorem RatFunc.algebraMap_eq_C {K : Type u} [CommRing K] [IsDomain K] : algebraMap K (RatFunc K) = C

@[simp]

theorem RatFunc.algebraMap_C {K : Type u} [CommRing K] [IsDomain K] (a : K) : (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = C a

@[simp]

theorem RatFunc.algebraMap_comp_C {K : Type u} [CommRing K] [IsDomain K] : (algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = C

theorem RatFunc.smul_eq_C_mul {K : Type u} [CommRing K] [IsDomain K] (r : K) (x : RatFunc K) : r • x = C r * x

theorem RatFunc.C_injective {K : Type u} [CommRing K] [IsDomain K] : Function.Injective ⇑C

def RatFunc.X {K : Type u} [CommRing K] [IsDomain K] : RatFunc K

RatFunc.X is the polynomial variable (aka indeterminate).

@[simp]

theorem RatFunc.algebraMap_X {K : Type u} [CommRing K] [IsDomain K] : (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = X

@[simp]

theorem RatFunc.algebraMap_monomial {K : Type u} [CommRing K] [IsDomain K] (n : ℕ) (a : K) : (algebraMap (Polynomial K) (RatFunc K)) ((Polynomial.monomial n) a) = C a * X ^ n

@[simp]

theorem RatFunc.aeval_X_left_eq_algebraMap {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) : (Polynomial.aeval X) p = (algebraMap (Polynomial K) (RatFunc K)) p

@[simp]

theorem RatFunc.liftRingHom_C {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : K) : (liftRingHom φ hφ) (C x) = φ (Polynomial.C x)

@[simp]

theorem RatFunc.liftRingHom_X {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) : (liftRingHom φ hφ) X = φ Polynomial.X

@[simp]

theorem RatFunc.num_C {K : Type u} [Field K] (c : K) : (C c).num = Polynomial.C c

@[simp]

theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) : (C c).denom = 1

@[simp]

theorem RatFunc.num_X {K : Type u} [Field K] : X.num = Polynomial.X

@[simp]

theorem RatFunc.denom_X {K : Type u} [Field K] : X.denom = 1

theorem RatFunc.X_ne_zero {K : Type u} [Field K] : X ≠ 0

theorem RatFunc.eq_C_iff {K : Type u} [Field K] (f : RatFunc K) : (∃ (c : K), f = C c) ↔ f.num.natDegree = 0 ∧ f.denom.natDegree = 0

def RatFunc.eval {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) (p : RatFunc K) : L

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

theorem RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : Polynomial.eval₂ f a x.denom = 0) : eval f a x = 0

theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [Field K] {L : Type u} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : eval f a x ≠ 0) : Polynomial.eval₂ f a x.denom ≠ 0

@[simp]

theorem RatFunc.eval_C {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {c : K} : eval f a (C c) = f c

@[simp]

theorem RatFunc.eval_X {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) : eval f a X = a

@[simp]

theorem RatFunc.eval_zero {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) : eval f a 0 = 0

@[simp]

theorem RatFunc.eval_one {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) : eval f a 1 = 1

@[simp]

theorem RatFunc.eval_algebraMap {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {S : Type u_1} [CommSemiring S] [Algebra S (Polynomial K)] (p : S) : eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)

theorem RatFunc.eval_add {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom ≠ 0) (hy : Polynomial.eval₂ f a y.denom ≠ 0) : eval f a (x + y) = eval f a x + eval f a y

eval is an additive homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0 ... ≠ 1 = eval _ 1 ((X-1) / (X-1)).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

theorem RatFunc.eval_mul {K : Type u} [Field K] {L : Type u} [Field L] (f : K →+* L) (a : L) {x y : RatFunc K} (hx : Polynomial.eval₂ f a x.denom ≠ 0) (hy : Polynomial.eval₂ f a y.denom ≠ 0) : eval f a (x * y) = eval f a x * eval f a y

eval is a multiplicative homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

theorem RatFunc.transcendental_X {K : Type u} [CommRing K] [IsDomain K] : Transcendental K X

instance RatFunc.transcendental {K : Type u} [CommRing K] [IsDomain K] : Algebra.Transcendental K (RatFunc K)

def Polynomial.idealX (K : Type u_1) [Field K] : IsDedekindDomain.HeightOneSpectrum (Polynomial K)

This is the principal ideal generated by X in the ring of polynomials over a field K, regarded as an element of the height-one-spectrum.

@[simp]

theorem Polynomial.idealX_span (K : Type u_1) [Field K] : (idealX K).asIdeal = Ideal.span {X}

@[simp]

theorem Polynomial.valuation_X_eq_neg_one (K : Type u_1) [Field K] : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (idealX K)) RatFunc.X = WithZero.exp (-1)

theorem Polynomial.valuation_of_mk (K : Type u_1) [Field K] (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (idealX K)) (RatFunc.mk f g) = (idealX K).intValuation f / (idealX K).intValuation g

theorem Polynomial.valuation_aeval_monomial_eq_valuation_pow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (L : Type u_3) [Field L] [Algebra K L] {v : Valuation L Γ} (hv : ∀ (a : K), a ≠ 0 → v ((algebraMap K L) a) = 1) (w : L) (n : ℕ) {a : K} (ha : a ≠ 0) : v ((aeval w) ((monomial n) a)) = v w ^ n

theorem Polynomial.valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] (L : Type u_3) [Field L] [Algebra K L] {v : Valuation L Γ} (hv : ∀ (a : K), a ≠ 0 → v ((algebraMap K L) a) = 1) (w : L) (hpos : 1 < v w) {p : Polynomial K} (hp : p ≠ 0) : v ((aeval w) p) = v w ^ p.natDegree

theorem Polynomial.valuation_monomial_eq_valuation_X_pow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} (hv : ∀ (a : K), a ≠ 0 → v ↑(C a) = 1) (n : ℕ) {a : K} (ha : a ≠ 0) : v ↑((monomial n) a) = v RatFunc.X ^ n

If a valuation v is trivial on constants then for every n : ℕ the valuation of (monomial n a) is equal to (v RatFunc.X) ^ n.

theorem Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} (hv : ∀ (a : K), a ≠ 0 → v ↑(C a) = 1) (hlt : 1 < v RatFunc.X) {p : Polynomial K} (hp : p ≠ 0) : v ↑p = v RatFunc.X ^ p.natDegree

If a valuation v is trivial on constants and 1 < v RatFunc.X then for every polynomial p, v p = v RatFunc.X ^ p.natDegree.

Note: The condition 1 < v RatFunc.X is typically satisfied by the valuation at infinity.

theorem Polynomial.valuation_le_one_of_valuation_X_le_one (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} (hv : ∀ (a : K), a ≠ 0 → v ↑(C a) = 1) (hle : v RatFunc.X ≤ 1) (p : Polynomial K) : v ↑p ≤ 1

If a valuation v is trivial on constants and v RatFunc.X ≤ 1 then for every polynomial p, v p ≤ 1.

theorem Polynomial.valuation_inv_monomial_eq_valuation_X_zpow (K : Type u_1) [Field K] {Γ : Type u_2} [LinearOrderedCommGroupWithZero Γ] {v : Valuation (RatFunc K) Γ} (hv : ∀ (a : K), a ≠ 0 → v ↑(C a) = 1) (n : ℕ) {a : K} (ha : a ≠ 0) : v (1 / ↑((monomial n) a)) = v RatFunc.X ^ (-↑n)

If a valuation v is trivial on constants then for every n : ℕ the valuation of 1 / (monomial n a) (as an element of the field of rational functions) is equal to (v RatFunc.X) ^ (- n).

instance RatFunc.instValuedWithZeroMultiplicativeInt (K : Type u_1) [Field K] : Valued (RatFunc K) (WithZero (Multiplicative ℤ))

@[simp]

theorem RatFunc.v_def (K : Type u_1) [Field K] {x : RatFunc K} : Valued.v x = (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) x