mathlib3 documentation

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

Type u

to_fraction_ring : fraction_ring (polynomial K)

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 K[X], especially fraction_ring K[X], are given by is_localization.algebra_equiv.

Instances for ratfunc

Constructing `ratfunc`s and their induction principles #

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

function.injective ratfunc.of_fraction_ring

function.injective ratfunc.to_fraction_ring

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

@[protected, irreducible]

noncomputable def ratfunc.lift_on {K : Type u} [comm_ring K] {P : Sort v} (x : ratfunc K) (f : polynomial K → polynomial K → P) (H : ∀ {p q p' q' : polynomial K}, q ∈ non_zero_divisors (polynomial K) → q' ∈ non_zero_divisors (polynomial K) → q' * p = q * p' → 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 q' * p = q * p' 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 : polynomial K) (q : ↥(non_zero_divisors (polynomial K))), f p ↑q) _

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

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

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

f p q = f p' q'

@[protected, irreducible]

noncomputable def ratfunc.mk {K : Type u} [comm_ring K] [is_domain K] (p q : polynomial 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 (polynomial K) (fraction_ring (polynomial K))) p / ⇑(algebra_map (polynomial K) (fraction_ring (polynomial K))) q}

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

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

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

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

theorem ratfunc.mk_coe_def {K : Type u} [comm_ring K] [is_domain K] (p : polynomial K) (q : ↥(non_zero_divisors (polynomial K))) :

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

theorem ratfunc.mk_def_of_mem {K : Type u} [comm_ring K] [is_domain K] (p : polynomial K) {q : polynomial K} (hq : q ∈ non_zero_divisors (polynomial K)) :

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

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

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

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

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

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

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

theorem ratfunc.mk_eq_mk {K : Type u} [comm_ring K] [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} [comm_ring K] [is_domain K] {P : Sort v} (p q : polynomial K) (f : polynomial K → polynomial K → P) (f0 : ∀ (p : polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : polynomial K}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q') (H : (∀ {p q p' q' : polynomial K}, q ∈ non_zero_divisors (polynomial K) → q' ∈ non_zero_divisors (polynomial K) → q' * p = q * p' → f p q = f p' q') := _) :

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

@[protected, irreducible]

noncomputable def ratfunc.lift_on' {K : Type u} [comm_ring K] [is_domain K] {P : Sort v} (x : ratfunc K) (f : polynomial K → polynomial K → P) (H : ∀ {p q a : polynomial K}, 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 _

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

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

@[protected, irreducible]

theorem ratfunc.induction_on' {K : Type u} [comm_ring K] [is_domain K] {P : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : polynomial K), 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 #

@[protected, irreducible]

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

The zero rational function.

Equations

ratfunc.zero = {to_fraction_ring := 0}

@[protected, instance]

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

has_zero (ratfunc K)

Equations

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

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

{to_fraction_ring := 0} = 0

@[protected, irreducible]

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

Addition of rational functions.

Equations

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

@[protected, instance]

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

has_add (ratfunc K)

Equations

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

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

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

@[protected, irreducible]

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

Subtraction of rational functions.

Equations

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

@[protected, instance]

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

has_sub (ratfunc K)

Equations

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

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

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

@[protected, irreducible]

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

ratfunc K → ratfunc K

Additive inverse of a rational function.

Equations

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

@[protected, instance]

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

has_neg (ratfunc K)

Equations

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

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

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

@[protected, irreducible]

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

The multiplicative unit of rational functions.

Equations

ratfunc.one = {to_fraction_ring := 1}

@[protected, instance]

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

has_one (ratfunc K)

Equations

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

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

{to_fraction_ring := 1} = 1

@[protected, irreducible]

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

Multiplication of rational functions.

Equations

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

@[protected, instance]

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

has_mul (ratfunc K)

Equations

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

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

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

@[protected, irreducible]

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

Division of rational functions.

Equations

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

@[protected, instance]

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

has_div (ratfunc K)

Equations

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

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

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

@[protected, irreducible]

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

ratfunc K → ratfunc K

Multiplicative inverse of a rational function.

Equations

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

@[protected, instance]

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

has_inv (ratfunc K)

Equations

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

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

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

