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:

ratfunc.field provides a field structure
ratfunc.C is the constant polynomial
ratfunc.X is the indeterminate
ratfunc.eval evaluates a rational function given a value for the indeterminate You can use is_fraction_ring API to treat ratfunc as the field of fractions of polynomials:

algebra_map K[X] (ratfunc K) maps polynomials to rational functions
is_fraction_ring.alg_equiv maps other fields of fractions of polynomial K to ratfunc K, in particular:
fraction_ring.alg_equiv K[X] (ratfunc K) maps the generic field of fraction construction to ratfunc K. Combine this with alg_equiv.restrict_scalars to change the fraction_ring K[X] ≃ₐ[polynomial K] ratfunc K to fraction_ring K[X] ≃ₐ[K] ratfunc K.

Working with rational functions as fractions:

ratfunc.num and ratfunc.denom give the numerator and denominator. These values are chosen to be coprime and such that ratfunc.denom is monic.

Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying ratfunc.coe_alg_hom.

Lifting homomorphisms of polynomials to other types, by mapping and dividing, as long as the homomorphism retains the non-zero-divisor property:

ratfunc.lift_monoid_with_zero_hom lifts a polynomial K →*₀ G₀ to a ratfunc K →*₀ G₀, where [comm_ring K] [comm_group_with_zero G₀]
ratfunc.lift_ring_hom lifts a polynomial K →+* L to a ratfunc K →+* L, where [comm_ring K] [field L]
ratfunc.lift_alg_hom lifts a polynomial K →ₐ[S] L to a ratfunc K →ₐ[S] L, where [comm_ring K] [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] This is satisfied by injective homs. We also have lifting homomorphisms of polynomials to other polynomials, with the same condition on retaining the non-zero-divisor property across the map:
ratfunc.map lifts polynomial K →* R[X] when [comm_ring K] [comm_ring R]
ratfunc.map_ring_hom lifts polynomial K →+* R[X] when [comm_ring K] [comm_ring R]
ratfunc.map_alg_hom lifts polynomial K →ₐ[S] R[X] when [comm_ring K] [is_domain K] [comm_ring R] [is_domain R]

We also have a set of recursion and induction principles:

ratfunc.lift_on: define a function by mapping a fraction of polynomials p/q to f p q, if f is well-defined in the sense that p/q = p'/q' → f p q = f p' q'.
ratfunc.lift_on': define a function by mapping a fraction of polynomials p/q to f p q, if f is well-defined in the sense that f (a * p) (a * q) = f p' q'.
ratfunc.induction_on: if P holds on p / q for all polynomials p q, then P holds on all rational functions

We define the degree of a rational function, with values in ℤ:

int_degree is the degree of a rational function, defined as the difference between the nat_degree of its numerator and the nat_degree of its denominator. In particular, int_degree 0 = 0.

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 K[X] (ratfunc K) and is_localization.alg_equiv.

There are separate lifts and maps of homomorphisms, to provide routes of lifting even when the codomain is not a field or even an integral domain.

References #

source

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

Type u

to_fraction_ring : fraction_ring K[X]

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

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

Constructing `ratfunc`s and their induction principles #

source

theorem ratfunc.of_fraction_ring_injective {K : Type u} [hring : comm_ring K] :

function.injective ratfunc.of_fraction_ring

source

theorem ratfunc.to_fraction_ring_injective {K : Type u} [hring : comm_ring K] :

function.injective ratfunc.to_fraction_ring

source

@[protected]

noncomputable def ratfunc.lift_on {K : Type u} [hring : comm_ring K] {P : Sort v} (x : ratfunc K) (f : K[X] → K[X] → P) (H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → p * q' = p' * q → f p q = f p' q') :

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 : K[X]), 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 ∉ K[X]⁰, q' ∉ K[X]⁰.

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 : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q).

Equations

x.lift_on f H = localization.lift_on x.to_fraction_ring (λ (p : K[X]) (q : ↥K[X]⁰), f p ↑q) _

source

theorem ratfunc.lift_on_of_fraction_ring_mk {K : Type u} [hring : comm_ring K] {P : Sort v} (n : K[X]) (d : ↥K[X]⁰) (f : K[X] → K[X] → P) (H : ∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → p * q' = p' * q → f p q = f p' q') :

{to_fraction_ring := localization.mk n d}.lift_on f H = f n ↑d

source

@[protected]

noncomputable def ratfunc.mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : K[X]) :

ratfunc K

ratfunc.mk (p q : K[X]) 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

ratfunc.mk p q = {to_fraction_ring := ⇑(algebra_map K[X] (fraction_ring K[X])) p / ⇑(algebra_map K[X] (fraction_ring K[X])) q}

source

theorem ratfunc.mk_eq_div' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : K[X]) :

ratfunc.mk p q = {to_fraction_ring := ⇑(algebra_map K[X] (fraction_ring K[X])) p / ⇑(algebra_map K[X] (fraction_ring K[X])) q}

