mathlib documentation

field_theory.ratfunc

The field of rational functions #

This file defines the field ratfunc K of rational functions over a field K, and shows it is the field of fractions of polynomial K.

Main definitions #

Working with rational functions as polynomials:

Working with rational functions as fractions:

We also have a set of recursion and induction principles:

Implementation notes #

To provide good API encapsulation and speed up unification problems, ratfunc is defined as a structure, and all operations are @[irreducible] defs

We need a couple of maps to set up the field and is_fraction_ring structure, namely ratfunc.of_fraction_ring, ratfunc.to_fraction_ring, ratfunc.mk and ratfunc.to_fraction_ring_ring_equiv. All these maps get simped to bundled morphisms like algebra_map (polynomial K) (ratfunc K) and is_localization.alg_equiv.

References #

structure ratfunc (K : Type u) [hring : comm_ring K] :
Type u

ratfunc K is K(x), the field of rational functions over K.

The inclusion of polynomials into ratfunc is algebra_map (polynomial K) (ratfunc K), the maps between ratfunc K and another field of fractions of polynomial K, especially fraction_ring (polynomial K), are given by is_localization.algebra_equiv.

Constructing ratfuncs and their induction principles #

theorem ratfunc.of_fraction_ring_injective {K : Type u} [hring : comm_ring K] :
function.injective ratfunc.of_fraction_ring
@[protected]
noncomputable def ratfunc.lift_on {K : Type u} [hring : comm_ring K] {P : Sort v} (x : ratfunc K) (f : polynomial Kpolynomial K → P) (H : ∀ {p q p' q' : polynomial K}, q (polynomial K)q' (polynomial K)p * q' = p' * qf p q = f p' q') :
P

Non-dependent recursion principle for ratfunc K: To construct a term of P : Sort* out of x : ratfunc K, it suffices to provide a constructor f : Π (p q : polynomial K), P and a proof that f p q = f p' q' for all p q p' q' such that p * q' = p' * q where both q and q' are not zero divisors, stated as q ∉ (polynomial K)⁰, q' ∉ (polynomial K)⁰.

If considering K as an integral domain, this is the same as saying that we construct a value of P for such elements of ratfunc K by setting lift_on (p / q) f _ = f p q.

When [is_domain K], one can use ratfunc.lift_on', which has the stronger requirement of ∀ {p q a : polynomial K} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q).

Equations
theorem ratfunc.lift_on_of_fraction_ring_mk {K : Type u} [hring : comm_ring K] {P : Sort v} (n : polynomial K) (d : (polynomial K)) (f : polynomial Kpolynomial K → P) (H : ∀ {p q p' q' : polynomial K}, q (polynomial K)q' (polynomial K)p * q' = p' * qf p q = f p' q') :
@[protected]
noncomputable def ratfunc.mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : polynomial K) :

ratfunc.mk (p q : polynomial K) is p / q as a rational function.

If q = 0, then mk returns 0.

This is an auxiliary definition used to define an algebra structure on ratfunc; the simp normal form of mk p q is algebra_map _ _ p / algebra_map _ _ q.

Equations
theorem ratfunc.mk_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) :
theorem ratfunc.mk_coe_def {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) (q : (polynomial K)) :
theorem ratfunc.mk_def_of_mem {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q (polynomial K)) :
theorem ratfunc.mk_def_of_ne {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
theorem ratfunc.mk_eq_localization_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
theorem ratfunc.mk_one' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : polynomial K) :
theorem ratfunc.mk_eq_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p q p' q' : polynomial K} (hq : q 0) (hq' : q' 0) :
ratfunc.mk p q = ratfunc.mk p' q' p * q' = p' * q
theorem ratfunc.lift_on_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial Kpolynomial K → P) (f0 : ∀ (p : polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : polynomial K}, q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : polynomial K}, q (polynomial K)q' (polynomial K)p * q' = p' * qf p q = f p' q') := _) :
(ratfunc.mk p q).lift_on f H = f p q
theorem ratfunc.lift_on_condition_of_lift_on'_condition {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} {f : polynomial Kpolynomial K → P} (H : ∀ {p q a : polynomial K}, q 0a 0f (a * p) (a * q) = f p q) ⦃p q p' q' : polynomial K⦄ (hq : q 0) (hq' : q' 0) (h : p * q' = p' * q) :
f p q = f p' q'
@[protected]
noncomputable def ratfunc.lift_on' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (x : ratfunc K) (f : polynomial Kpolynomial K → P) (H : ∀ {p q a : polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
P