theorem ratfunc.mul_inv_cancel {K : Type u} [comm_ring K] [is_domain K] {p : ratfunc K} (hp : p ≠ 0) :

p * p⁻¹ = 1

@[protected, irreducible]

def ratfunc.smul {K : Type u} [comm_ring K] {R : Type u_1} [has_smul R (fraction_ring (polynomial K))] :

R → ratfunc K → ratfunc K

Scalar multiplication of rational functions.

Equations

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

@[protected, nolint, instance]

def ratfunc.has_smul {K : Type u} [comm_ring K] {R : Type u_1} [has_smul R (fraction_ring (polynomial K))] :

has_smul R (ratfunc K)

Equations

ratfunc.has_smul = {smul := ratfunc.smul _inst_2}

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

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

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

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

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

r • x = ⇑polynomial.C r • x

theorem ratfunc.mk_smul {K : Type u} [comm_ring K] {R : Type u_1} [is_domain K] [monoid R] [distrib_mul_action R (polynomial K)] [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} [comm_ring K] {R : Type u_1} [is_domain K] [monoid R] [distrib_mul_action R (polynomial K)] [is_scalar_tower R (polynomial K) (polynomial K)] :

is_scalar_tower R (polynomial K) (ratfunc K)

@[protected, instance]

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

subsingleton (ratfunc K)

@[protected, instance]

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

inhabited (ratfunc K)

Equations

ratfunc.inhabited K = {default := 0}

@[protected, instance]

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

nontrivial (ratfunc K)

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

ratfunc K ≃+* fraction_ring (polynomial K)

ratfunc K is isomorphic to the field of fractions of K[X], 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 _inst_1, inv_fun := ratfunc.of_fraction_ring _inst_1, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[simp]

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

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

meta def ratfunc.frac_tac :

tactic unit

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

meta def ratfunc.smul_tac :

tactic unit

Solve equations for ratfunc K by applying ratfunc.induction_on.

@[protected, instance]

noncomputable def ratfunc.comm_ring (K : Type u) [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_smul.smul ratfunc.has_smul, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg ratfunc.has_neg, sub := has_sub.sub ratfunc.has_sub, sub_eq_add_neg := _, zsmul := has_smul.smul ratfunc.has_smul, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast._default (ring.nat_cast._default 1 has_add.add _ 0 _ _ has_smul.smul _ _) has_add.add _ 0 _ _ has_smul.smul _ _ 1 _ _ has_neg.neg has_sub.sub _ has_smul.smul _ _ _ _, nat_cast := ring.nat_cast._default 1 has_add.add _ 0 _ _ has_smul.smul _ _, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul ratfunc.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := npow_rec ratfunc.has_mul, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors (polynomial S))) :

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 : polynomial R), dite (⇑φ d ∈ non_zero_divisors (polynomial S)) (λ (h : ⇑φ d ∈ non_zero_divisors (polynomial S)), {to_fraction_ring := localization.mk (⇑φ n) ⟨⇑φ d, h⟩}) (λ (h : ⇑φ d ∉ non_zero_divisors (polynomial S)), 0)) _, map_one' := _, map_mul' := _}

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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors (polynomial S))) (n : polynomial R) (d : ↥(non_zero_divisors (polynomial R))) :

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

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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors (polynomial S))) (hf : function.injective ⇑φ) :

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

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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors (polynomial S))) :

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' := _}

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 (polynomial R) (polynomial S)] (φ : F) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors (polynomial S))) :

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

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

ratfunc R →*₀ G₀

