The field of rational functions

This file defines the field RatFunc K of rational functions over a field K, and shows it is the field of fractions of K[X].

Main definitions

Working with rational functions as polynomials:

• RatFunc.instField provides a field structure
• RatFunc.C is the constant polynomial
• RatFunc.X is the indeterminate
• RatFunc.eval evaluates a rational function given a value for the indeterminate You can use IsFractionRing API to treat RatFunc as the field of fractions of polynomials:

• algebraMap K[X] (RatFunc K) maps polynomials to rational functions
• IsFractionRing.algEquiv maps other fields of fractions of K[X] to RatFunc K, in particular:
• FractionRing.algEquiv K[X] (RatFunc K) maps the generic field of fraction construction to RatFunc K. Combine this with AlgEquiv.restrictScalars to change the FractionRing K[X] ≃ₐ[K[X]] RatFunc K to FractionRing K[X] ≃ₐ[K] RatFunc K.

Working with rational functions as fractions:

• RatFunc.num and RatFunc.denom give the numerator and denominator. These values are chosen to be coprime and such that RatFunc.denom is monic.

Embedding of rational functions into Laurent series, provided as a coercion, utilizing the underlying RatFunc.coeAlgHom.

Lifting homomorphisms of polynomials to other types, by mapping and dividing, as long as the homomorphism retains the non-zero-divisor property:

• RatFunc.liftMonoidWithZeroHom lifts a K[X] →*₀ G₀ to a RatFunc K →*₀ G₀, where [CommRing K] [CommGroupWithZero G₀]
• RatFunc.liftRingHom lifts a K[X] →+* L to a RatFunc K →+* L, where [CommRing K] [Field L]
• RatFunc.liftAlgHom lifts a K[X] →ₐ[S] L to a RatFunc K →ₐ[S] L, where [CommRing K] [Field L] [CommSemiring S] [Algebra S K[X]] [Algebra S L] This is satisfied by injective homs. We also have lifting homomorphisms of polynomials to other polynomials, with the same condition on retaining the non-zero-divisor property across the map:
• RatFunc.map lifts K[X] →* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapRingHom lifts K[X] →+* R[X] when [CommRing K] [CommRing R]
• RatFunc.mapAlgHom lifts K[X] →ₐ[S] R[X] when [CommRing K] [IsDomain K] [CommRing R] [IsDomain R]

We also have 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

We define the degree of a rational function, with values in ℤ:

• intDegree is the degree of a rational function, defined as the difference between the natDegree of its numerator and the natDegree of its denominator. In particular, intDegree 0 = 0.

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$][kleiman1979]
• 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)
• )

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 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') : RatFunc.liftOn x f H = Localization.liftOn x.toFractionRing (fun (p : Polynomial K) (q : ↥(nonZeroDivisors (Polynomial K))) => f p ↑q) (_ : ∀ {p p' : Polynomial K} {q q' : ↥(nonZeroDivisors (Polynomial K))}, (Localization.r (nonZeroDivisors (Polynomial K))) (p, q) (p', q') → f p ↑q = f p' ↑q')

@[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

• @RatFunc.liftOn = RatFunc.wrapped✝.1

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') : RatFunc.liftOn { toFractionRing := Localization.mk n d } 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 : 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'

@[irreducible]

def RatFunc.mk {K : Type u_1} [CommRing K] [IsDomain K] (p : Polynomial K) (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 = RatFunc.wrapped✝.1

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 }

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 { val := q, property := 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 { val := q, property := (_ : q ∈ nonZeroDivisors (Polynomial K)) } }

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 { val := q, property := (_ : q ∈ nonZeroDivisors (Polynomial K)) } }

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 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 : 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') (_ : ∀ {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.liftOn (RatFunc.mk p q) 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

• @RatFunc.liftOn' = RatFunc.wrapped✝.1

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) : RatFunc.liftOn' x f H = RatFunc.liftOn x f (_ : ∀ {_p _q _p' _q' : Polynomial K}, _q ∈ nonZeroDivisors (Polynomial K) → _q' ∈ nonZeroDivisors (Polynomial K) → _q' * _p = _q * _p' → f _p _q = f _p' _q')

theorem RatFunc.liftOn'_mk {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (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.liftOn' (RatFunc.mk p q) 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.

Defining the field structure

@[irreducible]

def RatFunc.zero {K : Type u_1} [CommRing K] : RatFunc K

The zero rational function.

Equations

• @RatFunc.zero = RatFunc.wrapped✝.1

theorem RatFunc.zero_def {K : Type u_1} [CommRing K] : RatFunc.zero = { toFractionRing := 0 }

instance RatFunc.instZeroRatFunc {K : Type u} [CommRing K] : Zero (RatFunc K)

Equations

• RatFunc.instZeroRatFunc = { zero := RatFunc.zero }

theorem RatFunc.ofFractionRing_zero {K : Type u} [CommRing K] : { toFractionRing := 0 } = 0

theorem RatFunc.add_def {K : Type u_1} [CommRing K] : ∀ (x x_1 : RatFunc K), RatFunc.add x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p + q }

@[irreducible]

def RatFunc.add {K : Type u_1} [CommRing K] : RatFunc K → RatFunc K → RatFunc K

Addition of rational functions.

Equations

• @RatFunc.add = RatFunc.wrapped✝.1

instance RatFunc.instAddRatFunc {K : Type u} [CommRing K] : Add (RatFunc K)

Equations

• RatFunc.instAddRatFunc = { add := RatFunc.add }

theorem RatFunc.ofFractionRing_add {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) : { toFractionRing := p + q } = { toFractionRing := p } + { toFractionRing := q }

