# 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 K[X].

## Main definitions #

Working with rational functions as polynomials:

Working with rational functions as fractions:

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

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

• RatFunc.liftMonoidWithZeroHom lifts a K[X] →*₀ G₀ to a RatFunc K →*₀ G₀, where [CommRing K] [CommGroupWithZero G₀]
• RatFunc.liftRingHom lifts a K[X] →+* L to a RatFunc K →+* L, where [CommRing K] [Field L]
• RatFunc.liftAlgHom lifts a K[X] →ₐ[S] L to a RatFunc K →ₐ[S] L, where [CommRing K] [Field L] [CommSemiring 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 K[X] →* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapRingHom lifts K[X] →+* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapAlgHom lifts K[X] →ₐ[S] R[X] when [CommRing K] [IsDomain K] [CommRing R] [IsDomain R]

We also have a set of recursion and induction principles:

• RatFunc.liftOn: 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.liftOn': 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 :

• intDegree is the degree of a rational function, defined as the difference between the natDegree of its numerator and the natDegree of its denominator. In particular, intDegree 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 IsFractionRing structure, namely RatFunc.ofFractionRing, RatFunc.toFractionRing, RatFunc.mk and RatFunc.toFractionRingRingEquiv. All these maps get simped to bundled morphisms like algebraMap K[X] (RatFunc K) and IsLocalization.algEquiv.

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 #

• [Kleiman, Misconceptions about $K_X$][kleiman1979]
• https://stacks.math.columbia.edu/tag/01X1
structure RatFunc (K : Type u) [] :

RatFunc K is K(X), the field of rational functions over K.

The inclusion of polynomials into RatFunc is algebraMap K[X] (RatFunc K), the maps between RatFunc K and another field of fractions of K[X], especially FractionRing K[X], are given by IsLocalization.algEquiv.

• ofFractionRing :: (
• toFractionRing :
• )
Instances For

### Constructing RatFuncs and their induction principles #

theorem RatFunc.ofFractionRing_injective {K : Type u} [] :
Function.Injective RatFunc.ofFractionRing
theorem RatFunc.toFractionRing_injective {K : Type u} [] :
Function.Injective RatFunc.toFractionRing
theorem RatFunc.liftOn_def {K : Type u_1} [] {P : Sort u_2} (x : ) (f : P) (H : ∀ {p q p' q' : }, q' q' * p = q * p'f p q = f p' q') :
= Localization.liftOn x.toFractionRing (fun (p : ) (q : ()) => f p q)
@[irreducible]
def RatFunc.liftOn {K : Type u_1} [] {P : Sort u_2} (x : ) (f : P) (H : ∀ {p q p' q' : }, q' q' * p = q * p'f 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 : 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 liftOn (p / q) f _ = f p q.

When [IsDomain K], one can use RatFunc.liftOn', 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
Instances For
theorem RatFunc.liftOn_ofFractionRing_mk {K : Type u} [] {P : Sort v} (n : ) (d : ()) (f : P) (H : ∀ {p q p' q' : }, q' q' * p = q * p'f p q = f p' q') :
RatFunc.liftOn { toFractionRing := } f H = f n d
theorem RatFunc.liftOn_condition_of_liftOn'_condition {K : Type u} [] {P : Sort v} {f : P} (H : ∀ {p q a : }, q 0a 0f (a * p) (a * q) = f p q) ⦃p : ⦃q : ⦃p' : ⦃q' : (hq : q 0) (hq' : q' 0) (h : q' * p = q * p') :
f p q = f p' q'
@[irreducible]
def RatFunc.mk {K : Type u_1} [] [] (p : ) (q : ) :

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 algebraMap _ _ p / algebraMap _ _ q.

Equations
Instances For
theorem RatFunc.mk_def {K : Type u_1} [] [] (p : ) (q : ) :
= { toFractionRing := (algebraMap () ()) p / (algebraMap () ()) q }
theorem RatFunc.mk_eq_div' {K : Type u} [] [] (p : ) (q : ) :
= { toFractionRing := (algebraMap () ()) p / (algebraMap () ()) q }
theorem RatFunc.mk_zero {K : Type u} [] [] (p : ) :
= { toFractionRing := 0 }
theorem RatFunc.mk_coe_def {K : Type u} [] [] (p : ) (q : ()) :
RatFunc.mk p q = { toFractionRing := }
theorem RatFunc.mk_def_of_mem {K : Type u} [] [] (p : ) {q : } (hq : ) :
= { toFractionRing := IsLocalization.mk' () p { val := q, property := hq } }
theorem RatFunc.mk_def_of_ne {K : Type u} [] [] (p : ) {q : } (hq : q 0) :
= { toFractionRing := IsLocalization.mk' () p { val := q, property := } }
theorem RatFunc.mk_eq_localization_mk {K : Type u} [] [] (p : ) {q : } (hq : q 0) :
= { toFractionRing := Localization.mk p { val := q, property := } }
theorem RatFunc.mk_one' {K : Type u} [] [] (p : ) :
= { toFractionRing := (algebraMap () ()) p }
theorem RatFunc.mk_eq_mk {K : Type u} [] [] {p : } {q : } {p' : } {q' : } (hq : q 0) (hq' : q' 0) :
= RatFunc.mk p' q' p * q' = p' * q
theorem RatFunc.liftOn_mk {K : Type u} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H' : ∀ {p q p' q' : }, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {p q p' q' : }, q' q' * p = q * p'f p q = f p' q') ) :
RatFunc.liftOn () f H = f p q
@[irreducible]
def RatFunc.liftOn' {K : Type u_1} [] [] {P : Sort u_2} (x : ) (f : P) (H : ∀ {p q a : }, 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
Instances For
theorem RatFunc.liftOn'_def {K : Type u_1} [] [] {P : Sort u_2} (x : ) (f : P) (H : ∀ {p q a : }, q 0a 0f (a * p) (a * q) = f p q) :
=
theorem RatFunc.liftOn'_mk {K : Type u} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H : ∀ {p q a : }, q 0a 0f (a * p) (a * q) = f p q) :
RatFunc.liftOn' () f H = f p q
theorem RatFunc.induction_on' {K : Type u} [] [] {P : Prop} (x : ) (_pq : ∀ (p q : ), q 0P ()) :
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 algebraMap.

### Defining the field structure #

@[irreducible]
def RatFunc.zero {K : Type u_1} [] :

The zero rational function.

Equations
Instances For
theorem RatFunc.zero_def {K : Type u_1} [] :
RatFunc.zero = { toFractionRing := 0 }
instance RatFunc.instZeroRatFunc {K : Type u} [] :
Zero ()
Equations
• RatFunc.instZeroRatFunc = { zero := RatFunc.zero }
theorem RatFunc.ofFractionRing_zero {K : Type u} [] :
{ toFractionRing := 0 } = 0
theorem RatFunc.add_def {K : Type u_1} [] :
∀ (x x_1 : ), RatFunc.add x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }
@[irreducible]
def RatFunc.add {K : Type u_1} [] :

Equations
Instances For
instance RatFunc.instAddRatFunc {K : Type u} [] :
Equations
theorem RatFunc.ofFractionRing_add {K : Type u} [] (p : ) (q : ) :
{ toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }
theorem RatFunc.sub_def {K : Type u_1} [] :
∀ (x x_1 : ), RatFunc.sub x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }
@[irreducible]
def RatFunc.sub {K : Type u_1} [] :

Subtraction of rational functions.

Equations
Instances For
instance RatFunc.instSubRatFunc {K : Type u} [] :
Sub ()
Equations
• RatFunc.instSubRatFunc = { sub := RatFunc.sub }
theorem RatFunc.ofFractionRing_sub {K : Type u} [] (p : ) (q : ) :
{ toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }
theorem RatFunc.neg_def {K : Type u_1} [] :
∀ (x : ), = match x with | { toFractionRing := p } => { toFractionRing := -p }
@[irreducible]
def RatFunc.neg {K : Type u_1} [] :

Additive inverse of a rational function.

Equations
Instances For
instance RatFunc.instNegRatFunc {K : Type u} [] :
Neg ()
Equations
• RatFunc.instNegRatFunc = { neg := RatFunc.neg }
theorem RatFunc.ofFractionRing_neg {K : Type u} [] (p : ) :
{ toFractionRing := -p } = -{ toFractionRing := p }
theorem RatFunc.one_def {K : Type u_1} [] :
RatFunc.one = { toFractionRing := 1 }
@[irreducible]
def RatFunc.one {K : Type u_1} [] :

The multiplicative unit of rational functions.

Equations
Instances For
instance RatFunc.instOneRatFunc {K : Type u} [] :
One ()
Equations
• RatFunc.instOneRatFunc = { one := RatFunc.one }
theorem RatFunc.ofFractionRing_one {K : Type u} [] :
{ toFractionRing := 1 } = 1
@[irreducible]
def RatFunc.mul {K : Type u_1} [] :

Multiplication of rational functions.

Equations
Instances For
theorem RatFunc.mul_def {K : Type u_1} [] :
∀ (x x_1 : ), RatFunc.mul x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }
instance RatFunc.instMulRatFunc {K : Type u} [] :
Mul ()
Equations
• RatFunc.instMulRatFunc = { mul := RatFunc.mul }
theorem RatFunc.ofFractionRing_mul {K : Type u} [] (p : ) (q : ) :
{ toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }
theorem RatFunc.div_def {K : Type u_1} [] [] :
∀ (x x_1 : ), RatFunc.div x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
@[irreducible]
def RatFunc.div {K : Type u_1} [] [] :

Division of rational functions.

Equations
Instances For
instance RatFunc.instDivRatFunc {K : Type u} [] [] :
Div ()
Equations
• RatFunc.instDivRatFunc = { div := RatFunc.div }
theorem RatFunc.ofFractionRing_div {K : Type u} [] [] (p : ) (q : ) :
{ toFractionRing := p / q } = { toFractionRing := p } / { toFractionRing := q }
@[irreducible]
def RatFunc.inv {K : Type u_1} [] [] :

Multiplicative inverse of a rational function.

Equations
Instances For
theorem RatFunc.inv_def {K : Type u_1} [] [] :
∀ (x : ), = match x with | { toFractionRing := p } => { toFractionRing := p⁻¹ }
instance RatFunc.instInvRatFunc {K : Type u} [] [] :
Inv ()
Equations
• RatFunc.instInvRatFunc = { inv := RatFunc.inv }
theorem RatFunc.ofFractionRing_inv {K : Type u} [] [] (p : ) :
{ toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹
theorem RatFunc.mul_inv_cancel {K : Type u} [] [] {p : } :
p 0p * p⁻¹ = 1
theorem RatFunc.smul_def {K : Type u_2} [] {R : Type u_3} [SMul R ()] :
∀ (x : R) (x_1 : ), RatFunc.smul x x_1 = match x, x_1 with | r, { toFractionRing := p } => { toFractionRing := r p }
@[irreducible]
def RatFunc.smul {K : Type u_2} [] {R : Type u_3} [SMul R ()] :
R

Scalar multiplication of rational functions.

Equations
Instances For
instance RatFunc.instSMulRatFunc {K : Type u} [] {R : Type u_1} [SMul R ()] :
SMul R ()
Equations
• RatFunc.instSMulRatFunc = { smul := RatFunc.smul }
theorem RatFunc.ofFractionRing_smul {K : Type u} [] {R : Type u_1} [SMul R ()] (c : R) (p : ) :
{ toFractionRing := c p } = c { toFractionRing := p }
theorem RatFunc.toFractionRing_smul {K : Type u} [] {R : Type u_1} [SMul R ()] (c : R) (p : ) :
(c p).toFractionRing = c p.toFractionRing
theorem RatFunc.smul_eq_C_smul {K : Type u} [] (x : ) (r : K) :
r x = Polynomial.C r x
theorem RatFunc.mk_smul {K : Type u} [] {R : Type u_1} [] [] [] [IsScalarTower R () ()] (c : R) (p : ) (q : ) :
RatFunc.mk (c p) q = c
instance RatFunc.instSubsingletonRatFunc (K : Type u) [] [] :
Equations
• =
Equations
• = { default := 0 }
instance RatFunc.instNontrivial (K : Type u) [] [] :
Equations
• =
@[simp]
theorem RatFunc.toFractionRingRingEquiv_apply (K : Type u) [] (self : ) :
self = self.toFractionRing

RatFunc K is isomorphic to the field of fractions of K[X], as rings.

This is an auxiliary definition; simp-normal form is IsLocalization.algEquiv.

Equations
• = { toEquiv := { toFun := RatFunc.toFractionRing, invFun := RatFunc.ofFractionRing, left_inv := , right_inv := }, map_mul' := , map_add' := }
Instances For

Solve equations for RatFunc K by working in FractionRing K[X].

Equations
Instances For

Solve equations for RatFunc K by applying RatFunc.induction_on.

Equations
Instances For
def RatFunc.instCommMonoid (K : Type u) [] :

RatFunc K is a commutative monoid.

This is an intermediate step on the way to the full instance RatFunc.instCommRing.

Equations
Instances For

RatFunc K is an additive commutative group.

This is an intermediate step on the way to the full instance RatFunc.instCommRing.

Equations
Instances For
instance RatFunc.instCommRing (K : Type u) [] :
Equations
• = let __src := ; let __src_1 := ;
def RatFunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F () ()] [MonoidHomClass F () ()] (φ : F) (hφ : ) :

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
• One or more equations did not get rendered due to their size.
Instances For
theorem RatFunc.map_apply_ofFractionRing_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F () ()] [MonoidHomClass F () ()] (φ : F) (hφ : ) (n : ) (d : ()) :
(RatFunc.map φ ) { toFractionRing := } = { toFractionRing := Localization.mk (φ n) { val := φ d, property := } }
theorem RatFunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F () ()] [MonoidHomClass F () ()] (φ : F) (hφ : ) (hf : ) :
def RatFunc.mapRingHom {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F () ()] [RingHomClass F () ()] (φ : F) (hφ : ) :

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
• = let __src := RatFunc.map φ ; { toMonoidHom := __src, map_zero' := , map_add' := }
Instances For
theorem RatFunc.coe_mapRingHom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F () ()] [RingHomClass F () ()] (φ : F) (hφ : ) :
() = (RatFunc.map φ )
def RatFunc.liftMonoidWithZeroHom {G₀ : Type u_1} {R : Type u_3} [] [] (φ : →*₀ G₀) (hφ : ) :
→*₀ G₀

