# The field of rational functions #

Files in this folder define the field RatFunc K of rational functions over a field K, show it is the field of fractions of K[X] and provide the main results concerning it. This file contains the basic definition.

For connections with Laurent Series, see Mathlib.RingTheory.LaurentSeries.

## Main definitions #

We provide 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

## 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 #

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 :

the coercion to the fraction ring of the polynomial ring

• )
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') :
x.liftOn f H = 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') :
{ toFractionRing := }.liftOn 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'
theorem RatFunc.mk_def {K : Type u_1} [] [] (p : ) (q : ) :
= { toFractionRing := (algebraMap () ()) p / (algebraMap () ()) 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_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 q, hq }
theorem RatFunc.mk_def_of_ne {K : Type u} [] [] (p : ) {q : } (hq : q 0) :
= { toFractionRing := IsLocalization.mk' () p q, }
theorem RatFunc.mk_eq_localization_mk {K : Type u} [] [] (p : ) {q : } (hq : q 0) :
= { toFractionRing := Localization.mk p q, }
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') ) :
().liftOn f H = f p q
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) :
x.liftOn' f H = x.liftOn f
@[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'_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) :
().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.