theorem RatFunc.sub_def {K : Type u_1} [CommRing K] : ∀ (x x_1 : RatFunc K), RatFunc.sub x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p - q }

@[irreducible]

def RatFunc.sub {K : Type u_1} [CommRing K] : RatFunc K → RatFunc K → RatFunc K

Subtraction of rational functions.

Equations

• @RatFunc.sub = RatFunc.wrapped✝.1

instance RatFunc.instSubRatFunc {K : Type u} [CommRing K] : Sub (RatFunc K)

Equations

• RatFunc.instSubRatFunc = { sub := RatFunc.sub }

theorem RatFunc.ofFractionRing_sub {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) : { toFractionRing := p - q } = { toFractionRing := p } - { toFractionRing := q }

theorem RatFunc.neg_def {K : Type u_1} [CommRing K] : ∀ (x : RatFunc K), RatFunc.neg x = match x with | { toFractionRing := p } => { toFractionRing := -p }

@[irreducible]

def RatFunc.neg {K : Type u_1} [CommRing K] : RatFunc K → RatFunc K

Additive inverse of a rational function.

Equations

• @RatFunc.neg = RatFunc.wrapped✝.1

instance RatFunc.instNegRatFunc {K : Type u} [CommRing K] : Neg (RatFunc K)

Equations

• RatFunc.instNegRatFunc = { neg := RatFunc.neg }

theorem RatFunc.ofFractionRing_neg {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) : { toFractionRing := -p } = -{ toFractionRing := p }

theorem RatFunc.one_def {K : Type u_1} [CommRing K] : RatFunc.one = { toFractionRing := 1 }

@[irreducible]

def RatFunc.one {K : Type u_1} [CommRing K] : RatFunc K

The multiplicative unit of rational functions.

Equations

• @RatFunc.one = RatFunc.wrapped✝.1

instance RatFunc.instOneRatFunc {K : Type u} [CommRing K] : One (RatFunc K)

Equations

• RatFunc.instOneRatFunc = { one := RatFunc.one }

theorem RatFunc.ofFractionRing_one {K : Type u} [CommRing K] : { toFractionRing := 1 } = 1

@[irreducible]

def RatFunc.mul {K : Type u_1} [CommRing K] : RatFunc K → RatFunc K → RatFunc K

Multiplication of rational functions.

Equations

• @RatFunc.mul = RatFunc.wrapped✝.1

theorem RatFunc.mul_def {K : Type u_1} [CommRing K] : ∀ (x x_1 : RatFunc K), RatFunc.mul x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p * q }

instance RatFunc.instMulRatFunc {K : Type u} [CommRing K] : Mul (RatFunc K)

Equations

• RatFunc.instMulRatFunc = { mul := RatFunc.mul }

theorem RatFunc.ofFractionRing_mul {K : Type u} [CommRing K] (p : FractionRing (Polynomial K)) (q : FractionRing (Polynomial K)) : { toFractionRing := p * q } = { toFractionRing := p } * { toFractionRing := q }

theorem RatFunc.div_def {K : Type u_1} [CommRing K] [IsDomain K] : ∀ (x x_1 : RatFunc K), RatFunc.div x x_1 = match x, x_1 with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }

@[irreducible]

def RatFunc.div {K : Type u_1} [CommRing K] [IsDomain K] : RatFunc K → RatFunc K → RatFunc K

Division of rational functions.

Equations

• @RatFunc.div = RatFunc.wrapped✝.1

instance RatFunc.instDivRatFunc {K : Type u} [CommRing K] [IsDomain K] : Div (RatFunc K)

Equations

• RatFunc.instDivRatFunc = { div := RatFunc.div }

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

@[irreducible]

def RatFunc.inv {K : Type u_1} [CommRing K] [IsDomain K] : RatFunc K → RatFunc K

Multiplicative inverse of a rational function.

Equations

• @RatFunc.inv = RatFunc.wrapped✝.1

theorem RatFunc.inv_def {K : Type u_1} [CommRing K] [IsDomain K] : ∀ (x : RatFunc K), RatFunc.inv x = match x with | { toFractionRing := p } => { toFractionRing := p⁻¹ }

instance RatFunc.instInvRatFunc {K : Type u} [CommRing K] [IsDomain K] : Inv (RatFunc K)

Equations

• RatFunc.instInvRatFunc = { inv := RatFunc.inv }

theorem RatFunc.ofFractionRing_inv {K : Type u} [CommRing K] [IsDomain K] (p : FractionRing (Polynomial K)) : { toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹

theorem RatFunc.mul_inv_cancel {K : Type u} [CommRing K] [IsDomain K] {p : RatFunc K} : p ≠ 0 → p * p⁻¹ = 1

theorem RatFunc.smul_def {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] : ∀ (x : R) (x_1 : RatFunc K), RatFunc.smul x x_1 = match x, x_1 with | r, { toFractionRing := p } => { toFractionRing := r • p }

@[irreducible]

def RatFunc.smul {K : Type u_2} [CommRing K] {R : Type u_3} [SMul R (FractionRing (Polynomial K))] : R → RatFunc K → RatFunc K

Scalar multiplication of rational functions.

Equations

• @RatFunc.smul = RatFunc.wrapped✝.1

instance RatFunc.instSMulRatFunc {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] : SMul R (RatFunc K)

Equations

• RatFunc.instSMulRatFunc = { smul := RatFunc.smul }

theorem RatFunc.ofFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : FractionRing (Polynomial K)) : { toFractionRing := c • p } = c • { toFractionRing := p }

theorem RatFunc.toFractionRing_smul {K : Type u} [CommRing K] {R : Type u_1} [SMul R (FractionRing (Polynomial K))] (c : R) (p : RatFunc K) : (c • p).toFractionRing = c • p.toFractionRing

