Documentation

Mathlib.FieldTheory.RatFunc.AsPolynomial

Generalities on the polynomial structure of rational functions #

Main definitions #

Polynomial structure: C, X, eval #

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

RatFunc.C a is the constant rational function a.

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

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

    Equations
    Instances For
      @[simp]
      theorem RatFunc.num_C {K : Type u} [Field K] (c : K) :
      @[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] :
      @[simp]
      theorem RatFunc.denom_X {K : Type u} [Field K] :
      theorem RatFunc.X_ne_zero {K : Type u} [Field K] :
      X 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.

      Equations
      Instances For
        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) :
        @[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) :
        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.

        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
        Instances For
          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 0v ((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 0v ((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 0v (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 0v (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 0v (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 0v (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).