Lift an monoid with zero homomorphism R[X] →*₀ 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 : polynomial R), ⇑φ p / ⇑φ q) _, map_zero' := _, map_one' := _, map_mul' := _}

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] (φ : polynomial R →*₀ G₀) (hφ : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors G₀)) (n : polynomial R) (d : ↥(non_zero_divisors (polynomial R))) :

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

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] (φ : polynomial R →*₀ G₀) (hφ : function.injective ⇑φ) (hφ' : non_zero_divisors (polynomial R) ≤ submonoid.comap φ (non_zero_divisors G₀) := _) :

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

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

ratfunc R →+* L

Lift an injective ring homomorphism R[X] →+* 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' := _}

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

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

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

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

@[protected, instance]

noncomputable def ratfunc.field (K : Type u) [comm_ring K] [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 := _, int_cast := comm_ring.int_cast (ratfunc.comm_ring K), nat_cast := comm_ring.nat_cast (ratfunc.comm_ring K), one := comm_ring.one (ratfunc.comm_ring K), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul (ratfunc.comm_ring K), mul_assoc := _, 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 := _, rat_cast := division_ring.rat_cast._default comm_ring.add _ comm_ring.zero _ _ comm_ring.nsmul _ _ comm_ring.neg comm_ring.sub _ comm_ring.zsmul _ _ _ _ _ comm_ring.int_cast comm_ring.nat_cast comm_ring.one _ _ _ _ comm_ring.mul _ _ _ comm_ring.npow _ _ _ _ has_inv.inv has_div.div _ zpow_rec _ _ _, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul._default (… … _ _ _ _ comm_ring.int_cast comm_ring.nat_cast comm_ring.one _ _ _ _ comm_ring.mul _ _ _ comm_ring.npow _ _ _ _ has_inv.inv has_div.div _ zpow_rec _ _ _) comm_ring.add _ comm_ring.zero _ _ comm_ring.nsmul _ _ comm_ring.neg comm_ring.sub _ comm_ring.zsmul _ _ _ _ _ comm_ring.int_cast comm_ring.nat_cast comm_ring.one _ _ _ _ comm_ring.mul _ _ _ comm_ring.npow _ _ _ _, qsmul_eq_mul' := _}

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

@[protected, instance]

noncomputable def ratfunc.algebra (K : Type u) [comm_ring K] [is_domain K] (R : Type u_1) [comm_semiring R] [algebra R (polynomial K)] :

algebra R (ratfunc K)

Equations

ratfunc.algebra K R = {to_has_smul := {smul := has_smul.smul ratfunc.has_smul}, to_ring_hom := {to_fun := λ (x : R), ratfunc.mk (⇑(algebra_map R (polynomial K)) x) 1, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

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

ratfunc.mk x 1 = ⇑(algebra_map (polynomial K) (ratfunc K)) x

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

{to_fraction_ring := ⇑(algebra_map (polynomial K) (fraction_ring (polynomial K))) x} = ⇑(algebra_map (polynomial K) (ratfunc K)) x

@[simp]

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

ratfunc.mk p q = ⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q

@[simp]

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

⇑(algebra_map (polynomial K) (ratfunc K)) (c • p) / ⇑(algebra_map (polynomial K) (ratfunc K)) q = c • (⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q)

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

⇑(algebra_map R (ratfunc K)) x = ⇑(algebra_map (polynomial K) (ratfunc K)) (⇑(algebra_map R (polynomial K)) x) / ⇑(algebra_map (polynomial K) (ratfunc K)) 1

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

⇑(ratfunc.map φ hφ) (⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q) = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑φ p) / ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑φ q)

@[simp]

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

@[simp]

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

⇑(ratfunc.lift_monoid_with_zero_hom φ hφ) (⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q) = ⇑φ p / ⇑φ q

@[simp]

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

⇑(ratfunc.lift_ring_hom φ hφ) (⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q) = ⇑φ p / ⇑φ q

theorem ratfunc.of_fraction_ring_comp_algebra_map (K : Type u) [comm_ring K] [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) [comm_ring K] [is_domain K] :

function.injective ⇑(algebra_map (polynomial K) (ratfunc K))

@[simp]

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

⇑(algebra_map (polynomial K) (ratfunc K)) x = 0 ↔ x = 0

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

⇑(algebra_map (polynomial K) (ratfunc K)) x ≠ 0

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

ratfunc K →ₐ[S] ratfunc R

Lift an algebra homomorphism that maps polynomials φ : K[X] →ₐ[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' := _}

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

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

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

ratfunc K →ₐ[S] L

Lift an injective algebra homomorphism K[X] →ₐ[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' := _}

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

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

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

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

@[simp]

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

⇑(ratfunc.lift_alg_hom φ hφ) (⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q) = ⇑φ p / ⇑φ q

@[protected, instance]

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

is_fraction_ring (polynomial K) (ratfunc K)

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

@[simp]

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q).lift_on f H = f p q

@[simp]

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q).lift_on' f H = f p q

@[protected]

theorem ratfunc.induction_on {K : Type u} [comm_ring K] [is_domain K] {P : ratfunc K → Prop} (x : ratfunc K) (f : ∀ (p q : polynomial K), q ≠ 0 → P (⇑(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 : K[X], then P holds on all elements of ratfunc K.

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

theorem ratfunc.of_fraction_ring_mk' {K : Type u} [comm_ring K] [is_domain K] (x : polynomial K) (y : ↥(non_zero_divisors (polynomial K))) :

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

@[simp]

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

ratfunc.of_fraction_ring = ⇑(is_localization.alg_equiv (non_zero_divisors (polynomial K)) (fraction_ring (polynomial K)) (ratfunc K))

@[simp]

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

ratfunc.to_fraction_ring = ⇑(is_localization.alg_equiv (non_zero_divisors (polynomial K)) (ratfunc K) (fraction_ring (polynomial K)))

@[simp]

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

(ratfunc.to_fraction_ring_ring_equiv K).symm = (is_localization.alg_equiv (non_zero_divisors (polynomial K)) (fraction_ring (polynomial K)) (ratfunc K)).to_ring_equiv

Numerator and denominator #

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

polynomial K × polynomial K

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 : polynomial K), ite (q = 0) (0, 1) (let r : polynomial K := gcd_monoid.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

@[simp]

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

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

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

polynomial K

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

Equations

x.num = x.num_denom.fst

@[simp]

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

0.num = 0

@[simp]

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

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

@[simp]

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

1.num = 1

@[simp]

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p).num = p

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q).num ∣ p

@[simp]

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

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

A version of num_div_dvd with the LHS in simp normal form

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

polynomial K

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

Equations

x.denom = x.num_denom.snd

@[simp]

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

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

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

x.denom.monic

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

x.denom ≠ 0

@[simp]

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

0.denom = 1

@[simp]

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

1.denom = 1

@[simp]

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p).denom = 1

@[simp]

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

(⇑(algebra_map (polynomial K) (ratfunc K)) p / ⇑(algebra_map (polynomial K) (ratfunc K)) q).denom ∣ q

@[simp]

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

⇑(algebra_map (polynomial K) (ratfunc K)) x.num / ⇑(algebra_map (polynomial K) (ratfunc K)) x.denom = x

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

is_coprime x.num x.denom

@[simp]

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

x.num = 0 ↔ x = 0

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

x.num ≠ 0

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

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

theorem ratfunc.num_denom_add {K : Type u} [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_neg {K : Type u} [field K] (x : ratfunc K) :

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

theorem ratfunc.num_denom_mul {K : Type u} [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} [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} [field K] {x : ratfunc K} {q : polynomial K} (hq : q ≠ 0) :

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

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

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

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

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

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

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

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

⇑φ f.denom ≠ 0

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

⇑(ratfunc.map φ hφ) f = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑φ f.num) / ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑φ f.denom)

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

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

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

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

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

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

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

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

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

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

K →+* ratfunc K

ratfunc.C a is the constant rational function a.

Equations

ratfunc.C = algebra_map K (ratfunc K)

@[simp]

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

algebra_map K (ratfunc K) = ratfunc.C

@[simp]

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

⇑(algebra_map (polynomial K) (ratfunc K)) (⇑polynomial.C a) = ⇑ratfunc.C a

@[simp]

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

(algebra_map (polynomial K) (ratfunc K)).comp polynomial.C = ratfunc.C

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

r • x = ⇑ratfunc.C r * x

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

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

Equations

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

(⇑ratfunc.C c).denom = 1

@[simp]

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

ratfunc.X.num = polynomial.X

@[simp]

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

ratfunc.X.denom = 1

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

ratfunc.X ≠ 0

noncomputable def ratfunc.eval {K : Type u} [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

theorem ratfunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [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} [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

@[simp]

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

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

@[simp]

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

ratfunc.eval f a ratfunc.X = a

@[simp]

theorem ratfunc.eval_zero {K : Type u} [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} [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} [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) :

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

theorem ratfunc.eval_add {K : Type u} [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} [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.