theorem RatFunc.smul_eq_C_smul {K : Type u} [CommRing K] (x : RatFunc K) (r : K) : r • x = Polynomial.C r • x

theorem RatFunc.mk_smul {K : Type u} [CommRing K] {R : Type u_1} [IsDomain K] [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : Polynomial K) (q : Polynomial K) : RatFunc.mk (c • p) q = c • RatFunc.mk p q

instance RatFunc.instIsScalarTowerPolynomialToSemiringToCommSemiringRatFuncToSMulZeroToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddGroupWithOneRingToRingToDistribSMulInstSMulRatFuncInstSMulLocalizationToCommMonoidCommRingNonZeroDivisorsToMonoidWithZeroToSMulCommSemiringSemiringIdRightInstSMulRatFuncInstSMulLocalization {K : Type u} [CommRing K] {R : Type u_1} [IsDomain K] [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] : IsScalarTower R (Polynomial K) (RatFunc K)

Equations

• (_ : IsScalarTower R (Polynomial K) (RatFunc K)) = (_ : IsScalarTower R (Polynomial K) (RatFunc K))

instance RatFunc.instSubsingletonRatFunc (K : Type u) [CommRing K] [Subsingleton K] : Subsingleton (RatFunc K)

Equations

• (_ : Subsingleton (RatFunc K)) = (_ : Subsingleton (RatFunc K))

instance RatFunc.instInhabitedRatFunc (K : Type u) [CommRing K] : Inhabited (RatFunc K)

Equations

• RatFunc.instInhabitedRatFunc K = { default := 0 }

instance RatFunc.instNontrivial (K : Type u) [CommRing K] [Nontrivial K] : Nontrivial (RatFunc K)

Equations

• (_ : Nontrivial (RatFunc K)) = (_ : Nontrivial (RatFunc K))

@[simp]

theorem RatFunc.toFractionRingRingEquiv_apply (K : Type u) [CommRing K] (self : RatFunc K) : (RatFunc.toFractionRingRingEquiv K) self = self.toFractionRing

def RatFunc.toFractionRingRingEquiv (K : Type u) [CommRing K] : RatFunc K ≃+* FractionRing (Polynomial K)

RatFunc K is isomorphic to the field of fractions of K[X], as rings.

This is an auxiliary definition; simp-normal form is IsLocalization.algEquiv.

Equations

• One or more equations did not get rendered due to their size.

def RatFunc.tacticFrac_tac : Lean.ParserDescr

Solve equations for RatFunc K by working in FractionRing K[X].

Equations

• RatFunc.tacticFrac_tac = Lean.ParserDescr.node `RatFunc.tacticFrac_tac 1024 (Lean.ParserDescr.nonReservedSymbol "frac_tac" false)

def RatFunc.tacticSmul_tac : Lean.ParserDescr

Solve equations for RatFunc K by applying RatFunc.induction_on.

Equations

• RatFunc.tacticSmul_tac = Lean.ParserDescr.node `RatFunc.tacticSmul_tac 1024 (Lean.ParserDescr.nonReservedSymbol "smul_tac" false)

def RatFunc.instCommMonoid (K : Type u) [CommRing K] : CommMonoid (RatFunc K)

RatFunc K is a commutative monoid.

This is an intermediate step on the way to the full instance RatFunc.instCommRing.

Equations

• RatFunc.instCommMonoid K = CommMonoid.mk (_ : ∀ (a b : RatFunc K), a * b = b * a)

def RatFunc.instAddCommGroup (K : Type u) [CommRing K] : AddCommGroup (RatFunc K)

RatFunc K is an additive commutative group.

This is an intermediate step on the way to the full instance RatFunc.instCommRing.

Equations

• RatFunc.instAddCommGroup K = AddCommGroup.mk (_ : ∀ (a b : RatFunc K), a + b = b + a)

instance RatFunc.instCommRing (K : Type u) [CommRing K] : CommRing (RatFunc K)

Equations

• RatFunc.instCommRing K = let src := RatFunc.instCommMonoid K; let src_1 := RatFunc.instAddCommGroup K; CommRing.mk (_ : ∀ (a b : RatFunc K), a * b = b * a)

def RatFunc.map {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) : RatFunc R →* RatFunc S

Lift a monoid homomorphism that maps polynomials φ : R[X] →* S[X] to a RatFunc R →* RatFunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.map_apply_ofFractionRing_mk {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) : (RatFunc.map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) { val := φ ↑d, property := (_ : ↑d ∈ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) } }

theorem RatFunc.map_injective {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (hf : Function.Injective ⇑φ) : Function.Injective ⇑(RatFunc.map φ hφ)

def RatFunc.mapRingHom {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) : RatFunc R →+* RatFunc S

Lift a ring homomorphism that maps polynomials φ : R[X] →+* S[X] to a RatFunc R →+* RatFunc S, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.coe_mapRingHom_eq_coe_map {R : Type u_3} {S : Type u_4} {F : Type u_5} [CommRing R] [CommRing S] [FunLike F (Polynomial R) (Polynomial S)] [RingHomClass F (Polynomial R) (Polynomial S)] (φ : F) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) : ⇑(RatFunc.mapRingHom φ hφ) = ⇑(RatFunc.map φ hφ)

def RatFunc.liftMonoidWithZeroHom {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] (φ : Polynomial R →*₀ G₀) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) : RatFunc R →*₀ G₀

