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 polynomialsp/q
tof p q
, iff
is well-defined in the sense thatp/q = p'/q' → f p q = f p' q'
.RatFunc.liftOn'
: define a function by mapping a fraction of polynomialsp/q
tof p q
, iff
is well-defined in the sense thatf (a * p) (a * q) = f p' q'
.RatFunc.induction_on
: ifP
holds onp / q
for all polynomialsp q
, thenP
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 #
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
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
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
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
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
.