source

theorem ratfunc.mk_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) :

ratfunc.mk p 0 = {to_fraction_ring := 0}

source

theorem ratfunc.mk_coe_def {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) (q : ↥K[X]⁰) :

ratfunc.mk p ↑q = {to_fraction_ring := is_localization.mk' (fraction_ring K[X]) p q}

source

theorem ratfunc.mk_def_of_mem {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q ∈ K[X]⁰) :

ratfunc.mk p q = {to_fraction_ring := is_localization.mk' (fraction_ring K[X]) p ⟨q, hq⟩}

source

theorem ratfunc.mk_def_of_ne {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

ratfunc.mk p q = {to_fraction_ring := is_localization.mk' (fraction_ring K[X]) p ⟨q, _⟩}

source

theorem ratfunc.mk_eq_localization_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

ratfunc.mk p q = {to_fraction_ring := localization.mk p ⟨q, _⟩}

source

theorem ratfunc.mk_one' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : K[X]) :

ratfunc.mk p 1 = {to_fraction_ring := ⇑(algebra_map K[X] (fraction_ring K[X])) p}

source

theorem ratfunc.mk_eq_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {p q p' q' : K[X]} (hq : q ≠ 0) (hq' : q' ≠ 0) :

ratfunc.mk p q = ratfunc.mk p' q' ↔ p * q' = p' * q

source

theorem ratfunc.lift_on_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → p * q' = p' * q → f p q = f p' q') (H : (∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → p * q' = p' * q → f p q = f p' q') := _) :

(ratfunc.mk p q).lift_on f H = f p q

source

theorem ratfunc.lift_on_condition_of_lift_on'_condition {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} {f : K[X] → K[X] → P} (H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) ⦃p q p' q' : K[X]⦄ (hq : q ≠ 0) (hq' : q' ≠ 0) (h : p * q' = p' * q) :

f p q = f p' q'

source

@[protected]

noncomputable def ratfunc.lift_on' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (x : ratfunc K) (f : K[X] → K[X] → P) (H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) :

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

x.lift_on' f H = x.lift_on f _

source

theorem ratfunc.lift_on'_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) :

(ratfunc.mk p q).lift_on' f H = f p q

source

@[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 : K[X]), q ≠ 0 → P (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 #

source

@[protected]

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

ratfunc K

The zero rational function.

Equations

ratfunc.zero = {to_fraction_ring := 0}

source

@[protected, instance]

noncomputable def ratfunc.has_zero {K : Type u} [hring : comm_ring K] :

has_zero (ratfunc K)

Equations

ratfunc.has_zero = {zero := ratfunc.zero hring}

source

theorem ratfunc.of_fraction_ring_zero {K : Type u} [hring : comm_ring K] :

{to_fraction_ring := 0} = 0

source

@[protected]

noncomputable def ratfunc.add {K : Type u} [hring : comm_ring K] :

ratfunc K → ratfunc K → ratfunc K

Addition of rational functions.

Equations

{to_fraction_ring := p}.add {to_fraction_ring := q} = {to_fraction_ring := p + q}

source

@[protected, instance]

noncomputable def ratfunc.has_add {K : Type u} [hring : comm_ring K] :

has_add (ratfunc K)

Equations

ratfunc.has_add = {add := ratfunc.add hring}

source

theorem ratfunc.of_fraction_ring_add {K : Type u} [hring : comm_ring K] (p q : fraction_ring K[X]) :

{to_fraction_ring := p + q} = {to_fraction_ring := p} + {to_fraction_ring := q}

source

@[protected]

noncomputable def ratfunc.sub {K : Type u} [hring : comm_ring K] :

ratfunc K → ratfunc K → ratfunc K

Subtraction of rational functions.

Equations

{to_fraction_ring := p}.sub {to_fraction_ring := q} = {to_fraction_ring := p - q}

source

@[protected, instance]

noncomputable def ratfunc.has_sub {K : Type u} [hring : comm_ring K] :

has_sub (ratfunc K)

Equations

ratfunc.has_sub = {sub := ratfunc.sub hring}

source

theorem ratfunc.of_fraction_ring_sub {K : Type u} [hring : comm_ring K] (p q : fraction_ring K[X]) :

{to_fraction_ring := p - q} = {to_fraction_ring := p} - {to_fraction_ring := q}

source

@[protected]

noncomputable def ratfunc.neg {K : Type u} [hring : comm_ring K] :

ratfunc K → ratfunc K

Additive inverse of a rational function.

Equations

{to_fraction_ring := p}.neg = {to_fraction_ring := -p}

source

@[protected, instance]

noncomputable def ratfunc.has_neg {K : Type u} [hring : comm_ring K] :

has_neg (ratfunc K)

Equations

ratfunc.has_neg = {neg := ratfunc.neg hring}

source

theorem ratfunc.of_fraction_ring_neg {K : Type u} [hring : comm_ring K] (p : fraction_ring K[X]) :

{to_fraction_ring := -p} = -{to_fraction_ring := p}

source

@[protected]

noncomputable def ratfunc.one {K : Type u} [hring : comm_ring K] :

ratfunc K

The multiplicative unit of rational functions.

Equations

ratfunc.one = {to_fraction_ring := 1}

source

@[protected, instance]

noncomputable def ratfunc.has_one {K : Type u} [hring : comm_ring K] :

has_one (ratfunc K)

Equations

ratfunc.has_one = {one := ratfunc.one hring}

source

theorem ratfunc.of_fraction_ring_one {K : Type u} [hring : comm_ring K] :

{to_fraction_ring := 1} = 1

source

@[protected]

noncomputable def ratfunc.mul {K : Type u} [hring : comm_ring K] :

ratfunc K → ratfunc K → ratfunc K

Multiplication of rational functions.

Equations

{to_fraction_ring := p}.mul {to_fraction_ring := q} = {to_fraction_ring := p * q}

source

@[protected, instance]

noncomputable def ratfunc.has_mul {K : Type u} [hring : comm_ring K] :

has_mul (ratfunc K)

Equations

ratfunc.has_mul = {mul := ratfunc.mul hring}

source

theorem ratfunc.of_fraction_ring_mul {K : Type u} [hring : comm_ring K] (p q : fraction_ring K[X]) :

{to_fraction_ring := p * q} = {to_fraction_ring := p} * {to_fraction_ring := q}

source

@[protected]

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

ratfunc K → ratfunc K → ratfunc K

Division of rational functions.

Equations

{to_fraction_ring := p}.div {to_fraction_ring := q} = {to_fraction_ring := p / q}

source

@[protected, instance]

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

has_div (ratfunc K)

Equations

ratfunc.has_div = {div := ratfunc.div hdomain}

source

theorem ratfunc.of_fraction_ring_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : fraction_ring K[X]) :

{to_fraction_ring := p / q} = {to_fraction_ring := p} / {to_fraction_ring := q}

source

@[protected]

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

ratfunc K → ratfunc K

Multiplicative inverse of a rational function.

Equations

{to_fraction_ring := p}.inv = {to_fraction_ring := p⁻¹}

source

@[protected, instance]

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

has_inv (ratfunc K)

Equations

ratfunc.has_inv = {inv := ratfunc.inv hdomain}

source

theorem ratfunc.of_fraction_ring_inv {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p : fraction_ring K[X]) :

{to_fraction_ring := p⁻¹} = {to_fraction_ring := p}⁻¹

source

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

source

@[protected]

def ratfunc.smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] :

R → ratfunc K → ratfunc K

Scalar multiplication of rational functions.

Equations

ratfunc.smul r {to_fraction_ring := p} = {to_fraction_ring := r • p}

source

@[protected, instance]

def ratfunc.has_scalar {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] :

has_scalar R (ratfunc K)

Equations

ratfunc.has_scalar = {smul := ratfunc.smul _inst_1}

source

theorem ratfunc.of_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] (c : R) (p : fraction_ring K[X]) :

{to_fraction_ring := c • p} = c • {to_fraction_ring := p}

source

theorem ratfunc.to_fraction_ring_smul {K : Type u} [hring : comm_ring K] {R : Type u_1} [has_scalar R (fraction_ring K[X])] (c : R) (p : ratfunc K) :

(c • p).to_fraction_ring = c • p.to_fraction_ring

source

theorem ratfunc.smul_eq_C_smul {K : Type u} [hring : comm_ring K] (x : ratfunc K) (r : K) :

r • x = ⇑polynomial.C r • x

source

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 K[X]] [htower : is_scalar_tower R K[X] K[X]] (c : R) (p q : K[X]) :