Lift a monoid with zero homomorphism R[X] →*₀ G₀ to a RatFunc R →*₀ G₀ on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] (φ : Polynomial R →*₀ G₀) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) : (RatFunc.liftMonoidWithZeroHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d

theorem RatFunc.liftMonoidWithZeroHom_injective {G₀ : Type u_1} {R : Type u_3} [CommGroupWithZero G₀] [CommRing R] [Nontrivial R] (φ : Polynomial R →*₀ G₀) (hφ : Function.Injective ⇑φ) (hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀)) (_ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀))) : Function.Injective ⇑(RatFunc.liftMonoidWithZeroHom φ hφ')

def RatFunc.liftRingHom {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) : RatFunc R →+* L

Lift an injective ring homomorphism R[X] →+* L to a RatFunc R →+* L by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.liftRingHom_apply_ofFractionRing_mk {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial R) (d : ↥(nonZeroDivisors (Polynomial R))) : (RatFunc.liftRingHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d

theorem RatFunc.liftRingHom_injective {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] [Nontrivial R] (φ : Polynomial R →+* L) (hφ : Function.Injective ⇑φ) (hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (_ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L))) : Function.Injective ⇑(RatFunc.liftRingHom φ hφ')

instance RatFunc.instField (K : Type u) [CommRing K] [IsDomain K] : Field (RatFunc K)

Equations

• One or more equations did not get rendered due to their size.

RatFunc as field of fractions of Polynomial

instance RatFunc.instAlgebraRatFuncToSemiringToDivisionSemiringToSemifieldInstField (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] : Algebra R (RatFunc K)

Equations

• One or more equations did not get rendered due to their size.

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

theorem RatFunc.ofFractionRing_algebraMap {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) : { toFractionRing := (algebraMap (Polynomial K) (FractionRing (Polynomial K))) x } = (algebraMap (Polynomial K) (RatFunc K)) x

@[simp]

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

@[simp]

theorem RatFunc.div_smul {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [Monoid R] [DistribMulAction R (Polynomial K)] [IsScalarTower R (Polynomial K) (Polynomial K)] (c : R) (p : Polynomial K) (q : Polynomial K) : (algebraMap (Polynomial K) (RatFunc K)) (c • p) / (algebraMap (Polynomial K) (RatFunc K)) q = c • ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)

theorem RatFunc.algebraMap_apply {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} [CommSemiring R] [Algebra R (Polynomial K)] (x : R) : (algebraMap R (RatFunc K)) x = (algebraMap (Polynomial K) (RatFunc K)) ((algebraMap R (Polynomial K)) x) / (algebraMap (Polynomial K) (RatFunc K)) 1

theorem RatFunc.map_apply_div_ne_zero {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p : Polynomial K) (q : Polynomial K) (hq : q ≠ 0) : (RatFunc.map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)

@[simp]

theorem RatFunc.map_apply_div {K : Type u} [CommRing K] [IsDomain K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidWithZeroHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (p : Polynomial K) (q : Polynomial K) : (RatFunc.map φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (algebraMap (Polynomial R) (RatFunc R)) (φ p) / (algebraMap (Polynomial R) (RatFunc R)) (φ q)

theorem RatFunc.liftMonoidWithZeroHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

@[simp]

theorem RatFunc.liftMonoidWithZeroHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

theorem RatFunc.liftRingHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

@[simp]

theorem RatFunc.liftRingHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

theorem RatFunc.ofFractionRing_comp_algebraMap (K : Type u) [CommRing K] [IsDomain K] : RatFunc.ofFractionRing ∘ ⇑(algebraMap (Polynomial K) (FractionRing (Polynomial K))) = ⇑(algebraMap (Polynomial K) (RatFunc K))

theorem RatFunc.algebraMap_injective (K : Type u) [CommRing K] [IsDomain K] : Function.Injective ⇑(algebraMap (Polynomial K) (RatFunc K))

@[simp]

theorem RatFunc.algebraMap_eq_zero_iff (K : Type u) [CommRing K] [IsDomain K] {x : Polynomial K} : (algebraMap (Polynomial K) (RatFunc K)) x = 0 ↔ x = 0

theorem RatFunc.algebraMap_ne_zero {K : Type u} [CommRing K] [IsDomain K] {x : Polynomial K} (hx : x ≠ 0) : (algebraMap (Polynomial K) (RatFunc K)) x ≠ 0

def RatFunc.mapAlgHom {K : Type u} [CommRing K] [IsDomain K] {R : Type u_2} {S : Type u_3} [CommRing R] [IsDomain R] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : Polynomial K →ₐ[S] Polynomial R) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) : RatFunc K →ₐ[S] RatFunc R

Lift an algebra homomorphism that maps polynomials φ : K[X] →ₐ[S] R[X] to a RatFunc K →ₐ[S] RatFunc R, on the condition that φ maps non zero divisors to non zero divisors, by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.coe_mapAlgHom_eq_coe_map {K : Type u} [CommRing K] [IsDomain K] {R : Type u_2} {S : Type u_3} [CommRing R] [IsDomain R] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S (Polynomial R)] (φ : Polynomial K →ₐ[S] Polynomial R) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) : ⇑(RatFunc.mapAlgHom φ hφ) = ⇑(RatFunc.map φ hφ)

def RatFunc.liftAlgHom {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) : RatFunc K →ₐ[S] L

