Adjoining roots of polynomials #
This file defines the commutative ring AdjoinRoot f
, the ring R[X]/(f) obtained from a
commutative ring R
and a polynomial f : R[X]
. If furthermore R
is a field and f
is
irreducible, the field structure on AdjoinRoot f
is constructed.
We suggest stating results on IsAdjoinRoot
instead of AdjoinRoot
to achieve higher
generality, since IsAdjoinRoot
works for all different constructions of R[α]
including AdjoinRoot f = R[X]/(f)
itself.
Main definitions and results #
The main definitions are in the AdjoinRoot
namespace.
-
mk f : R[X] →+* AdjoinRoot f
, the natural ring homomorphism. -
of f : R →+* AdjoinRoot f
, the natural ring homomorphism. -
root f : AdjoinRoot f
, the image of X in R[X]/(f). -
lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (AdjoinRoot f) →+* S
, the ring homomorphism from R[X]/(f) to S extendingi : R →+* S
and sendingX
tox
. -
lift_hom (x : S) (hfx : aeval x f = 0) : AdjoinRoot f →ₐ[R] S
, the algebra homomorphism from R[X]/(f) to S extendingalgebraMap R S
and sendingX
tox
-
equiv : (AdjoinRoot f →ₐ[F] E) ≃ {x // x ∈ f.aroots E}
a bijection between algebra homomorphisms fromAdjoinRoot
and roots off
inS
Adjoin a root of a polynomial f
to a commutative ring R
. We define the new ring
as the quotient of R[X]
by the principal ideal generated by f
.
Equations
- AdjoinRoot f = (Polynomial R ⧸ Ideal.span {f})
Instances For
Equations
Equations
- AdjoinRoot.instInhabitedAdjoinRoot f = { default := 0 }
Equations
Ring homomorphism from R[x]
to AdjoinRoot f
sending X
to the root
.
Equations
- AdjoinRoot.mk f = Ideal.Quotient.mk (Ideal.span {f})
Instances For
Embedding of the original ring R
into AdjoinRoot f
.
Equations
- AdjoinRoot.of f = RingHom.comp (AdjoinRoot.mk f) Polynomial.C
Instances For
Equations
Equations
- AdjoinRoot.hasCoeT = { coe := ↑(AdjoinRoot.of f) }
Two R
-AlgHom
from AdjoinRoot f
to the same R
-algebra are the same iff
they agree on root f
.
Lift a ring homomorphism i : R →+* S
to AdjoinRoot f →+* S
.
Equations
- AdjoinRoot.lift i x h = Ideal.Quotient.lift (Ideal.span {f}) (Polynomial.eval₂RingHom i x) (_ : ∀ (g : Polynomial R), g ∈ Ideal.span {f} → ↑(Polynomial.eval₂RingHom i x) g = 0)
Instances For
Produce an algebra homomorphism AdjoinRoot f →ₐ[R] S
sending root f
to
a root of f
in S
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
AdjoinRoot.modByMonicHom
sends the equivalence class of f
mod g
to f %ₘ g
.
This is a well-defined right inverse to AdjoinRoot.mk
, see AdjoinRoot.mk_leftInverse
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The elements 1, root g, ..., root g ^ (d - 1)
form a basis for AdjoinRoot g
,
where g
is a monic polynomial of degree d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The power basis 1, root g, ..., root g ^ (d - 1)
for AdjoinRoot g
,
where g
is a monic polynomial of degree d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The elements 1, root f, ..., root f ^ (d - 1)
form a basis for AdjoinRoot f
,
where f
is an irreducible polynomial over a field of degree d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The power basis 1, root f, ..., root f ^ (d - 1)
for AdjoinRoot f
,
where f
is an irreducible polynomial over a field of degree d
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The surjective algebra morphism R[X]/(minpoly R x) → R[x]
.
If R
is a GCD domain and x
is integral, this is an isomorphism,
see minpoly.equivAdjoin
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If S
is an extension of R
with power basis pb
and g
is a monic polynomial over R
such that pb.gen
has a minimal polynomial g
, then S
is isomorphic to AdjoinRoot g
.
Compare PowerBasis.equivOfRoot
, which would require
h₂ : aeval pb.gen (minpoly R (root g)) = 0
; that minimal polynomial is not
guaranteed to be identical to g
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If L
is a field extension of F
and f
is a polynomial over F
then the set
of maps from F[x]/(f)
into L
is in bijection with the set of roots of f
in L
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f))
for α
a root of
f : R[X]
and I : Ideal R
.
See adjoin_root.quot_map_of_equiv
for the isomorphism with (R/I)[X] / (f mod I)
.
Equations
- AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk I f = Ideal.quotEquivOfEq (_ : Ideal.map (AdjoinRoot.of f) I = Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I))
Instances For
The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])
for α
a root of f : R[X]
and I : Ideal R
Equations
- AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk I f = DoubleQuot.quotQuotEquivComm (Ideal.span {f}) (Ideal.map Polynomial.C I)
Instances For
The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x])
where
f : R[X]
and I : Ideal R
Equations
- One or more equations did not get rendered due to their size.
Instances For
The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I)
for α
a root of f : R[X]
and I : Ideal R
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Promote AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot
to an alg_equiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Let α
have minimal polynomial f
over R
and I
be an ideal of R
,
then R[α] / (I) = (R[x] / (f)) / pS = (R/p)[x] / (f mod p)
.
Equations
- One or more equations did not get rendered due to their size.