# 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} [] [] :

RatFunc.C a is the constant rational function a.

Equations
Instances For
@[simp]
theorem RatFunc.algebraMap_eq_C {K : Type u} [] [] :
algebraMap K () = RatFunc.C
@[simp]
theorem RatFunc.algebraMap_C {K : Type u} [] [] (a : K) :
(algebraMap () ()) (Polynomial.C a) = RatFunc.C a
@[simp]
theorem RatFunc.algebraMap_comp_C {K : Type u} [] [] :
(algebraMap () ()).comp Polynomial.C = RatFunc.C
theorem RatFunc.smul_eq_C_mul {K : Type u} [] [] (r : K) (x : ) :
r x = RatFunc.C r * x
def RatFunc.X {K : Type u} [] [] :

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

Equations
Instances For
@[simp]
theorem RatFunc.algebraMap_X {K : Type u} [] [] :
(algebraMap () ()) Polynomial.X = RatFunc.X
@[simp]
theorem RatFunc.num_C {K : Type u} [] (c : K) :
(RatFunc.C c).num = Polynomial.C c
@[simp]
theorem RatFunc.denom_C {K : Type u} [] (c : K) :
(RatFunc.C c).denom = 1
@[simp]
theorem RatFunc.num_X {K : Type u} [] :
RatFunc.X.num = Polynomial.X
@[simp]
theorem RatFunc.denom_X {K : Type u} [] :
RatFunc.X.denom = 1
theorem RatFunc.X_ne_zero {K : Type u} [] :
RatFunc.X 0
def RatFunc.eval {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) (p : ) :
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.

Equations
Instances For
theorem RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [] {L : Type u} [] {f : K →+* L} {a : L} {x : } (h : Polynomial.eval₂ f a x.denom = 0) :
RatFunc.eval f a x = 0
theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [] {L : Type u} [] {f : K →+* L} {a : L} {x : } (h : RatFunc.eval f a x 0) :
Polynomial.eval₂ f a x.denom 0
@[simp]
theorem RatFunc.eval_C {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) {c : K} :
RatFunc.eval f a (RatFunc.C c) = f c
@[simp]
theorem RatFunc.eval_X {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) :
RatFunc.eval f a RatFunc.X = a
@[simp]
theorem RatFunc.eval_zero {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) :
RatFunc.eval f a 0 = 0
@[simp]
theorem RatFunc.eval_one {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) :
RatFunc.eval f a 1 = 1
@[simp]
theorem RatFunc.eval_algebraMap {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) {S : Type u_1} [] [Algebra S ()] (p : S) :
RatFunc.eval f a ((algebraMap S ()) p) = Polynomial.eval₂ f a ((algebraMap S ()) p)
theorem RatFunc.eval_add {K : Type u} [] {L : Type u} [] (f : K →+* L) (a : L) {x : } {y : } (hx : Polynomial.eval₂ f a x.denom 0) (hy : Polynomial.eval₂ f a y.denom 0) :
RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.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} [] {L : Type u} [] (f : K →+* L) (a : L) {x : } {y : } (hx : Polynomial.eval₂ f a x.denom 0) (hy : Polynomial.eval₂ f a y.denom 0) :
RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.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.

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

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.

Equations
• = { asIdeal := Ideal.span {Polynomial.X}, isPrime := , ne_bot := }
Instances For
@[simp]
theorem Polynomial.idealX_span (K : Type u_1) [] :
.asIdeal = Ideal.span {Polynomial.X}
@[simp]
theorem Polynomial.valuation_X_eq_neg_one (K : Type u_1) [] :
.valuation RatFunc.X = (Multiplicative.ofAdd (-1))
Equations
@[simp]
theorem RatFunc.WithZero.valued_def (K : Type u_1) [] {x : } :
Valued.v x = .valuation x