Lift an injective algebra homomorphism K[X] →ₐ[S] L to a RatFunc K →ₐ[S] L by mapping both the numerator and denominator and quotienting them.

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.liftAlgHom_apply_ofFractionRing_mk {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial K) (d : ↥(nonZeroDivisors (Polynomial K))) : (RatFunc.liftAlgHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d

theorem RatFunc.liftAlgHom_injective {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : Function.Injective ⇑φ) (hφ' : optParam (nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (_ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L))) : Function.Injective ⇑(RatFunc.liftAlgHom φ hφ')

@[simp]

theorem RatFunc.liftAlgHom_apply_div' {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

theorem RatFunc.liftAlgHom_apply_div {K : Type u} [CommRing K] [IsDomain K] {L : Type u_1} {S : Type u_3} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (p : Polynomial K) (q : Polynomial K) : (RatFunc.liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

instance RatFunc.instIsFractionRingPolynomialToSemiringToCommSemiringCommRingRatFuncInstCommRingInstAlgebraRatFuncToSemiringToDivisionSemiringToSemifieldInstFieldId (K : Type u) [CommRing K] [IsDomain K] : IsFractionRing (Polynomial K) (RatFunc K)

RatFunc K is the field of fractions of the polynomials over K.

Equations

• (_ : IsFractionRing (Polynomial K) (RatFunc K)) = (_ : IsLocalization (nonZeroDivisors (Polynomial K)) (RatFunc K))

@[simp]

theorem RatFunc.liftOn_div {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (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 : 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') (_ : ∀ {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.liftOn ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) f H = f p q

@[simp]

theorem RatFunc.liftOn'_div {K : Type u} [CommRing K] [IsDomain K] {P : Sort v} (p : Polynomial K) (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.liftOn' ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) f H = f p q

theorem RatFunc.induction_on {K : Type u} [CommRing K] [IsDomain K] {P : RatFunc K → Prop} (x : RatFunc K) (f : ∀ (p q : Polynomial K), q ≠ 0 → P ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)) : P x

Induction principle for RatFunc K: if f p q : P (p / q) for all p q : K[X], then P holds on all elements of RatFunc K.

See also induction_on', which is a recursion principle defined in terms of RatFunc.mk.

theorem RatFunc.ofFractionRing_mk' {K : Type u} [CommRing K] [IsDomain K] (x : Polynomial K) (y : ↥(nonZeroDivisors (Polynomial K))) : { toFractionRing := IsLocalization.mk' (FractionRing (Polynomial K)) x y } = IsLocalization.mk' (RatFunc K) x y

@[simp]

theorem RatFunc.ofFractionRing_eq {K : Type u} [CommRing K] [IsDomain K] : RatFunc.ofFractionRing = ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K))

@[simp]

theorem RatFunc.toFractionRing_eq {K : Type u} [CommRing K] [IsDomain K] : RatFunc.toFractionRing = ⇑(IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (RatFunc K) (FractionRing (Polynomial K)))

@[simp]

theorem RatFunc.toFractionRingRingEquiv_symm_eq {K : Type u} [CommRing K] [IsDomain K] : RingEquiv.symm (RatFunc.toFractionRingRingEquiv K) = AlgEquiv.toRingEquiv (IsLocalization.algEquiv (nonZeroDivisors (Polynomial K)) (FractionRing (Polynomial K)) (RatFunc K))

Numerator and denominator

def RatFunc.numDenom {K : Type u} [Field K] (x : RatFunc K) : Polynomial K × Polynomial K

RatFunc.numDenom are numerator and denominator of a rational function over a field, normalized such that the denominator is monic.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RatFunc.numDenom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : RatFunc.numDenom ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = (Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q), Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q))

def RatFunc.num {K : Type u} [Field K] (x : RatFunc K) : Polynomial K

RatFunc.num is the numerator of a rational function, normalized such that the denominator is monic.

Equations

• RatFunc.num x = (RatFunc.numDenom x).1

@[simp]

theorem RatFunc.num_zero {K : Type u} [Field K] : RatFunc.num 0 = 0

@[simp]

theorem RatFunc.num_div {K : Type u} [Field K] (p : Polynomial K) (q : Polynomial K) : RatFunc.num ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q)

@[simp]

theorem RatFunc.num_one {K : Type u} [Field K] : RatFunc.num 1 = 1

@[simp]

theorem RatFunc.num_algebraMap {K : Type u} [Field K] (p : Polynomial K) : RatFunc.num ((algebraMap (Polynomial K) (RatFunc K)) p) = p

theorem RatFunc.num_div_dvd {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : RatFunc.num ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) ∣ p

@[simp]

theorem RatFunc.num_div_dvd' {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (p / gcd p q) ∣ p

A version of num_div_dvd with the LHS in simp normal form

def RatFunc.denom {K : Type u} [Field K] (x : RatFunc K) : Polynomial K

RatFunc.denom is the denominator of a rational function, normalized such that it is monic.

Equations

• RatFunc.denom x = (RatFunc.numDenom x).2

@[simp]

theorem RatFunc.denom_div {K : Type u} [Field K] (p : Polynomial K) {q : Polynomial K} (hq : q ≠ 0) : RatFunc.denom ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = Polynomial.C (Polynomial.leadingCoeff (q / gcd p q))⁻¹ * (q / gcd p q)

theorem RatFunc.monic_denom {K : Type u} [Field K] (x : RatFunc K) : Polynomial.Monic (RatFunc.denom x)

theorem RatFunc.denom_ne_zero {K : Type u} [Field K] (x : RatFunc K) : RatFunc.denom x ≠ 0

@[simp]

theorem RatFunc.denom_zero {K : Type u} [Field K] : RatFunc.denom 0 = 1

@[simp]

theorem RatFunc.denom_one {K : Type u} [Field K] : RatFunc.denom 1 = 1

@[simp]

theorem RatFunc.denom_algebraMap {K : Type u} [Field K] (p : Polynomial K) : RatFunc.denom ((algebraMap (Polynomial K) (RatFunc K)) p) = 1

@[simp]

theorem RatFunc.denom_div_dvd {K : Type u} [Field K] (p : Polynomial K) (q : Polynomial K) : RatFunc.denom ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) ∣ q

