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] (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.

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]

@[irreducible]

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 }

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]

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

Addition of rational functions.

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]

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

Subtraction of rational functions.

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]

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 }

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]

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 }

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

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

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 }

@[irreducible]

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

Multiplication of rational functions.

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]

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

Division of rational functions.

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 }

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

@[irreducible]

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

Multiplicative inverse of a rational function.

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

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 }

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

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)

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)

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.

@[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 RatFunc K by working in FractionRing K[X].

def RatFunc.tacticSmul_tac : Lean.ParserDescr

Solve equations for RatFunc K by applying RatFunc.induction_on.

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.

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.

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

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.

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φ)

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.

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φ)

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.

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φ')

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.

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

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φ')

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

Stacks Tag 09FK

RatFunc as field of fractions of Polynomial

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

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

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

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

@[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 q : Polynomial K) : (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) p) / (liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) q) = φ p / φ q

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))

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.

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φ)

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.

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)

RatFunc K 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 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

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

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.

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

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

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