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.instInhabited 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 = (AdjoinRoot.mk f).comp Polynomial.C
Instances For
Equations
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
R[x]/(f)
is R
-algebra
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) ⋯
Instances For
Produce an algebra homomorphism AdjoinRoot f →ₐ[R] S
sending root f
to
a root of f
in S
.
Equations
- AdjoinRoot.liftHom f x hfx = { toRingHom := AdjoinRoot.lift (algebraMap R S) x hfx, commutes' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Equations
- AdjoinRoot.instGroupWithZero = Ideal.Quotient.groupWithZero (Ideal.span {f})
If R
is a field and f
is irreducible, then AdjoinRoot f
is a field
Equations
- AdjoinRoot.instField = Field.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x1 : ℚ≥0) (x2 : AdjoinRoot f) => x1 • x2) ⋯ ⋯ (fun (x1 : ℚ) (x2 : AdjoinRoot f) => x1 • x2) ⋯
Equations
- ⋯ = ⋯
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
- AdjoinRoot.modByMonicHom hg = (Submodule.restrictScalars R (Ideal.span {g})).liftQ g.modByMonicHom ⋯ ∘ₗ ↑(Submodule.Quotient.restrictScalarsEquiv R (Ideal.span {g})).symm
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
- AdjoinRoot.powerBasis' hg = { gen := AdjoinRoot.root g, dim := g.natDegree, basis := AdjoinRoot.powerBasisAux' hg, basis_eq_pow := ⋯ }
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
- AdjoinRoot.powerBasisAux hf = Basis.mk ⋯ ⋯
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
- AdjoinRoot.powerBasis hf = { gen := AdjoinRoot.root f, dim := f.natDegree, basis := AdjoinRoot.powerBasisAux hf, basis_eq_pow := ⋯ }
Instances For
The surjective algebra morphism R[X]/(minpoly R x) → R[x]
.
If R
is a integrally closed domain and x
is integral, this is an isomorphism,
see minpoly.equivAdjoin
.
Equations
- AdjoinRoot.Minpoly.toAdjoin R x = AdjoinRoot.liftHom (minpoly R x) ⟨x, ⋯⟩ ⋯
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
- AdjoinRoot.equiv L F f hf = (AdjoinRoot.powerBasis hf).liftEquiv'.trans ((Equiv.refl L).subtypeEquiv ⋯)
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
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
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
- pb.quotientEquivQuotientMinpolyMap I = (AlgEquiv.ofRingEquiv ⋯).trans (AdjoinRoot.quotEquivQuotMap (minpoly R pb.gen) I)
Instances For
If L / K
is an integral extension, K
is a domain, L
is a field, then any irreducible
polynomial over L
divides some monic irreducible polynomial over K
.