@[simp]

theorem RatFunc.num_div_denom {K : Type u} [Field K] (x : RatFunc K) : (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.num x) / (algebraMap (Polynomial K) (RatFunc K)) (RatFunc.denom x) = x

theorem RatFunc.isCoprime_num_denom {K : Type u} [Field K] (x : RatFunc K) : IsCoprime (RatFunc.num x) (RatFunc.denom x)

@[simp]

theorem RatFunc.num_eq_zero_iff {K : Type u} [Field K] {x : RatFunc K} : RatFunc.num x = 0 ↔ x = 0

theorem RatFunc.num_ne_zero {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) : RatFunc.num x ≠ 0

theorem RatFunc.num_mul_eq_mul_denom_iff {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} {q : Polynomial K} (hq : q ≠ 0) : RatFunc.num x * q = p * RatFunc.denom x ↔ x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q

theorem RatFunc.num_denom_add {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) : RatFunc.num (x + y) * (RatFunc.denom x * RatFunc.denom y) = (RatFunc.num x * RatFunc.denom y + RatFunc.denom x * RatFunc.num y) * RatFunc.denom (x + y)

theorem RatFunc.num_denom_neg {K : Type u} [Field K] (x : RatFunc K) : RatFunc.num (-x) * RatFunc.denom x = -RatFunc.num x * RatFunc.denom (-x)

theorem RatFunc.num_denom_mul {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) : RatFunc.num (x * y) * (RatFunc.denom x * RatFunc.denom y) = RatFunc.num x * RatFunc.num y * RatFunc.denom (x * y)

theorem RatFunc.num_dvd {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} (hp : p ≠ 0) : RatFunc.num x ∣ p ↔ ∃ (q : Polynomial K), q ≠ 0 ∧ x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q

theorem RatFunc.denom_dvd {K : Type u} [Field K] {x : RatFunc K} {q : Polynomial K} (hq : q ≠ 0) : RatFunc.denom x ∣ q ↔ ∃ (p : Polynomial K), x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q

theorem RatFunc.num_mul_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) : RatFunc.num (x * y) ∣ RatFunc.num x * RatFunc.num y

theorem RatFunc.denom_mul_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) : RatFunc.denom (x * y) ∣ RatFunc.denom x * RatFunc.denom y

theorem RatFunc.denom_add_dvd {K : Type u} [Field K] (x : RatFunc K) (y : RatFunc K) : RatFunc.denom (x + y) ∣ RatFunc.denom x * RatFunc.denom y

theorem RatFunc.map_denom_ne_zero {K : Type u} [Field K] {L : Type u_1} {F : Type u_2} [Zero L] [FunLike F (Polynomial K) L] [ZeroHomClass F (Polynomial K) L] (φ : F) (hφ : Function.Injective ⇑φ) (f : RatFunc K) : φ (RatFunc.denom f) ≠ 0

theorem RatFunc.map_apply {K : Type u} [Field K] {R : Type u_1} {F : Type u_2} [CommRing R] [IsDomain R] [FunLike F (Polynomial K) (Polynomial R)] [MonoidHomClass F (Polynomial K) (Polynomial R)] (φ : F) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial R))) (f : RatFunc K) : (RatFunc.map φ hφ) f = (algebraMap (Polynomial R) (RatFunc R)) (φ (RatFunc.num f)) / (algebraMap (Polynomial R) (RatFunc R)) (φ (RatFunc.denom f))

theorem RatFunc.liftMonoidWithZeroHom_apply {K : Type u} [Field K] {L : Type u_1} [CommGroupWithZero L] (φ : Polynomial K →*₀ L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) : (RatFunc.liftMonoidWithZeroHom φ hφ) f = φ (RatFunc.num f) / φ (RatFunc.denom f)

theorem RatFunc.liftRingHom_apply {K : Type u} [Field K] {L : Type u_1} [Field L] (φ : Polynomial K →+* L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) : (RatFunc.liftRingHom φ hφ) f = φ (RatFunc.num f) / φ (RatFunc.denom f)