ratfunc.mk (c • p) q = c • ratfunc.mk p q

source

@[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 K[X]] [htower : is_scalar_tower R K[X] K[X]] :

is_scalar_tower R K[X] (ratfunc K)

source

@[protected, instance]

def ratfunc.subsingleton (K : Type u) [hring : comm_ring K] [subsingleton K] :

subsingleton (ratfunc K)

source

@[protected, instance]

noncomputable def ratfunc.inhabited (K : Type u) [hring : comm_ring K] :

inhabited (ratfunc K)

Equations

ratfunc.inhabited K = {default := 0}

source

@[protected, instance]

def ratfunc.nontrivial (K : Type u) [hring : comm_ring K] [nontrivial K] :

nontrivial (ratfunc K)

source

def ratfunc.to_fraction_ring_ring_equiv (K : Type u) [hring : comm_ring K] :

ratfunc K ≃+* fraction_ring K[X]

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

ratfunc.to_fraction_ring_ring_equiv K = {to_fun := ratfunc.to_fraction_ring hring, inv_fun := ratfunc.of_fraction_ring hring, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ratfunc.to_fraction_ring_ring_equiv_apply (K : Type u) [hring : comm_ring K] (self : ratfunc K) :

⇑(ratfunc.to_fraction_ring_ring_equiv K) self = self.to_fraction_ring

source

meta def ratfunc.frac_tac :

tactic unit

Solve equations for ratfunc K by working in fraction_ring K[X].

source

meta def ratfunc.smul_tac :

tactic unit

Solve equations for ratfunc K by applying ratfunc.induction_on.

source

@[protected, instance]

noncomputable def ratfunc.comm_ring (K : Type u) [hring : comm_ring K] :

comm_ring (ratfunc K)

Equations

ratfunc.comm_ring K = {add := has_add.add ratfunc.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := has_scalar.smul ratfunc.has_scalar, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ratfunc.has_neg, sub := has_sub.sub ratfunc.has_sub, sub_eq_add_neg := _, zsmul := has_scalar.smul ratfunc.has_scalar, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul ratfunc.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec ratfunc.has_mul, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

noncomputable def ratfunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ S[X]⁰) :

ratfunc R →* ratfunc S

Lift a monoid homomorphism that maps polynomials φ : R[X] →* S[X] to a ratfunc R →* ratfunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

ratfunc.map φ hφ = {to_fun := λ (f : ratfunc R), f.lift_on (λ (n d : R[X]), dite (⇑φ d ∈ S[X]⁰) (λ (h : ⇑φ d ∈ S[X]⁰), {to_fraction_ring := localization.mk (⇑φ n) ⟨⇑φ d, h⟩}) (λ (h : ⇑φ d ∉ S[X]⁰), 0)) _, map_one' := _, map_mul' := _}

source

theorem ratfunc.map_apply_of_fraction_ring_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ S[X]⁰) (n : R[X]) (d : ↥R[X]⁰) :

