# 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.lean`.

## 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] def`s

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 `simp`ed 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://freedommathdance.blogspot.com/2012/11/misconceptions-about-kx.html
- https://stacks.math.columbia.edu/tag/01X1

source
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

- )

Instances For

### Constructing `RatFunc`s and their induction principles #

source
theorem RatFunc.ofFractionRing_injective {K : Type u} [CommRing K] :
Function.Injective ofFractionRing
source
theorem RatFunc.toFractionRing_injective {K : Type u} [CommRing K] :
Function.Injective toFractionRing
source
@[simp]
theorem RatFunc.toFractionRing_inj {K : Type u} [CommRing K] {x y : RatFunc K} :
x.toFractionRing = y.toFractionRing ↔ x = y
source
@[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) ⋯

Instances For

source
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) ⋯
source
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
source
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'
source
@[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 }

Instances For

source
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 }
source
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 }
source
theorem RatFunc.mk_zero {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) :
RatFunc.mk p 0 = { toFractionRing := 0 }
source
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 }
source
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⟩ }
source
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, ⋯⟩ }
source
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, ⋯⟩ }
source
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 }
source
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
source
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
source
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 ⋯
source
@[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 ⋯

Instances For

source
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
source
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`.