Theory of univariate polynomials #
We show that A[X]
is an R-algebra when A
is an R-algebra.
We promote eval₂
to an algebra hom in aeval
.
Note that this instance also provides Algebra R R[X]
.
Equations
- Polynomial.algebraOfAlgebra = Algebra.mk (Polynomial.C.comp (algebraMap R A)) ⋯ ⋯
When we have [CommSemiring R]
, the function C
is the same as algebraMap R R[X]
.
(But note that C
is defined when R
is not necessarily commutative, in which case
algebraMap
is not available.)
Polynomial.C
as an AlgHom
.
Equations
- Polynomial.CAlgHom = { toRingHom := Polynomial.C, commutes' := ⋯ }
Instances For
Extensionality lemma for algebra maps out of A'[X]
over a smaller base ring than A'
Algebra isomorphism between R[X]
and R[ℕ]
. This is just an
implementation detail, but it can be useful to transfer results from Finsupp
to polynomials.
Equations
- Polynomial.toFinsuppIsoAlg R = { toEquiv := (Polynomial.toFinsuppIso R).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Alias of Polynomial.ringHom_eval₂_intCastRingHom
.
Alias of Polynomial.eval₂_intCastRingHom_X
.
Polynomial.eval₂
as an AlgHom
for noncommutative algebras.
This is Polynomial.eval₂RingHom'
for AlgHom
s.
Equations
- Polynomial.eval₂AlgHom' f b hf = { toRingHom := Polynomial.eval₂RingHom' (↑f) b hf, commutes' := ⋯ }
Instances For
Polynomial.map
as an AlgHom
for noncommutative algebras.
This is the algebra version of Polynomial.mapRingHom
.
Equations
- Polynomial.mapAlgHom f = { toRingHom := Polynomial.mapRingHom f.toRingHom, commutes' := ⋯ }
Instances For
If A
and B
are isomorphic as R
-algebras, then so are their polynomial rings
Equations
- Polynomial.mapAlgEquiv f = AlgEquiv.ofAlgHom (Polynomial.mapAlgHom ↑f) (Polynomial.mapAlgHom ↑f.symm) ⋯ ⋯
Instances For
Given a valuation x
of the variable in an R
-algebra A
, aeval R A x
is
the unique R
-algebra homomorphism from R[X]
to A
sending X
to x
.
This is a stronger variant of the linear map Polynomial.leval
.
Equations
- Polynomial.aeval x = Polynomial.eval₂AlgHom' (Algebra.ofId R A) x ⋯
Instances For
Alias of Polynomial.aeval_natCast
.
Two polynomials p
and q
such that p(q(X))=X
and q(p(X))=X
induces an automorphism of the polynomial algebra.
Equations
- p.algEquivOfCompEqX q hpq hqp = AlgEquiv.ofAlgHom (Polynomial.aeval p) (Polynomial.aeval q) ⋯ ⋯
Instances For
The automorphism of the polynomial algebra given by p(X) ↦ p(X+t)
,
with inverse p(X) ↦ p(X-t)
.
Equations
- Polynomial.algEquivAevalXAddC t = (Polynomial.X + Polynomial.C t).algEquivOfCompEqX (Polynomial.X - Polynomial.C t) ⋯ ⋯
Instances For
Equations
Equations
Version of aeval
for defining algebra homs out of R[X]
over a smaller base ring
than R
.
Equations
- Polynomial.aevalTower f x = Polynomial.eval₂AlgHom' f x ⋯
Instances For
The evaluation map is not generally multiplicative when the coefficient ring is noncommutative,
but nevertheless any polynomial of the form p * (X - monomial 0 r)
is sent to zero
when evaluated at r
.
This is the key step in our proof of the Cayley-Hamilton theorem.