Non-dependent recursion principle for ratfunc K: if f p q : P for all p q, such that f (a * p) (a * q) = f p q, then we can find a value of P for all elements of ratfunc K by setting lift_on' (p / q) f _ = f p q.

The value of f p 0 for any p is never used and in principle this may be anything, although many usages of lift_on' assume f p 0 = f 0 1.

Equations
theorem ratfunc.lift_on'_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial Kpolynomial K → P) (f0 : ∀ (p : polynomial K), f p 0 = f 0 1) (H : ∀ {p q a : polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
(ratfunc.mk p q).lift_on' f H = f p q
@[protected]
theorem ratfunc.induction_on' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : polynomial K), q 0P (ratfunc.mk p q)) :
P x

Induction principle for ratfunc K: if f p q : P (ratfunc.mk p q) for all p q, then P holds on all elements of ratfunc K.

See also induction_on, which is a recursion principle defined in terms of algebra_map.

Defining the field structure #

@[protected]
noncomputable def ratfunc.zero {K : Type u} [hring : comm_ring K] :

The zero rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_zero {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_zero {K : Type u} [hring : comm_ring K] :
@[protected]
noncomputable def ratfunc.add {K : Type u} [hring : comm_ring K] :
ratfunc Kratfunc Kratfunc K

Addition of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_add {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_add {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.sub {K : Type u} [hring : comm_ring K] :
ratfunc Kratfunc Kratfunc K

Subtraction of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_sub {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_sub {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.neg {K : Type u} [hring : comm_ring K] :

Additive inverse of a rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_neg {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_neg {K : Type u} [hring : comm_ring K] (p : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.one {K : Type u} [hring : comm_ring K] :

The multiplicative unit of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_one {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_one {K : Type u} [hring : comm_ring K] :
@[protected]
noncomputable def ratfunc.mul {K : Type u} [hring : comm_ring K] :
ratfunc Kratfunc Kratfunc K

Multiplication of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_mul {K : Type u} [hring : comm_ring K] :
Equations
theorem ratfunc.of_fraction_ring_mul {K : Type u} [hring : comm_ring K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc Kratfunc Kratfunc K

Division of rational functions.

Equations
@[protected, instance]
noncomputable def ratfunc.has_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
Equations
theorem ratfunc.of_fraction_ring_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : fraction_ring (polynomial K)) :
@[protected]
noncomputable def ratfunc.inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

Multiplicative inverse of a rational function.

Equations
@[protected, instance]
noncomputable def ratfunc.has_inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
Equations
theorem ratfunc.of_fraction_ring_inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : fraction_ring (polynomial K)) :
theorem ratfunc.mul_inv_cancel {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p : ratfunc K} (hp : p 0) :
p * p⁻¹ = 1
@[protected]
def ratfunc.smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring (polynomial K))] :
R → ratfunc Kratfunc K

Scalar multiplication of rational functions.

Equations
@[protected, instance]
def ratfunc.has_scalar {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring (polynomial K))] :
Equations
theorem ratfunc.of_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring (polynomial K))] (c : R) (p : fraction_ring (polynomial K)) :
theorem ratfunc.to_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring (polynomial K))] (c : R) (p : ratfunc K) :
theorem ratfunc.mk_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [distrib_mul_action R (polynomial K)] [htower : is_scalar_tower R (polynomial K) (polynomial K)] (c : R) (p q : polynomial K) :
ratfunc.mk (c p) q = c ratfunc.mk p q
@[protected, instance]
def ratfunc.is_scalar_tower {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [distrib_mul_action R (polynomial K)] [htower : is_scalar_tower R (polynomial K) (polynomial K)] :
@[protected, instance]
noncomputable def ratfunc.inhabited (K : Type u) [hring : comm_ring K] :
Equations
@[protected, instance]
def ratfunc.nontrivial (K : Type u) [hring : comm_ring K] [is_domain K] :
noncomputable def ratfunc.to_fraction_ring_ring_equiv (K : Type u) [hring : comm_ring K] :

ratfunc K is isomorphic to the field of fractions of polynomial K, as rings.

This is an auxiliary definition; simp-normal form is is_localization.alg_equiv.

Equations

Solve equations for ratfunc K by working in fraction_ring (polynomial K).

Solve equations for ratfunc K by applying ratfunc.induction_on.

ratfunc as field of fractions of polynomial #

@[protected, instance]
noncomputable def ratfunc.algebra {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (R : Type u_1) [comm_semiring R] [algebra R (polynomial K)] :
Equations
theorem ratfunc.mk_one {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : polynomial K) :
@[simp]
theorem ratfunc.mk_eq_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : polynomial K) :
theorem ratfunc.of_fraction_ring_comp_algebra_map (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
ratfunc.of_fraction_ring (algebra_map (polynomial K) (fraction_ring (polynomial K))) = (algebra_map (polynomial K) (ratfunc K))
theorem ratfunc.algebra_map_injective (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.algebra_map_eq_zero_iff (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] {x : polynomial K} :
theorem ratfunc.algebra_map_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {x : polynomial K} (hx : x 0) :
@[protected, instance]
def ratfunc.is_fraction_ring (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :

ratfunc K is the field of fractions of the polynomials over K.

@[simp]
theorem ratfunc.lift_on_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial Kpolynomial K → P) (f0 : ∀ (p : polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : polynomial K}, q 0q' 0p * q' = p' * qf p q = f p' q') (H : (∀ {p q p' q' : polynomial K}, q (polynomial K)q' (polynomial K)p * q' = p' * qf p q = f p' q') := _) :
@[simp]
theorem ratfunc.lift_on'_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial Kpolynomial K → P) (f0 : ∀ (p : polynomial K), f p 0 = f 0 1) (H : ∀ {p q a : polynomial K}, q 0a 0f (a * p) (a * q) = f p q) :
@[protected]
theorem ratfunc.induction_on {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : polynomial K), q 0P ((algebra_map (polynomial K) (ratfunc K)) p / (algebra_map (polynomial K) (ratfunc K)) q)) :
P x

Induction principle for ratfunc K: if f p q : P (p / q) for all p q : polynomial K, then P holds on all elements of ratfunc K.

See also induction_on', which is a recursion principle defined in terms of ratfunc.mk.

@[simp]
theorem ratfunc.of_fraction_ring_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

Numerator and denominator #

noncomputable def ratfunc.num_denom {K : Type u} [hfield : field K] (x : ratfunc K) :

ratfunc.num_denom are numerator and denominator of a rational function over a field, normalized such that the denominator is monic.

Equations
@[simp]
theorem ratfunc.num_denom_div {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
noncomputable def ratfunc.num {K : Type u} [hfield : field K] (x : ratfunc K) :

ratfunc.num is the numerator of a rational function, normalized such that the denominator is monic.

Equations
@[simp]
theorem ratfunc.num_div {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
@[simp]
theorem ratfunc.num_zero {K : Type u} [hfield : field K] :
0.num = 0
@[simp]
theorem ratfunc.num_one {K : Type u} [hfield : field K] :
1.num = 1
@[simp]
theorem ratfunc.num_algebra_map {K : Type u} [hfield : field K] (p : polynomial K) :
@[simp]
theorem ratfunc.num_div_dvd {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
noncomputable def ratfunc.denom {K : Type u} [hfield : field K] (x : ratfunc K) :

ratfunc.denom is the denominator of a rational function, normalized such that it is monic.

Equations
@[simp]
theorem ratfunc.denom_div {K : Type u} [hfield : field K] (p : polynomial K) {q : polynomial K} (hq : q 0) :
theorem ratfunc.monic_denom {K : Type u} [hfield : field K] (x : ratfunc K) :
theorem ratfunc.denom_ne_zero {K : Type u} [hfield : field K] (x : ratfunc K) :
@[simp]
theorem ratfunc.denom_zero {K : Type u} [hfield : field K] :
0.denom = 1
@[simp]
theorem ratfunc.denom_one {K : Type u} [hfield : field K] :
1.denom = 1
@[simp]
theorem ratfunc.denom_algebra_map {K : Type u} [hfield : field K] (p : polynomial K) :
@[simp]
theorem ratfunc.denom_div_dvd {K : Type u} [hfield : field K] (p q : polynomial K) :
@[simp]
theorem ratfunc.num_div_denom {K : Type u} [hfield : field K] (x : ratfunc K) :
@[simp]
theorem ratfunc.num_eq_zero_iff {K : Type u} [hfield : field K] {x : ratfunc K} :
x.num = 0 x = 0
theorem ratfunc.num_ne_zero {K : Type u} [hfield : field K] {x : ratfunc K} (hx : x 0) :
x.num 0
theorem ratfunc.num_mul_eq_mul_denom_iff {K : Type u} [hfield : field K] {x : ratfunc K} {p q : polynomial K} (hq : q 0) :
theorem ratfunc.num_denom_add {K : Type u} [hfield : field K] (x y : ratfunc K) :
((x + y).num) * (x.denom) * y.denom = ((x.num) * y.denom + (x.denom) * y.num) * (x + y).denom
theorem ratfunc.num_denom_mul {K : Type u} [hfield : field K] (x y : ratfunc K) :
((x * y).num) * (x.denom) * y.denom = ((x.num) * y.num) * (x * y).denom
theorem ratfunc.num_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {p : polynomial K} (hp : p 0) :
x.num p ∃ (q : polynomial K) (hq : q 0), x = (algebra_map (polynomial K) (ratfunc K)) p / (algebra_map (polynomial K) (ratfunc K)) q
theorem ratfunc.denom_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {q : polynomial K} (hq : q 0) :
theorem ratfunc.num_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x * y).num (x.num) * y.num
theorem ratfunc.denom_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x * y).denom (x.denom) * y.denom
theorem ratfunc.denom_add_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :
(x + y).denom (x.denom) * y.denom

Polynomial structure: C, X, eval #

noncomputable def ratfunc.C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

ratfunc.C a is the constant rational function a.

Equations
@[simp]
theorem ratfunc.algebra_map_eq_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.algebra_map_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (a : K) :
@[simp]
theorem ratfunc.algebra_map_comp_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
noncomputable def ratfunc.X {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

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

Equations
@[simp]
theorem ratfunc.algebra_map_X {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :
@[simp]
theorem ratfunc.num_C {K : Type u} [hfield : field K] (c : K) :
@[simp]
theorem ratfunc.denom_C {K : Type u} [hfield : field K] (c : K) :
@[simp]
theorem ratfunc.num_X {K : Type u} [hfield : field K] :
@[simp]
theorem ratfunc.denom_X {K : Type u} [hfield : field K] :
noncomputable def ratfunc.eval {K : Type u} [hfield : field K] {L : Type u_1} [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
theorem ratfunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : polynomial.eval₂ f a x.denom = 0) :
ratfunc.eval f a x = 0
theorem ratfunc.eval₂_denom_ne_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] {f : K →+* L} {a : L} {x : ratfunc K} (h : ratfunc.eval f a x 0) :
@[simp]
theorem ratfunc.eval_C {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {c : K} :
@[simp]
theorem ratfunc.eval_X {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
@[simp]
theorem ratfunc.eval_zero {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
ratfunc.eval f a 0 = 0
@[simp]
theorem ratfunc.eval_one {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :
ratfunc.eval f a 1 = 1
@[simp]
theorem ratfunc.eval_algebra_map {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {S : Type u_2} [comm_semiring S] [algebra S (polynomial K)] (p : S) :
theorem ratfunc.eval_add {K : Type u} [hfield : field K] {L : Type u_1} [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) :
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} [hfield : field K] {L : Type u_1} [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) :
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.