The field structure of rational functions

Main definitions

Working with rational functions as polynomials:

• RatFunc.instField provides a field structure You can use IsFractionRing API to treat RatFunc as the field of fractions of polynomials:

• algebraMap K[X] K⟮X⟯ maps polynomials to rational functions
• IsFractionRing.algEquiv maps other fields of fractions of K[X] to K⟮X⟯.

In particular:

• FractionRing.algEquiv K[X] K⟮X⟯ maps the generic field of fraction construction to K⟮X⟯. Combine this with AlgEquiv.restrictScalars to change the FractionRing K[X] ≃ₐ[K[X]] K⟮X⟯ to FractionRing K[X] ≃ₐ[K] K⟮X⟯.

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.

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 K⟮X⟯ →*₀ G₀, where [CommRing K] [CommGroupWithZero G₀]
• RatFunc.liftRingHom lifts a K[X] →+* L to a K⟮X⟯ →+* L, where [CommRing K] [Field L]
• RatFunc.liftAlgHom lifts a K[X] →ₐ[S] L to a K⟮X⟯ →ₐ[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]

@[irreducible]

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

The zero rational function.

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

@[implicit_reducible]

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

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

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

@[irreducible]

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

Addition of rational functions.

@[implicit_reducible]

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

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

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

@[irreducible]

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

Subtraction of rational functions.

@[implicit_reducible]

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

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

@[irreducible]

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

Additive inverse of a rational function.

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

@[implicit_reducible]

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

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

@[irreducible]

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

The multiplicative unit of rational functions.

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

@[implicit_reducible]

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

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

@[irreducible]

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

Multiplication of rational functions.

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

@[implicit_reducible]

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

theorem RatFunc.ofFractionRing_mul {K : Type u} [CommRing K] (p 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✝¹ : RatFunc K) : x✝.div x✝¹ = match x✝, x✝¹ with | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }

@[irreducible]

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

Division of rational functions.

@[implicit_reducible]

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

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

@[irreducible]

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

Multiplicative inverse of a rational function.

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

@[implicit_reducible]

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

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

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

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

@[implicit_reducible]

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

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 q : Polynomial K) : RatFunc.mk (c • p) q = c • RatFunc.mk p q

instance RatFunc.instIsScalarTowerPolynomial {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)

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

@[implicit_reducible]

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

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

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

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

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

@[simp]

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

def RatFunc.tacticFrac_tac : Lean.ParserDescr

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

def RatFunc.tacticSmul_tac : Lean.ParserDescr

Solve equations for K⟮X⟯ by applying RatFunc.induction_on.

@[implicit_reducible]

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

K⟮X⟯ is a commutative monoid.

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

@[implicit_reducible]

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

K⟮X⟯ is an additive commutative group.

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

@[implicit_reducible]

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

noncomputable 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 R⟮X⟯ →* S⟮X⟯, on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

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))) : (map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }

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 ⇑(map φ hφ)

noncomputable 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 R⟮X⟯ →+* S⟮X⟯, on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

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))) : ⇑(mapRingHom φ hφ) = ⇑(map φ hφ)

noncomputable 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 R⟮X⟯ →*₀ G₀ on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

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))) : (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φ' : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀) := ⋯) : Function.Injective ⇑(liftMonoidWithZeroHom φ hφ')

noncomputable 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 R⟮X⟯ →+* L by mapping both the numerator and denominator and quotienting them.

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))) : (liftRingHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d

@[simp]

theorem RatFunc.liftRingHom_ofFractionRing_algebraMap {L : Type u_2} {R : Type u_3} [Field L] [CommRing R] (φ : Polynomial R →+* L) (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : Polynomial R) : (liftRingHom φ hφ) { toFractionRing := (algebraMap (Polynomial R) (FractionRing (Polynomial R))) x } = φ x

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φ' : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L) := ⋯) : Function.Injective ⇑(liftRingHom φ hφ')

@[implicit_reducible]

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

Stacks Tag 09FK

RatFunc as field of fractions of Polynomial

@[implicit_reducible]

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

noncomputable def RatFunc.coePolynomial {K : Type u} [CommRing K] [IsDomain K] (P : Polynomial K) : RatFunc K

The coercion from polynomials to rational functions, implemented as the algebra map from a domain to its field of fractions

@[implicit_reducible]

noncomputable instance RatFunc.instCoePolynomial {K : Type u} [CommRing K] [IsDomain K] : Coe (Polynomial K) (RatFunc K)

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

def RatFunc.toFractionRingAlgEquiv (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] : RatFunc K ≃ₐ[R] FractionRing (Polynomial K)

The equivalence between K⟮X⟯ and the field of fractions of K[X]

@[simp]

theorem RatFunc.toFractionRingAlgEquiv_apply (K : Type u) [CommRing K] [IsDomain K] (R : Type u_1) [CommSemiring R] [Algebra R (Polynomial K)] (self : RatFunc K) : (toFractionRingAlgEquiv K R) self = self.toFractionRing

@[simp]

theorem RatFunc.mk_eq_div {K : Type u} [CommRing K] [IsDomain K] (p 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 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 q : Polynomial K) (hq : q ≠ 0) : (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 q : Polynomial K) : (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 q : Polynomial K) : (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 q : Polynomial K) : (liftMonoidWithZeroHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (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 q : Polynomial K) : (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (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 q : Polynomial K) : (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

@[simp]

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

@[simp]

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

theorem RatFunc.ofFractionRing_comp_algebraMap (K : Type u) [CommRing K] [IsDomain K] : 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))

noncomputable 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 K⟮X⟯ →ₐ[S] R⟮X⟯, on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

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))) : ⇑(mapAlgHom φ hφ) = ⇑(map φ hφ)