theorem RatFunc.liftAlgHom_apply {K : Type u} [Field K] {L : Type u_1} {S : Type u_2} [Field L] [CommSemiring S] [Algebra S (Polynomial K)] [Algebra S L] (φ : Polynomial K →ₐ[S] L) (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (f : RatFunc K) : (RatFunc.liftAlgHom φ hφ) f = φ (RatFunc.num f) / φ (RatFunc.denom f)

theorem RatFunc.num_mul_denom_add_denom_mul_num_ne_zero {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hxy : x + y ≠ 0) : RatFunc.num x * RatFunc.denom y + RatFunc.denom x * RatFunc.num y ≠ 0

Polynomial structure: C, X, eval

def RatFunc.C {K : Type u} [CommRing K] [IsDomain K] : K →+* RatFunc K

RatFunc.C a is the constant rational function a.

Equations

• RatFunc.C = algebraMap K (RatFunc K)

@[simp]

theorem RatFunc.algebraMap_eq_C {K : Type u} [CommRing K] [IsDomain K] : algebraMap K (RatFunc K) = RatFunc.C

@[simp]

theorem RatFunc.algebraMap_C {K : Type u} [CommRing K] [IsDomain K] (a : K) : (algebraMap (Polynomial K) (RatFunc K)) (Polynomial.C a) = RatFunc.C a

@[simp]

theorem RatFunc.algebraMap_comp_C {K : Type u} [CommRing K] [IsDomain K] : RingHom.comp (algebraMap (Polynomial K) (RatFunc K)) Polynomial.C = RatFunc.C

theorem RatFunc.smul_eq_C_mul {K : Type u} [CommRing K] [IsDomain K] (r : K) (x : RatFunc K) : r • x = RatFunc.C r * x

def RatFunc.X {K : Type u} [CommRing K] [IsDomain K] : RatFunc K

RatFunc.X is the polynomial variable (aka indeterminate).

Equations

• RatFunc.X = (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X

@[simp]

theorem RatFunc.algebraMap_X {K : Type u} [CommRing K] [IsDomain K] : (algebraMap (Polynomial K) (RatFunc K)) Polynomial.X = RatFunc.X

@[simp]

theorem RatFunc.num_C {K : Type u} [Field K] (c : K) : RatFunc.num (RatFunc.C c) = Polynomial.C c

@[simp]

theorem RatFunc.denom_C {K : Type u} [Field K] (c : K) : RatFunc.denom (RatFunc.C c) = 1

@[simp]

theorem RatFunc.num_X {K : Type u} [Field K] : RatFunc.num RatFunc.X = Polynomial.X

@[simp]

theorem RatFunc.denom_X {K : Type u} [Field K] : RatFunc.denom RatFunc.X = 1

theorem RatFunc.X_ne_zero {K : Type u} [Field K] : RatFunc.X ≠ 0

def RatFunc.eval {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) (p : RatFunc K) : L

Evaluate a rational function p given a ring hom f from the scalar field to the target and a value x for the variable in the target.

Fractions are reduced by clearing common denominators before evaluating: eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2, not 0 / 0 = 0.

Equations

• RatFunc.eval f a p = Polynomial.eval₂ f a (RatFunc.num p) / Polynomial.eval₂ f a (RatFunc.denom p)

theorem RatFunc.eval_eq_zero_of_eval₂_denom_eq_zero {K : Type u} [Field K] {L : Type u_1} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : Polynomial.eval₂ f a (RatFunc.denom x) = 0) : RatFunc.eval f a x = 0

theorem RatFunc.eval₂_denom_ne_zero {K : Type u} [Field K] {L : Type u_1} [Field L] {f : K →+* L} {a : L} {x : RatFunc K} (h : RatFunc.eval f a x ≠ 0) : Polynomial.eval₂ f a (RatFunc.denom x) ≠ 0

@[simp]

theorem RatFunc.eval_C {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) {c : K} : RatFunc.eval f a (RatFunc.C c) = f c

@[simp]

theorem RatFunc.eval_X {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) : RatFunc.eval f a RatFunc.X = a

@[simp]

theorem RatFunc.eval_zero {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) : RatFunc.eval f a 0 = 0

@[simp]

theorem RatFunc.eval_one {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) : RatFunc.eval f a 1 = 1

@[simp]

theorem RatFunc.eval_algebraMap {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) {S : Type u_2} [CommSemiring S] [Algebra S (Polynomial K)] (p : S) : RatFunc.eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)

theorem RatFunc.eval_add {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a (RatFunc.denom x) ≠ 0) (hy : Polynomial.eval₂ f a (RatFunc.denom y) ≠ 0) : RatFunc.eval f a (x + y) = RatFunc.eval f a x + RatFunc.eval f a y

eval is an additive homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0 ... ≠ 1 = eval _ 1 ((X-1) / (X-1)).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

theorem RatFunc.eval_mul {K : Type u} [Field K] {L : Type u_1} [Field L] (f : K →+* L) (a : L) {x : RatFunc K} {y : RatFunc K} (hx : Polynomial.eval₂ f a (RatFunc.denom x) ≠ 0) (hy : Polynomial.eval₂ f a (RatFunc.denom y) ≠ 0) : RatFunc.eval f a (x * y) = RatFunc.eval f a x * RatFunc.eval f a y

eval is a multiplicative homomorphism except when a denominator evaluates to 0.

Counterexample: eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X).

See also RatFunc.eval₂_denom_ne_zero to make the hypotheses simpler but less general.

def RatFunc.intDegree {K : Type u} [Field K] (x : RatFunc K) : ℤ

intDegree x is the degree of the rational function x, defined as the difference between the natDegree of its numerator and the natDegree of its denominator. In particular, intDegree 0 = 0.

Equations

• RatFunc.intDegree x = ↑(Polynomial.natDegree (RatFunc.num x)) - ↑(Polynomial.natDegree (RatFunc.denom x))

@[simp]

theorem RatFunc.intDegree_zero {K : Type u} [Field K] : RatFunc.intDegree 0 = 0

@[simp]

theorem RatFunc.intDegree_one {K : Type u} [Field K] : RatFunc.intDegree 1 = 0

@[simp]

theorem RatFunc.intDegree_C {K : Type u} [Field K] (k : K) : RatFunc.intDegree (RatFunc.C k) = 0

@[simp]

theorem RatFunc.intDegree_X {K : Type u} [Field K] : RatFunc.intDegree RatFunc.X = 1

@[simp]

theorem RatFunc.intDegree_polynomial {K : Type u} [Field K] {p : Polynomial K} : RatFunc.intDegree ((algebraMap (Polynomial K) (RatFunc K)) p) = ↑(Polynomial.natDegree p)

theorem RatFunc.intDegree_mul {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) : RatFunc.intDegree (x * y) = RatFunc.intDegree x + RatFunc.intDegree y

@[simp]

theorem RatFunc.intDegree_neg {K : Type u} [Field K] (x : RatFunc K) : RatFunc.intDegree (-x) = RatFunc.intDegree x

theorem RatFunc.intDegree_add {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hxy : x + y ≠ 0) : RatFunc.intDegree (x + y) = ↑(Polynomial.natDegree (RatFunc.num x * RatFunc.denom y + RatFunc.denom x * RatFunc.num y)) - ↑(Polynomial.natDegree (RatFunc.denom x * RatFunc.denom y))

