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

• Kleiman, Misconceptions about $K_X$
• https://freedommathdance.blogspot.com/2012/11/misconceptions-about-kx.html
• https://stacks.math.columbia.edu/tag/01X1

structure RatFunc (K : Type u) [CommRing 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 : FractionRing (Polynomial K)

  the coercion to the fraction ring of the polynomial ring

• )

Constructing RatFuncs and their induction principles

theorem RatFunc.ofFractionRing_injective {K : Type u} [CommRing K] : Function.Injective RatFunc.ofFractionRing

theorem RatFunc.toFractionRing_injective {K : Type u} [CommRing K] : Function.Injective RatFunc.toFractionRing

@[simp]

theorem RatFunc.toFractionRing_eq_iff {K : Type u} [CommRing K] {x y : RatFunc K} : x.toFractionRing = y.toFractionRing ↔ x = y

@[irreducible]

def RatFunc.liftOn {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial K → Polynomial K → P) (H : ∀ {p q p' q' : Polynomial K}, q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → 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

• x.liftOn f H = Localization.liftOn x.toFractionRing (fun (p : Polynomial K) (q : ↥(nonZeroDivisors (Polynomial K))) => f p ↑q) ⋯

theorem RatFunc.liftOn_def {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial K → Polynomial K → P) (H : ∀ {p q p' q' : Polynomial K}, q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q') : x.liftOn f H = Localization.liftOn x.toFractionRing (fun (p : Polynomial K) (q : ↥(nonZeroDivisors (Polynomial K))) => f p ↑q) ⋯

theorem RatFunc.liftOn_ofFractionRing_mk {K : Type u} [CommRing K] {P : Sort v} (n : Polynomial K) (d : ↥(nonZeroDivisors (Polynomial K))) (f : Polynomial K → Polynomial K → P) (H : ∀ {p q p' q' : Polynomial K}, q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q') : { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d

theorem RatFunc.liftOn_condition_of_liftOn'_condition {K : Type u} [CommRing 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'

@[irreducible]

def RatFunc.mk {K : Type u_1} [CommRing K] [IsDomain K] (p q : Polynomial K) : 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 algebraMap _ _ p / algebraMap _ _ q.

Equations

• RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }

theorem RatFunc.mk_def {K : Type u_1} [CommRing K] [IsDomain K] (p q : Polynomial K) : RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }

theorem RatFunc.mk_eq_div' {K : Type u} [CommRing K] [IsDomain K] (p q : Polynomial K) : RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }

theorem RatFunc.mk_zero {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) : RatFunc.mk p 0 = { toFractionRing := 0 }

theorem RatFunc.mk_coe_def {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) (q : ↥(nonZeroDivisors (Polynomial K))) : RatFunc.mk p ↑q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p q }

theorem RatFunc.mk_def_of_mem {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ∈ nonZeroDivisors (Polynomial K)) : RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p ⟨q, hq⟩ }

theorem RatFunc.mk_def_of_ne {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) p ⟨q, ⋯⟩ }

theorem RatFunc.mk_eq_localization_mk {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : RatFunc.mk p q = { toFractionRing := Localization.mk p ⟨q, ⋯⟩ }

theorem RatFunc.mk_one' {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) : RatFunc.mk p 1 = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p }

theorem RatFunc.mk_eq_mk {K : Type u} [CommRing K] [IsDomain 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.liftOn_mk {K : Type u} [CommRing K] [IsDomain 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 ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q' := ⋯) : (RatFunc.mk p q).liftOn f H = f p q

@[irreducible]

def RatFunc.liftOn' {K : Type u_1} [CommRing K] [IsDomain K] {P : Sort u_2} (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) : 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

• x.liftOn' f H = x.liftOn f ⋯

theorem RatFunc.liftOn'_def {K : Type u_1} [CommRing K] [IsDomain K] {P : Sort u_2} (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) : x.liftOn' f H = x.liftOn f ⋯

theorem RatFunc.liftOn'_mk {K : Type u} [CommRing K] [IsDomain 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).liftOn' f H = f p q

theorem RatFunc.induction_on' {K : Type u} [CommRing K] [IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K) (_pq : ∀ (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 algebraMap.