Lift a 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
• One or more equations did not get rendered due to their size.
Instances For
theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk {G₀ : Type u_1} {R : Type u_3} [] [] (φ : →*₀ G₀) (hφ : ) (n : ) (d : ()) :
{ toFractionRing := } = φ n / φ d
theorem RatFunc.liftMonoidWithZeroHom_injective {G₀ : Type u_1} {R : Type u_3} [] [] [] (φ : →*₀ G₀) (hφ : ) (hφ' : optParam () ) :
def RatFunc.liftRingHom {L : Type u_2} {R : Type u_3} [] [] (φ : ) (hφ : ) :

Lift an injective ring homomorphism R[X] →+* L to a RatFunc R →+* L by mapping both the numerator and denominator and quotienting them.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem RatFunc.liftRingHom_apply_ofFractionRing_mk {L : Type u_2} {R : Type u_3} [] [] (φ : ) (hφ : ) (n : ) (d : ()) :
() { toFractionRing := } = φ n / φ d
theorem RatFunc.liftRingHom_injective {L : Type u_2} {R : Type u_3} [] [] [] (φ : ) (hφ : ) (hφ' : optParam () ) :
instance RatFunc.instField (K : Type u) [] [] :
Equations
• = let __src := ; let __src_1 := ; Field.mk zpowRec (qsmulRec fun (a : ) => a)

### RatFunc as field of fractions of Polynomial#

Equations
• One or more equations did not get rendered due to their size.
theorem RatFunc.mk_one {K : Type u} [] [] (x : ) :
= (algebraMap () ()) x
theorem RatFunc.ofFractionRing_algebraMap {K : Type u} [] [] (x : ) :
{ toFractionRing := (algebraMap () ()) x } = (algebraMap () ()) x
@[simp]
theorem RatFunc.mk_eq_div {K : Type u} [] [] (p : ) (q : ) :
= (algebraMap () ()) p / (algebraMap () ()) q
@[simp]
theorem RatFunc.div_smul {K : Type u} [] [] {R : Type u_1} [] [] [IsScalarTower R () ()] (c : R) (p : ) (q : ) :
(algebraMap () ()) (c p) / (algebraMap () ()) q = c ((algebraMap () ()) p / (algebraMap () ()) q)
theorem RatFunc.algebraMap_apply {K : Type u} [] [] {R : Type u_1} [] [Algebra R ()] (x : R) :
(algebraMap R ()) x = (algebraMap () ()) ((algebraMap R ()) x) / (algebraMap () ()) 1
theorem RatFunc.map_apply_div_ne_zero {K : Type u} [] [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F () ()] [MonoidHomClass F () ()] (φ : F) (hφ : ) (p : ) (q : ) (hq : q 0) :
(RatFunc.map φ ) ((algebraMap () ()) p / (algebraMap () ()) q) = (algebraMap () ()) (φ p) / (algebraMap () ()) (φ q)
@[simp]
theorem RatFunc.map_apply_div {K : Type u} [] [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F () ()] [] (φ : F) (hφ : ) (p : ) (q : ) :
(RatFunc.map φ ) ((algebraMap () ()) p / (algebraMap () ()) q) = (algebraMap () ()) (φ p) / (algebraMap () ()) (φ q)
theorem RatFunc.liftMonoidWithZeroHom_apply_div {K : Type u} [] [] {L : Type u_1} (φ : ) (hφ : ) (p : ) (q : ) :
((algebraMap () ()) p / (algebraMap () ()) q) = φ p / φ q
@[simp]
theorem RatFunc.liftMonoidWithZeroHom_apply_div' {K : Type u} [] [] {L : Type u_1} (φ : ) (hφ : ) (p : ) (q : ) :
((algebraMap () ()) p) / ((algebraMap () ()) q) = φ p / φ q
theorem RatFunc.liftRingHom_apply_div {K : Type u} [] [] {L : Type u_1} [] (φ : ) (hφ : ) (p : ) (q : ) :
() ((algebraMap () ()) p / (algebraMap () ()) q) = φ p / φ q
@[simp]
theorem RatFunc.liftRingHom_apply_div' {K : Type u} [] [] {L : Type u_1} [] (φ : ) (hφ : ) (p : ) (q : ) :
() ((algebraMap () ()) p) / () ((algebraMap () ()) q) = φ p / φ q
theorem RatFunc.ofFractionRing_comp_algebraMap (K : Type u) [] [] :
RatFunc.ofFractionRing (algebraMap () ()) = (algebraMap () ())
@[simp]
theorem RatFunc.algebraMap_eq_zero_iff (K : Type u) [] [] {x : } :
(algebraMap () ()) x = 0 x = 0
theorem RatFunc.algebraMap_ne_zero {K : Type u} [] [] {x : } (hx : x 0) :
(algebraMap () ()) x 0
def RatFunc.mapAlgHom {K : Type u} [] [] {R : Type u_2} {S : Type u_3} [] [] [] [Algebra S ()] [Algebra S ()] (φ : ) (hφ : ) :

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
• = let __src := ; { toRingHom := __src, commutes' := }
Instances For
theorem RatFunc.coe_mapAlgHom_eq_coe_map {K : Type u} [] [] {R : Type u_2} {S : Type u_3} [] [] [] [Algebra S ()] [Algebra S ()] (φ : ) (hφ : ) :
() = (RatFunc.map φ )
def RatFunc.liftAlgHom {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) :

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
Instances For
theorem RatFunc.liftAlgHom_apply_ofFractionRing_mk {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (n : ) (d : ()) :
() { toFractionRing := } = φ n / φ d
theorem RatFunc.liftAlgHom_injective {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (hφ' : optParam () ) :
@[simp]
theorem RatFunc.liftAlgHom_apply_div' {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (p : ) (q : ) :
() ((algebraMap () ()) p) / () ((algebraMap () ()) q) = φ p / φ q
theorem RatFunc.liftAlgHom_apply_div {K : Type u} [] [] {L : Type u_1} {S : Type u_3} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (p : ) (q : ) :
() ((algebraMap () ()) p / (algebraMap () ()) q) = φ p / φ q

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

Equations
• =
@[simp]
theorem RatFunc.liftOn_div {K : Type u} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H' : ∀ {p q p' q' : }, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {p q p' q' : }, q' q' * p = q * p'f p q = f p' q') ) :
RatFunc.liftOn ((algebraMap () ()) p / (algebraMap () ()) q) f H = f p q
@[simp]
theorem RatFunc.liftOn'_div {K : Type u} [] [] {P : Sort v} (p : ) (q : ) (f : P) (f0 : ∀ (p : ), f p 0 = f 0 1) (H : ∀ {p q a : }, q 0a 0f (a * p) (a * q) = f p q) :
RatFunc.liftOn' ((algebraMap () ()) p / (algebraMap () ()) q) f H = f p q
theorem RatFunc.induction_on {K : Type u} [] [] {P : Prop} (x : ) (f : ∀ (p q : ), q 0P ((algebraMap () ()) p / (algebraMap () ()) 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.ofFractionRing_mk' {K : Type u} [] [] (x : ) (y : ()) :
{ toFractionRing := } =
@[simp]
theorem RatFunc.ofFractionRing_eq {K : Type u} [] [] :
RatFunc.ofFractionRing = ()
@[simp]
theorem RatFunc.toFractionRing_eq {K : Type u} [] [] :
RatFunc.toFractionRing = ()
@[simp]

### Numerator and denominator #

def RatFunc.numDenom {K : Type u} [] (x : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem RatFunc.numDenom_div {K : Type u} [] (p : ) {q : } (hq : q 0) :
RatFunc.numDenom ((algebraMap () ()) p / (algebraMap () ()) q) = (Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q), Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q))
def RatFunc.num {K : Type u} [] (x : ) :

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

Equations
• = ().1
Instances For
@[simp]
theorem RatFunc.num_zero {K : Type u} [] :
= 0
@[simp]
theorem RatFunc.num_div {K : Type u} [] (p : ) (q : ) :
RatFunc.num ((algebraMap () ()) p / (algebraMap () ()) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q)
@[simp]
theorem RatFunc.num_one {K : Type u} [] :
= 1
@[simp]
theorem RatFunc.num_algebraMap {K : Type u} [] (p : ) :
RatFunc.num ((algebraMap () ()) p) = p
theorem RatFunc.num_div_dvd {K : Type u} [] (p : ) {q : } (hq : q 0) :
RatFunc.num ((algebraMap () ()) p / (algebraMap () ()) q) p
@[simp]
theorem RatFunc.num_div_dvd' {K : Type u} [] (p : ) {q : } (hq : q 0) :
Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q) p

A version of num_div_dvd with the LHS in simp normal form

def RatFunc.denom {K : Type u} [] (x : ) :

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

Equations
• = ().2
Instances For
@[simp]
theorem RatFunc.denom_div {K : Type u} [] (p : ) {q : } (hq : q 0) :
RatFunc.denom ((algebraMap () ()) p / (algebraMap () ()) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q)
theorem RatFunc.monic_denom {K : Type u} [] (x : ) :
theorem RatFunc.denom_ne_zero {K : Type u} [] (x : ) :
@[simp]
theorem RatFunc.denom_zero {K : Type u} [] :
@[simp]
theorem RatFunc.denom_one {K : Type u} [] :
@[simp]
theorem RatFunc.denom_algebraMap {K : Type u} [] (p : ) :
RatFunc.denom ((algebraMap () ()) p) = 1
@[simp]
theorem RatFunc.denom_div_dvd {K : Type u} [] (p : ) (q : ) :
RatFunc.denom ((algebraMap () ()) p / (algebraMap () ()) q) q
@[simp]
theorem RatFunc.num_div_denom {K : Type u} [] (x : ) :
(algebraMap () ()) () / (algebraMap () ()) () = x
theorem RatFunc.isCoprime_num_denom {K : Type u} [] (x : ) :
@[simp]
theorem RatFunc.num_eq_zero_iff {K : Type u} [] {x : } :
= 0 x = 0
theorem RatFunc.num_ne_zero {K : Type u} [] {x : } (hx : x 0) :
0
theorem RatFunc.num_mul_eq_mul_denom_iff {K : Type u} [] {x : } {p : } {q : } (hq : q 0) :
* q = x = (algebraMap () ()) p / (algebraMap () ()) q
theorem RatFunc.num_denom_add {K : Type u} [] (x : ) (y : ) :
RatFunc.num (x + y) * () = () * RatFunc.denom (x + y)
theorem RatFunc.num_denom_neg {K : Type u} [] (x : ) :
=
theorem RatFunc.num_denom_mul {K : Type u} [] (x : ) (y : ) :
RatFunc.num (x * y) * () = * RatFunc.denom (x * y)
theorem RatFunc.num_dvd {K : Type u} [] {x : } {p : } (hp : p 0) :
p ∃ (q : ), q 0 x = (algebraMap () ()) p / (algebraMap () ()) q
theorem RatFunc.denom_dvd {K : Type u} [] {x : } {q : } (hq : q 0) :
∃ (p : ), x = (algebraMap () ()) p / (algebraMap () ()) q
theorem RatFunc.num_mul_dvd {K : Type u} [] (x : ) (y : ) :
theorem RatFunc.denom_mul_dvd {K : Type u} [] (x : ) (y : ) :
theorem RatFunc.denom_add_dvd {K : Type u} [] (x : ) (y : ) :
theorem RatFunc.map_denom_ne_zero {K : Type u} [] {L : Type u_1} {F : Type u_2} [Zero L] [FunLike F () L] [ZeroHomClass F () L] (φ : F) (hφ : ) (f : ) :
φ () 0
theorem RatFunc.map_apply {K : Type u} [] {R : Type u_1} {F : Type u_2} [] [] [FunLike F () ()] [MonoidHomClass F () ()] (φ : F) (hφ : ) (f : ) :
(RatFunc.map φ ) f = (algebraMap () ()) (φ ()) / (algebraMap () ()) (φ ())
theorem RatFunc.liftMonoidWithZeroHom_apply {K : Type u} [] {L : Type u_1} (φ : ) (hφ : ) (f : ) :
f = φ () / φ ()
theorem RatFunc.liftRingHom_apply {K : Type u} [] {L : Type u_1} [] (φ : ) (hφ : ) (f : ) :
() f = φ () / φ ()
theorem RatFunc.liftAlgHom_apply {K : Type u} [] {L : Type u_1} {S : Type u_2} [] [] [Algebra S ()] [Algebra S L] (φ : →ₐ[S] L) (hφ : ) (f : ) :
() f = φ () / φ ()
theorem RatFunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [] {x : } {y : } (hxy : x + y 0) :
0

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

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

RatFunc.C a is the constant rational function a.

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

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

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

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

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

theorem RatFunc.eval_mul {K : Type u} [] {L : Type u_1} [] (f : K →+* L) (a : L) {x : } {y : } (hx : 0) (hy : 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).

def RatFunc.intDegree {K : Type u} [] (x : ) :

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

Equations
Instances For
@[simp]
theorem RatFunc.intDegree_zero {K : Type u} [] :
@[simp]
theorem RatFunc.intDegree_one {K : Type u} [] :
@[simp]
theorem RatFunc.intDegree_C {K : Type u} [] (k : K) :
RatFunc.intDegree (RatFunc.C k) = 0
@[simp]
theorem RatFunc.intDegree_X {K : Type u} [] :
RatFunc.intDegree RatFunc.X = 1
@[simp]
theorem RatFunc.intDegree_polynomial {K : Type u} [] {p : } :
theorem RatFunc.intDegree_mul {K : Type u} [] {x : } {y : } (hx : x 0) (hy : y 0) :
@[simp]
theorem RatFunc.intDegree_neg {K : Type u} [] (x : ) :
theorem RatFunc.intDegree_add {K : Type u} [] {x : } {y : } (hxy : x + y 0) :
RatFunc.intDegree (x + y) = () -
theorem RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree {K : Type u} [] {x : } (hx : x 0) {s : } (hs : s 0) :
() - () =
theorem RatFunc.intDegree_add_le {K : Type u} [] {x : } {y : } (hy : y 0) (hxy : x + y 0) :
def RatFunc.coeAlgHom (F : Type u) [] :

The coercion RatFunc F → LaurentSeries F as bundled alg hom.

Equations
Instances For
def RatFunc.coeToLaurentSeries_fun {F : Type u} [] :

The coercion RatFunc F → LaurentSeries F as a function.

This is the implementation of coeToLaurentSeries.

Equations
• RatFunc.coeToLaurentSeries_fun =
Instances For
instance RatFunc.coeToLaurentSeries {F : Type u} [] :
Coe () ()
Equations
• RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }
theorem RatFunc.coe_def {F : Type u} [] (f : ) :
f = f
theorem RatFunc.coe_num_denom {F : Type u} [] (f : ) :
f = () / ()
theorem RatFunc.coe_injective {F : Type u} [] :
Function.Injective RatFunc.coeToLaurentSeries_fun
@[simp]
theorem RatFunc.coe_apply {F : Type u} [] (f : ) :
f = f
@[simp]
theorem RatFunc.coe_zero {F : Type u} [] :
0 = 0
@[simp]
theorem RatFunc.coe_one {F : Type u} [] :
1 = 1
@[simp]
theorem RatFunc.coe_add {F : Type u} [] (f : ) (g : ) :
(f + g) = f + g
@[simp]
theorem RatFunc.coe_sub {F : Type u} [] (f : ) (g : ) :
(f - g) = f - g
@[simp]
theorem RatFunc.coe_neg {F : Type u} [] (f : ) :
(-f) = -f
@[simp]
theorem RatFunc.coe_mul {F : Type u} [] (f : ) (g : ) :
(f * g) = f * g
@[simp]
theorem RatFunc.coe_pow {F : Type u} [] (f : ) (n : ) :
(f ^ n) = f ^ n
@[simp]
theorem RatFunc.coe_div {F : Type u} [] (f : ) (g : ) :
(f / g) = f / g
@[simp]
theorem RatFunc.coe_C {F : Type u} [] (r : F) :
(RatFunc.C r) = HahnSeries.C r
@[simp]
theorem RatFunc.coe_smul {F : Type u} [] (f : ) (r : F) :
(r f) = r f
@[simp]
theorem RatFunc.coe_X {F : Type u} [] :
RatFunc.X = 1
Equations
• One or more equations did not get rendered due to their size.
theorem RatFunc.algebraMap_apply_div {F : Type u} [] (p : ) (q : ) :
(algebraMap () ()) ((algebraMap () ()) p / (algebraMap () ()) q) = () p / () q