⇑(ratfunc.map φ hφ) {to_fraction_ring := localization.mk n d} = {to_fraction_ring := localization.mk (⇑φ n) ⟨⇑φ ↑d, _⟩}

source

theorem ratfunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [monoid_hom_class F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ S[X]⁰) (hf : function.injective ⇑φ) :

function.injective ⇑(ratfunc.map φ hφ)

source

noncomputable def ratfunc.map_ring_hom {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ring_hom_class F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ S[X]⁰) :

ratfunc R →+* ratfunc S

Lift a ring homomorphism that maps polynomials φ : R[X] →+* S[X] to a ratfunc R →+* ratfunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

ratfunc.map_ring_hom φ hφ = {to_fun := (ratfunc.map φ hφ).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem ratfunc.coe_map_ring_hom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [comm_ring R] [comm_ring S] [ring_hom_class F R[X] S[X]] (φ : F) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ S[X]⁰) :

⇑(ratfunc.map_ring_hom φ hφ) = ⇑(ratfunc.map φ hφ)

source

noncomputable def ratfunc.lift_monoid_with_zero_hom {G₀ : Type u_1} {R : Type u_3} [comm_group_with_zero G₀] [comm_ring R] (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ G₀⁰) :

ratfunc R →*₀ G₀

Lift an monoid with zero homomorphism polynomial R →*₀ G₀ to a ratfunc R →*₀ G₀ on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them. -

Equations

ratfunc.lift_monoid_with_zero_hom φ hφ = {to_fun := λ (f : ratfunc R), f.lift_on (λ (p q : R[X]), ⇑φ p / ⇑φ q) _, map_zero' := _, map_one' := _, map_mul' := _}

source

theorem ratfunc.lift_monoid_with_zero_hom_apply_of_fraction_ring_mk {G₀ : Type u_1} {R : Type u_3} [comm_group_with_zero G₀] [comm_ring R] (φ : R[X] →*₀ G₀) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ G₀⁰) (n : R[X]) (d : ↥R[X]⁰) :

⇑(ratfunc.lift_monoid_with_zero_hom φ hφ) {to_fraction_ring := localization.mk n d} = ⇑φ n / ⇑φ ↑d

source

