The field structure of rational functions #
Main definitions #
Working with rational functions as polynomials:
RatFunc.instField
provides a field structure You can useIsFractionRing
API to treatRatFunc
as the field of fractions of polynomials:
algebraMap K[X] (RatFunc K)
maps polynomials to rational functionsIsFractionRing.algEquiv
maps other fields of fractions ofK[X]
toRatFunc K
, in particular:FractionRing.algEquiv K[X] (RatFunc K)
maps the generic field of fraction construction toRatFunc K
. Combine this withAlgEquiv.restrictScalars
to change theFractionRing K[X] ≃ₐ[K[X]] RatFunc K
toFractionRing K[X] ≃ₐ[K] RatFunc K
.
Working with rational functions as fractions:
RatFunc.num
andRatFunc.denom
give the numerator and denominator. These values are chosen to be coprime and such thatRatFunc.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 aK[X] →*₀ G₀
to aRatFunc K →*₀ G₀
, where[CommRing K] [CommGroupWithZero G₀]
RatFunc.liftRingHom
lifts aK[X] →+* L
to aRatFunc K →+* L
, where[CommRing K] [Field L]
RatFunc.liftAlgHom
lifts aK[X] →ₐ[S] L
to aRatFunc 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
liftsK[X] →* R[X]
when[CommRing K] [CommRing R]
RatFunc.mapRingHom
liftsK[X] →+* R[X]
when[CommRing K] [CommRing R]
RatFunc.mapAlgHom
liftsK[X] →ₐ[S] R[X]
when[CommRing K] [IsDomain K] [CommRing R] [IsDomain R]
Scalar multiplication of rational functions.
Equations
- RatFunc.smul x✝ x = match x✝, x with | r, { toFractionRing := p } => { toFractionRing := r • p }
Instances For
Equations
- RatFunc.instSMulOfFractionRingPolynomial = { smul := RatFunc.smul }
Equations
- RatFunc.instInhabited K = { default := 0 }
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
- RatFunc.toFractionRingRingEquiv K = { toFun := RatFunc.toFractionRing, invFun := RatFunc.ofFractionRing, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
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)
Instances For
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)
Instances For
RatFunc K
is a commutative monoid.
This is an intermediate step on the way to the full instance RatFunc.instCommRing
.
Equations
Instances For
RatFunc K
is an additive commutative group.
This is an intermediate step on the way to the full instance RatFunc.instCommRing
.
Equations
Instances For
Equations
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.
Instances For
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
- RatFunc.mapRingHom φ hφ = { toMonoidHom := RatFunc.map φ hφ, map_zero' := ⋯, map_add' := ⋯ }
Instances For
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
- RatFunc.liftMonoidWithZeroHom φ hφ = { toFun := fun (f : RatFunc R) => f.liftOn (fun (p q : Polynomial R) => φ p / φ q) ⋯, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Lift an injective ring homomorphism R[X] →+* L
to a RatFunc R →+* L
by mapping both the numerator and denominator and quotienting them.
Equations
- RatFunc.liftRingHom φ hφ = { toFun := (↑(RatFunc.liftMonoidWithZeroHom φ.toMonoidWithZeroHom hφ)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
RatFunc
as field of fractions of Polynomial
#
Equations
- One or more equations did not get rendered due to their size.
The coercion from polynomials to rational functions, implemented as the algebra map from a domain to its field of fractions
Equations
- ↑P = (algebraMap (Polynomial K) (RatFunc K)) P
Instances For
Equations
- RatFunc.instCoePolynomial = { coe := RatFunc.coePolynomial }
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
- RatFunc.mapAlgHom φ hφ = { toRingHom := RatFunc.mapRingHom φ hφ, commutes' := ⋯ }
Instances For
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
- RatFunc.liftAlgHom φ hφ = { toRingHom := RatFunc.liftRingHom φ.toRingHom hφ, commutes' := ⋯ }
Instances For
RatFunc K
is the field of fractions of the polynomials over K
.
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
.
Numerator and denominator #
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.
Instances For
RatFunc.num
is the numerator of a rational function,
normalized such that the denominator is monic.
Equations
- x.num = x.numDenom.1
Instances For
A version of num_div_dvd
with the LHS in simp normal form
RatFunc.denom
is the denominator of a rational function,
normalized such that it is monic.
Equations
- x.denom = x.numDenom.2