theorem RatFunc.natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) {s : Polynomial K} (hs : s ≠ 0) : ↑(Polynomial.natDegree (RatFunc.num x * s)) - ↑(Polynomial.natDegree (s * RatFunc.denom x)) = RatFunc.intDegree x

theorem RatFunc.intDegree_add_le {K : Type u} [Field K] {x : RatFunc K} {y : RatFunc K} (hy : y ≠ 0) (hxy : x + y ≠ 0) : RatFunc.intDegree (x + y) ≤ max (RatFunc.intDegree x) (RatFunc.intDegree y)

def RatFunc.coeAlgHom (F : Type u) [Field F] : RatFunc F →ₐ[Polynomial F] LaurentSeries F

The coercion RatFunc F → LaurentSeries F as bundled alg hom.

Equations

• One or more equations did not get rendered due to their size.

def RatFunc.coeToLaurentSeries_fun {F : Type u} [Field F] : RatFunc F → LaurentSeries F

The coercion RatFunc F → LaurentSeries F as a function.

This is the implementation of coeToLaurentSeries.

Equations

• RatFunc.coeToLaurentSeries_fun = ⇑(RatFunc.coeAlgHom F)

instance RatFunc.coeToLaurentSeries {F : Type u} [Field F] : Coe (RatFunc F) (LaurentSeries F)

Equations

• RatFunc.coeToLaurentSeries = { coe := RatFunc.coeToLaurentSeries_fun }

theorem RatFunc.coe_def {F : Type u} [Field F] (f : RatFunc F) : ↑f = (RatFunc.coeAlgHom F) f

theorem RatFunc.coe_num_denom {F : Type u} [Field F] (f : RatFunc F) : ↑f = (HahnSeries.ofPowerSeries ℤ F) ↑(RatFunc.num f) / (HahnSeries.ofPowerSeries ℤ F) ↑(RatFunc.denom f)

theorem RatFunc.coe_injective {F : Type u} [Field F] : Function.Injective RatFunc.coeToLaurentSeries_fun

@[simp]

theorem RatFunc.coe_apply {F : Type u} [Field F] (f : RatFunc F) : (RatFunc.coeAlgHom F) f = ↑f

@[simp]

theorem RatFunc.coe_zero {F : Type u} [Field F] : ↑0 = 0

@[simp]

theorem RatFunc.coe_one {F : Type u} [Field F] : ↑1 = 1

@[simp]

theorem RatFunc.coe_add {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f + g) = ↑f + ↑g

@[simp]

theorem RatFunc.coe_sub {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f - g) = ↑f - ↑g

@[simp]

theorem RatFunc.coe_neg {F : Type u} [Field F] (f : RatFunc F) : ↑(-f) = -↑f

@[simp]

theorem RatFunc.coe_mul {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f * g) = ↑f * ↑g

@[simp]

theorem RatFunc.coe_pow {F : Type u} [Field F] (f : RatFunc F) (n : ℕ) : ↑(f ^ n) = ↑f ^ n

@[simp]

theorem RatFunc.coe_div {F : Type u} [Field F] (f : RatFunc F) (g : RatFunc F) : ↑(f / g) = ↑f / ↑g

@[simp]

theorem RatFunc.coe_C {F : Type u} [Field F] (r : F) : ↑(RatFunc.C r) = HahnSeries.C r

@[simp]

theorem RatFunc.coe_smul {F : Type u} [Field F] (f : RatFunc F) (r : F) : ↑(r • f) = r • ↑f

@[simp]

theorem RatFunc.coe_X {F : Type u} [Field F] : ↑RatFunc.X = (HahnSeries.single 1) 1

instance RatFunc.instAlgebraRatFuncToCommRingLaurentSeriesToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToCommSemiringInstFieldIsDomainInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiringToDivisionSemiring {F : Type u} [Field F] : Algebra (RatFunc F) (LaurentSeries F)

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.algebraMap_apply_div {F : Type u} [Field F] (p : Polynomial F) (q : Polynomial F) : (algebraMap (RatFunc F) (LaurentSeries F)) ((algebraMap (Polynomial F) (RatFunc F)) p / (algebraMap (Polynomial F) (RatFunc F)) q) = (algebraMap (Polynomial F) (LaurentSeries F)) p / (algebraMap (Polynomial F) (LaurentSeries F)) q

instance RatFunc.instIsScalarTowerPolynomialToSemiringToDivisionSemiringToSemifieldRatFuncToCommRingLaurentSeriesToZeroToCommMonoidWithZeroToCommGroupWithZeroInstSMulRatFuncInstSMulLocalizationToSemiringToCommSemiringToCommMonoidCommRingNonZeroDivisorsToMonoidWithZeroToSMulCommSemiringToCommSemiringSemiringIdRightInstFieldIsDomainInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingInstAlgebraRatFuncToCommRingLaurentSeriesToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToCommSemiringInstFieldIsDomainInstSemiringHahnSeriesToPartialOrderToOrderedAddCommMonoidToZeroToMonoidWithZeroIntToOrderedCancelAddCommMonoidToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringLinearOrderedCommRingToSemiringToDivisionSemiringPowerSeriesAlgebraAlgebraPolynomial {F : Type u} [Field F] : IsScalarTower (Polynomial F) (RatFunc F) (LaurentSeries F)

Equations

• (_ : IsScalarTower (Polynomial F) (RatFunc F) (LaurentSeries F)) = (_ : IsScalarTower (Polynomial F) (RatFunc F) (LaurentSeries F))