noncomputable 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 K⟮X⟯ →ₐ[S] L by mapping both the numerator and denominator and quotienting them.

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))) : (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φ' : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L) := ⋯) : Function.Injective ⇑(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 q : Polynomial K) : (liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (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 q : Polynomial K) : (liftAlgHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

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

K⟮X⟯ is the field of fractions of the polynomials over K.

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

@[simp]

theorem RatFunc.liftOn_div {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' := ⋯) : ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn f H = f p q

@[simp]

theorem RatFunc.liftOn'_div {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) : ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) 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) (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 K⟮X⟯: if f p q : P (p / q) for all p q : K[X], then P holds on all elements of K⟮X⟯.

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

theorem RatFunc.mk_eq_mk' {K : Type u} [CommRing K] [IsDomain K] (f : Polynomial K) {g : Polynomial K} (hg : g ≠ 0) : RatFunc.mk f g = IsLocalization.mk' (RatFunc K) f ⟨g, ⋯⟩

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

noncomputable def RatFunc.liftAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [Field L] [IsDomain R] [Algebra (Polynomial R) L] [FaithfulSMul (Polynomial R) L] : Algebra (RatFunc R) L

FractionRing.liftAlgebra specialized to R⟮X⟯.

This is a scoped instance because it creates a diamond when L = R⟮X⟯.

instance RatFunc.isScalarTower_liftAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [Field L] [IsDomain R] [Algebra (Polynomial R) L] [FaithfulSMul (Polynomial R) L] : IsScalarTower (Polynomial R) (RatFunc R) L

FractionRing.isScalarTower_liftAlgebra specialized to R⟮X⟯.

instance RatFunc.faithfulSMul (K : Type u_3) (E : Type u_4) [Field K] [Field E] [Algebra K E] [FaithfulSMul K E] : FaithfulSMul (Polynomial K) (RatFunc E)

FractionRing.instFaithfulSMul specialized to R⟮X⟯.

theorem RatFunc.rank_ratFunc_ratFunc (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] : Module.rank (RatFunc k) (RatFunc K) = Module.rank k K

theorem RatFunc.finrank_ratFunc_ratFunc (k : Type u_3) (K : Type u_4) [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] : Module.finrank (RatFunc k) (RatFunc K) = Module.finrank k K

instance RatFunc.instIsScalarTowerOfIsDomainOfPolynomial (R₀ : Type u_1) (R : Type u_2) (A : Type u_3) [CommSemiring R₀] [CommSemiring R] [CommRing A] [IsDomain A] [Algebra R₀ (Polynomial A)] [SMul R₀ R] [Algebra R (Polynomial A)] [IsScalarTower R₀ R (Polynomial A)] : IsScalarTower R₀ R (RatFunc A)

Let A⟮X⟯ / A[X] / R / R₀ be a tower. If A[X] / R / R₀ is a scalar tower then so is A⟮X⟯ / R / R₀.

instance RatFunc.instIsScalarTowerOfPolynomial (R : Type u_1) (A : Type u_2) (K : Type u_3) [CommRing A] [IsDomain A] [Field K] [Algebra (Polynomial A) K] [FaithfulSMul (Polynomial A) K] [CommSemiring R] [Algebra R (Polynomial A)] [SMul R K] [IsScalarTower R (Polynomial A) K] : IsScalarTower R (RatFunc A) K

Let K / A⟮X⟯ / A[X] / R be a tower. If K / A[X] / R is a scalar tower then so is K / A⟮X⟯ / R.

instance RatFunc.instIsScalarTowerOfPolynomial_1 (A : Type u_1) (k : Type u_2) (K : Type u_3) [CommRing A] [IsDomain A] [Field k] [Field K] [Algebra (Polynomial A) k] [Algebra (Polynomial A) K] [SMul k K] [FaithfulSMul (Polynomial A) k] [FaithfulSMul (Polynomial A) K] [IsScalarTower (Polynomial A) k K] : IsScalarTower (RatFunc A) k K

Let K / k / A⟮X⟯ / A[X] be a tower. If K / k / A[X] is a scalar tower then so is K / k / A⟮X⟯.

Numerator and denominator

noncomputable 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.

@[simp]

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

noncomputable 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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

A version of num_div_dvd with the LHS in simp normal form

noncomputable 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.

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

theorem RatFunc.num_dvd {K : Type u} [Field K] {x : RatFunc K} {p : Polynomial K} (hp : p ≠ 0) : x.num ∣ 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) : x.denom ∣ 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 y : RatFunc K) : (x * y).num ∣ x.num * y.num

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

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

theorem RatFunc.num_inv_dvd {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) : x⁻¹.num ∣ x.denom

theorem RatFunc.denom_inv_dvd {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) : x⁻¹.denom ∣ x.num

theorem RatFunc.associated_num_inv {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) : Associated x⁻¹.num x.denom

theorem RatFunc.associated_denom_inv {K : Type u} [Field K] {x : RatFunc K} (hx : x ≠ 0) : Associated x⁻¹.denom x.num

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) : φ f.denom ≠ 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) : (map φ hφ) f = (algebraMap (Polynomial R) (RatFunc R)) (φ f.num) / (algebraMap (Polynomial R) (RatFunc R)) (φ f.denom)

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) : (liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom

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) : (liftRingHom φ hφ) f = φ f.num / φ f.denom

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) : (liftAlgHom φ hφ) f = φ f.num / φ f.denom

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

instance RatFunc.instCharP {K : Type u} [Field K] {p : ℕ} [CharP K p] : CharP (RatFunc K) p

instance RatFunc.instExpChar {K : Type u} [Field K] {p : ℕ} [ExpChar K p] : ExpChar (RatFunc K) p

instance RatFunc.instCharZero {K : Type u} [Field K] [CharZero K] : CharZero (RatFunc K)