theorem ratfunc.lift_monoid_with_zero_hom_injective {G₀ : Type u_1} {R : Type u_3} [comm_group_with_zero G₀] [comm_ring R] [nontrivial R] (φ : R[X] →*₀ G₀) (hφ : function.injective ⇑φ) (hφ' : R[X]⁰ ≤ submonoid.comap ↑φ G₀⁰ := _) :

function.injective ⇑(ratfunc.lift_monoid_with_zero_hom φ hφ')

source

noncomputable def ratfunc.lift_ring_hom {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ L⁰) :

ratfunc R →+* L

Lift an injective ring homomorphism polynomial R →+* L to a ratfunc R →+* L by mapping both the numerator and denominator and quotienting them. -

Equations

ratfunc.lift_ring_hom φ hφ = {to_fun := (ratfunc.lift_monoid_with_zero_hom φ.to_monoid_with_zero_hom hφ).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem ratfunc.lift_ring_hom_apply_of_fraction_ring_mk {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] (φ : R[X] →+* L) (hφ : R[X]⁰ ≤ submonoid.comap ↑φ L⁰) (n : R[X]) (d : ↥R[X]⁰) :

⇑(ratfunc.lift_ring_hom φ hφ) {to_fraction_ring := localization.mk n d} = ⇑φ n / ⇑φ ↑d

source

theorem ratfunc.lift_ring_hom_injective {L : Type u_2} {R : Type u_3} [field L] [comm_ring R] [nontrivial R] (φ : R[X] →+* L) (hφ : function.injective ⇑φ) (hφ' : R[X]⁰ ≤ submonoid.comap ↑φ L⁰ := _) :

function.injective ⇑(ratfunc.lift_ring_hom φ hφ')

source

@[protected, instance]

noncomputable def ratfunc.field (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :

field (ratfunc K)

Equations

ratfunc.field K = {add := comm_ring.add (ratfunc.comm_ring K), add_assoc := _, zero := comm_ring.zero (ratfunc.comm_ring K), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (ratfunc.comm_ring K), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (ratfunc.comm_ring K), sub := comm_ring.sub (ratfunc.comm_ring K), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (ratfunc.comm_ring K), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (ratfunc.comm_ring K), mul_assoc := _, one := comm_ring.one (ratfunc.comm_ring K), one_mul := _, mul_one := _, npow := comm_ring.npow (ratfunc.comm_ring K), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv ratfunc.has_inv, div := has_div.div ratfunc.has_div, div_eq_mul_inv := _, zpow := zpow_rec ratfunc.has_inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

`ratfunc` as field of fractions of `polynomial` #

source

@[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 K[X]] :

algebra R (ratfunc K)

Equations

ratfunc.algebra R = {to_has_scalar := {smul := has_scalar.smul ratfunc.has_scalar}, to_ring_hom := {to_fun := λ (x : R), ratfunc.mk (⇑(algebra_map R K[X]) x) 1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

theorem ratfunc.mk_one {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : K[X]) :

ratfunc.mk x 1 = ⇑(algebra_map K[X] (ratfunc K)) x

source

theorem ratfunc.of_fraction_ring_algebra_map {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : K[X]) :

{to_fraction_ring := ⇑(algebra_map K[X] (fraction_ring K[X])) x} = ⇑(algebra_map K[X] (ratfunc K)) x

source

@[simp]

theorem ratfunc.mk_eq_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (p q : K[X]) :

ratfunc.mk p q = ⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q

source

@[simp]

theorem ratfunc.div_smul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [monoid R] [distrib_mul_action R K[X]] [is_scalar_tower R K[X] K[X]] (c : R) (p q : K[X]) :

⇑(algebra_map K[X] (ratfunc K)) (c • p) / ⇑(algebra_map K[X] (ratfunc K)) q = c • (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q)

source

theorem ratfunc.algebra_map_apply {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} [comm_semiring R] [algebra R K[X]] (x : R) :

⇑(algebra_map R (ratfunc K)) x = ⇑(algebra_map K[X] (ratfunc K)) (⇑(algebra_map R K[X]) x) / ⇑(algebra_map K[X] (ratfunc K)) 1

source

theorem ratfunc.map_apply_div_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [monoid_hom_class F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ R[X]⁰) (p q : K[X]) (hq : q ≠ 0) :

⇑(ratfunc.map φ hφ) (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q) = ⇑(algebra_map R[X] (ratfunc R)) (⇑φ p) / ⇑(algebra_map R[X] (ratfunc R)) (⇑φ q)

source

@[simp]

theorem ratfunc.map_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [monoid_with_zero_hom_class F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ R[X]⁰) (p q : K[X]) :

⇑(ratfunc.map φ hφ) (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q) = ⇑(algebra_map R[X] (ratfunc R)) (⇑φ p) / ⇑(algebra_map R[X] (ratfunc R)) (⇑φ q)

source

@[simp]

theorem ratfunc.lift_monoid_with_zero_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} [comm_group_with_zero L] (φ : K[X] →*₀ L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (p q : K[X]) :

⇑(ratfunc.lift_monoid_with_zero_hom φ hφ) (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q) = ⇑φ p / ⇑φ q

source

@[simp]

theorem ratfunc.lift_ring_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} [field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (p q : K[X]) :

⇑(ratfunc.lift_ring_hom φ hφ) (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q) = ⇑φ p / ⇑φ q

source

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 K[X] (fraction_ring K[X])) = ⇑(algebra_map K[X] (ratfunc K))

source

theorem ratfunc.algebra_map_injective (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :

function.injective ⇑(algebra_map K[X] (ratfunc K))

source

@[simp]

theorem ratfunc.algebra_map_eq_zero_iff (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] {x : K[X]} :

⇑(algebra_map K[X] (ratfunc K)) x = 0 ↔ x = 0

source

theorem ratfunc.algebra_map_ne_zero {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {x : K[X]} (hx : x ≠ 0) :

⇑(algebra_map K[X] (ratfunc K)) x ≠ 0

source

noncomputable def ratfunc.map_alg_hom {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_2} {S : Type u_3} [comm_ring R] [is_domain R] [comm_semiring S] [algebra S K[X]] [algebra S R[X]] (φ : K[X] →ₐ[S] R[X]) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ R[X]⁰) :

ratfunc K →ₐ[S] ratfunc R

Lift an algebra homomorphism that maps polynomials φ : polynomial K →ₐ[S] R[X] to a ratfunc K →ₐ[S] ratfunc R, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

ratfunc.map_alg_hom φ hφ = {to_fun := (ratfunc.map_ring_hom φ hφ).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

theorem ratfunc.coe_map_alg_hom_eq_coe_map {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {R : Type u_2} {S : Type u_3} [comm_ring R] [is_domain R] [comm_semiring S] [algebra S K[X]] [algebra S R[X]] (φ : K[X] →ₐ[S] R[X]) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ R[X]⁰) :

⇑(ratfunc.map_alg_hom φ hφ) = ⇑(ratfunc.map φ hφ)

source

noncomputable def ratfunc.lift_alg_hom {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) :

ratfunc K →ₐ[S] L

Lift an injective algebra homomorphism polynomial K →ₐ[S] L to a ratfunc K →ₐ[S] L by mapping both the numerator and denominator and quotienting them. -

Equations

ratfunc.lift_alg_hom φ hφ = {to_fun := (ratfunc.lift_ring_hom φ.to_ring_hom hφ).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

theorem ratfunc.lift_alg_hom_apply_of_fraction_ring_mk {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (n : K[X]) (d : ↥K[X]⁰) :

⇑(ratfunc.lift_alg_hom φ hφ) {to_fraction_ring := localization.mk n d} = ⇑φ n / ⇑φ ↑d

source

theorem ratfunc.lift_alg_hom_injective {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : function.injective ⇑φ) (hφ' : K[X]⁰ ≤ submonoid.comap ↑φ L⁰ := _) :

function.injective ⇑(ratfunc.lift_alg_hom φ hφ')

source

@[simp]

theorem ratfunc.lift_alg_hom_apply_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {L : Type u_1} {S : Type u_3} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (p q : K[X]) :

⇑(ratfunc.lift_alg_hom φ hφ) (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q) = ⇑φ p / ⇑φ q

source

@[protected, instance]

def ratfunc.is_fraction_ring (K : Type u) [hring : comm_ring K] [hdomain : is_domain K] :

is_fraction_ring K[X] (ratfunc K)

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

source

@[simp]

theorem ratfunc.lift_on_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H' : ∀ {p q p' q' : K[X]}, q ≠ 0 → q' ≠ 0 → p * q' = p' * q → f p q = f p' q') (H : (∀ {p q p' q' : K[X]}, q ∈ K[X]⁰ → q' ∈ K[X]⁰ → p * q' = p' * q → f p q = f p' q') := _) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).lift_on f H = f p q

source

@[simp]

theorem ratfunc.lift_on'_div {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ (p : K[X]), f p 0 = f 0 1) (H : ∀ {p q a : K[X]}, q ≠ 0 → a ≠ 0 → f (a * p) (a * q) = f p q) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).lift_on' f H = f p q

source

@[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 : K[X]), q ≠ 0 → P (⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (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.

source

theorem ratfunc.of_fraction_ring_mk' {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (x : K[X]) (y : ↥K[X]⁰) :

{to_fraction_ring := is_localization.mk' (fraction_ring K[X]) x y} = is_localization.mk' (ratfunc K) x y

source

@[simp]

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

ratfunc.of_fraction_ring = ⇑(is_localization.alg_equiv K[X]⁰ (fraction_ring K[X]) (ratfunc K))

source

@[simp]

theorem ratfunc.to_fraction_ring_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

ratfunc.to_fraction_ring = ⇑(is_localization.alg_equiv K[X]⁰ (ratfunc K) (fraction_ring K[X]))

source

@[simp]

theorem ratfunc.to_fraction_ring_ring_equiv_symm_eq {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

(ratfunc.to_fraction_ring_ring_equiv K).symm = (is_localization.alg_equiv K[X]⁰ (fraction_ring K[X]) (ratfunc K)).to_ring_equiv

Numerator and denominator #

source

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

K[X] × K[X]

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

Equations

x.num_denom = x.lift_on' (λ (p q : K[X]), ite (q = 0) (0, 1) (let r : K[X] := gcd p q in ((⇑polynomial.C ((q / r).leading_coeff)⁻¹) * (p / r), (⇑polynomial.C ((q / r).leading_coeff)⁻¹) * (q / r)))) ratfunc.num_denom._proof_2

source

@[simp]

theorem ratfunc.num_denom_div {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).num_denom = ((⇑polynomial.C ((q / gcd p q).leading_coeff)⁻¹) * (p / gcd p q), (⇑polynomial.C ((q / gcd p q).leading_coeff)⁻¹) * (q / gcd p q))

source

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

K[X]

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

Equations

x.num = x.num_denom.fst

source

@[simp]

theorem ratfunc.num_zero {K : Type u} [hfield : field K] :

0.num = 0

source

@[simp]

theorem ratfunc.num_div {K : Type u} [hfield : field K] (p q : K[X]) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).num = (⇑polynomial.C ((q / gcd p q).leading_coeff)⁻¹) * (p / gcd p q)

source

@[simp]

theorem ratfunc.num_one {K : Type u} [hfield : field K] :

1.num = 1

source

@[simp]

theorem ratfunc.num_algebra_map {K : Type u} [hfield : field K] (p : K[X]) :

(⇑(algebra_map K[X] (ratfunc K)) p).num = p

source

theorem ratfunc.num_div_dvd {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).num ∣ p

source

@[simp]

theorem ratfunc.num_div_dvd' {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

(⇑polynomial.C ((q / gcd p q).leading_coeff)⁻¹) * (p / gcd p q) ∣ p

A version of num_div_dvd with the LHS in simp normal form

source

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

K[X]

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

Equations

x.denom = x.num_denom.snd

source

@[simp]

theorem ratfunc.denom_div {K : Type u} [hfield : field K] (p : K[X]) {q : K[X]} (hq : q ≠ 0) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).denom = (⇑polynomial.C ((q / gcd p q).leading_coeff)⁻¹) * (q / gcd p q)

source

theorem ratfunc.monic_denom {K : Type u} [hfield : field K] (x : ratfunc K) :

x.denom.monic

source

theorem ratfunc.denom_ne_zero {K : Type u} [hfield : field K] (x : ratfunc K) :

x.denom ≠ 0

source

@[simp]

theorem ratfunc.denom_zero {K : Type u} [hfield : field K] :

0.denom = 1

source

@[simp]

theorem ratfunc.denom_one {K : Type u} [hfield : field K] :

1.denom = 1

source

@[simp]

theorem ratfunc.denom_algebra_map {K : Type u} [hfield : field K] (p : K[X]) :

(⇑(algebra_map K[X] (ratfunc K)) p).denom = 1

source

@[simp]

theorem ratfunc.denom_div_dvd {K : Type u} [hfield : field K] (p q : K[X]) :

(⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q).denom ∣ q

source

@[simp]

theorem ratfunc.num_div_denom {K : Type u} [hfield : field K] (x : ratfunc K) :

⇑(algebra_map K[X] (ratfunc K)) x.num / ⇑(algebra_map K[X] (ratfunc K)) x.denom = x

source

@[simp]

theorem ratfunc.num_eq_zero_iff {K : Type u} [hfield : field K] {x : ratfunc K} :

x.num = 0 ↔ x = 0

source

theorem ratfunc.num_ne_zero {K : Type u} [hfield : field K] {x : ratfunc K} (hx : x ≠ 0) :

x.num ≠ 0

source

theorem ratfunc.num_mul_eq_mul_denom_iff {K : Type u} [hfield : field K] {x : ratfunc K} {p q : K[X]} (hq : q ≠ 0) :

(x.num) * q = p * x.denom ↔ x = ⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q

source

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

source

theorem ratfunc.num_denom_neg {K : Type u} [hfield : field K] (x : ratfunc K) :

((-x).num) * x.denom = (-x.num) * (-x).denom

source

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

source

theorem ratfunc.num_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {p : K[X]} (hp : p ≠ 0) :

x.num ∣ p ↔ ∃ (q : K[X]) (hq : q ≠ 0), x = ⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q

source

theorem ratfunc.denom_dvd {K : Type u} [hfield : field K] {x : ratfunc K} {q : K[X]} (hq : q ≠ 0) :

x.denom ∣ q ↔ ∃ (p : K[X]), x = ⇑(algebra_map K[X] (ratfunc K)) p / ⇑(algebra_map K[X] (ratfunc K)) q

source

theorem ratfunc.num_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :

(x * y).num ∣ (x.num) * y.num

source

theorem ratfunc.denom_mul_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :

(x * y).denom ∣ (x.denom) * y.denom

source

theorem ratfunc.denom_add_dvd {K : Type u} [hfield : field K] (x y : ratfunc K) :

(x + y).denom ∣ (x.denom) * y.denom

source

theorem ratfunc.map_denom_ne_zero {K : Type u} [hfield : field K] {L : Type u_1} {F : Type u_2} [has_zero L] [zero_hom_class F K[X] L] (φ : F) (hφ : function.injective ⇑φ) (f : ratfunc K) :

⇑φ f.denom ≠ 0

source

theorem ratfunc.map_apply {K : Type u} [hfield : field K] {R : Type u_1} {F : Type u_2} [comm_ring R] [is_domain R] [monoid_hom_class F K[X] R[X]] (φ : F) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ R[X]⁰) (f : ratfunc K) :

⇑(ratfunc.map φ hφ) f = ⇑(algebra_map R[X] (ratfunc R)) (⇑φ f.num) / ⇑(algebra_map R[X] (ratfunc R)) (⇑φ f.denom)

source

theorem ratfunc.lift_monoid_with_zero_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} [comm_group_with_zero L] (φ : K[X] →*₀ L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (f : ratfunc K) :

⇑(ratfunc.lift_monoid_with_zero_hom φ hφ) f = ⇑φ f.num / ⇑φ f.denom

source

theorem ratfunc.lift_ring_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} [field L] (φ : K[X] →+* L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (f : ratfunc K) :

⇑(ratfunc.lift_ring_hom φ hφ) f = ⇑φ f.num / ⇑φ f.denom

source

theorem ratfunc.lift_alg_hom_apply {K : Type u} [hfield : field K] {L : Type u_1} {S : Type u_2} [field L] [comm_semiring S] [algebra S K[X]] [algebra S L] (φ : K[X] →ₐ[S] L) (hφ : K[X]⁰ ≤ submonoid.comap ↑φ L⁰) (f : ratfunc K) :

⇑(ratfunc.lift_alg_hom φ hφ) f = ⇑φ f.num / ⇑φ f.denom

source

theorem ratfunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [hfield : field K] {x y : ratfunc K} (hxy : x + y ≠ 0) :

(x.num) * y.denom + (x.denom) * y.num ≠ 0

Polynomial structure: `C`, `X`, `eval` #

source

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

K →+* ratfunc K

ratfunc.C a is the constant rational function a.

Equations

ratfunc.C = algebra_map K (ratfunc K)

source

@[simp]

theorem ratfunc.algebra_map_eq_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

algebra_map K (ratfunc K) = ratfunc.C

source

@[simp]

theorem ratfunc.algebra_map_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (a : K) :

⇑(algebra_map K[X] (ratfunc K)) (⇑polynomial.C a) = ⇑ratfunc.C a

source

@[simp]

theorem ratfunc.algebra_map_comp_C {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

(algebra_map K[X] (ratfunc K)).comp polynomial.C = ratfunc.C

source

theorem ratfunc.smul_eq_C_mul {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] (r : K) (x : ratfunc K) :

r • x = (⇑ratfunc.C r) * x

source

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

ratfunc K

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

Equations

ratfunc.X = ⇑(algebra_map K[X] (ratfunc K)) polynomial.X

source

@[simp]

theorem ratfunc.algebra_map_X {K : Type u} [hring : comm_ring K] [hdomain : is_domain K] :

⇑(algebra_map K[X] (ratfunc K)) polynomial.X = ratfunc.X

source

@[simp]

theorem ratfunc.num_C {K : Type u} [hfield : field K] (c : K) :

(⇑ratfunc.C c).num = ⇑polynomial.C c

source

@[simp]

theorem ratfunc.denom_C {K : Type u} [hfield : field K] (c : K) :

(⇑ratfunc.C c).denom = 1

source

@[simp]

theorem ratfunc.num_X {K : Type u} [hfield : field K] :

ratfunc.X.num = polynomial.X

source

@[simp]

theorem ratfunc.denom_X {K : Type u} [hfield : field K] :

ratfunc.X.denom = 1

source

theorem ratfunc.X_ne_zero {K : Type u} [hfield : field K] :

ratfunc.X ≠ 0

source

noncomputable def ratfunc.eval {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) (p : ratfunc K) :

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

ratfunc.eval f a p = polynomial.eval₂ f a p.num / polynomial.eval₂ f a p.denom

source

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

source

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) :

polynomial.eval₂ f a x.denom ≠ 0

source

@[simp]

theorem ratfunc.eval_C {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) {c : K} :

ratfunc.eval f a (⇑ratfunc.C c) = ⇑f c

source

@[simp]

theorem ratfunc.eval_X {K : Type u} [hfield : field K] {L : Type u_1} [field L] (f : K →+* L) (a : L) :

ratfunc.eval f a ratfunc.X = a

source

@[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

source

@[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

source

@[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 K[X]] (p : S) :

ratfunc.eval f a (⇑(algebra_map S (ratfunc K)) p) = polynomial.eval₂ f a (⇑(algebra_map S K[X]) p)

source

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.

source

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.

source

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

ℤ

int_degree x is the degree of the rational function x, defined as the difference between the nat_degree of its numerator and the nat_degree of its denominator. In particular, int_degree 0 = 0.

Equations