Documentation

Mathlib.FieldTheory.RatFunc.Defs

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:

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) [CommRing K] :

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 :: (
  • )
Instances For

    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
    theorem RatFunc.liftOn_def {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (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)
    @[irreducible]
    def RatFunc.liftOn {K : Type u_1} [CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (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
    Instances For
      theorem RatFunc.liftOn_ofFractionRing_mk {K : Type u} [CommRing K] {P : Sort v} (n : Polynomial K) (d : (nonZeroDivisors (Polynomial K))) (f : Polynomial KPolynomial KP) (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 KPolynomial KP} (H : ∀ {p q a : Polynomial K}, q 0a 0f (a * p) (a * q) = f p q) ⦃p : Polynomial K ⦃q : Polynomial K ⦃p' : Polynomial K ⦃q' : Polynomial K (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} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial K) :
      RatFunc.mk p q = { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) p / (algebraMap (Polynomial K) (FractionRing (Polynomial K))) q }
      @[irreducible]
      def RatFunc.mk {K : Type u_1} [CommRing K] [IsDomain K] (p : Polynomial K) (q : Polynomial 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
      Instances For
        theorem RatFunc.mk_eq_div' {K : Type u} [CommRing K] [IsDomain K] (p : Polynomial K) (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 : Polynomial K} {q : Polynomial K} {p' : Polynomial K} {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 : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H' : ∀ {p q p' q' : Polynomial K}, q 0q' 0q' * p = q * p'f p q = f p' q') (H : optParam (∀ {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
        theorem RatFunc.liftOn'_def {K : Type u_1} [CommRing K] [IsDomain K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q a : Polynomial K}, 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} [CommRing K] [IsDomain K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial KPolynomial KP) (H : ∀ {p q a : Polynomial K}, 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} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (q : Polynomial K) (f : Polynomial KPolynomial KP) (f0 : ∀ (p : Polynomial K), f p 0 = f 0 1) (H : ∀ {p q a : Polynomial K}, q 0a 0f (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 KProp} (x : RatFunc K) (_pq : ∀ (p q : Polynomial K), q 0P (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.