# Adjoining roots of polynomials #

This file defines the commutative ring adjoin_root 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 adjoin_root f is constructed.

We suggest stating results on is_adjoin_root instead of adjoin_root to achieve higher generality, since is_adjoin_root works for all different constructions of R[α] including adjoin_root f = R[X]/(f) itself.

## Main definitions and results #

The main definitions are in the adjoin_root namespace.

• mk f : R[X] →+* adjoin_root f, the natural ring homomorphism.

• of f : R →+* adjoin_root f, the natural ring homomorphism.

• root f : adjoin_root f, the image of X in R[X]/(f).

• lift (i : R →+* S) (x : S) (h : f.eval₂ i x = 0) : (adjoin_root f) →+* S, the ring homomorphism from R[X]/(f) to S extending i : R →+* S and sending X to x.

• lift_hom (x : S) (hfx : aeval x f = 0) : adjoin_root f →ₐ[R] S, the algebra homomorphism from R[X]/(f) to S extending algebra_map R S and sending X to x

• equiv : (adjoin_root f →ₐ[F] E) ≃ {x // x ∈ (f.map (algebra_map F E)).roots} a bijection between algebra homomorphisms from adjoin_root and roots of f in S

def adjoin_root {R : Type u} [comm_ring R] (f : polynomial R) :

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
Instances for adjoin_root
@[protected, instance]
noncomputable def adjoin_root.comm_ring {R : Type u} [comm_ring R] (f : polynomial R) :
Equations
@[protected, instance]
noncomputable def adjoin_root.inhabited {R : Type u} [comm_ring R] (f : polynomial R) :
Equations
@[protected, instance]
noncomputable def adjoin_root.decidable_eq {R : Type u} [comm_ring R] (f : polynomial R) :
Equations
@[protected]
theorem adjoin_root.nontrivial {R : Type u} [comm_ring R] (f : polynomial R) [is_domain R] (h : f.degree 0) :
noncomputable def adjoin_root.mk {R : Type u} [comm_ring R] (f : polynomial R) :

Ring homomorphism from R[x] to adjoin_root f sending X to the root.

Equations
theorem adjoin_root.induction_on {R : Type u} [comm_ring R] (f : polynomial R) {C : Prop} (x : adjoin_root f) (ih : (p : , C ( p)) :
C x
noncomputable def adjoin_root.of {R : Type u} [comm_ring R] (f : polynomial R) :

Embedding of the original ring R into adjoin_root f.

Equations
@[protected, instance]
noncomputable def adjoin_root.algebra {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] :
Equations
@[protected, instance]
def adjoin_root.is_scalar_tower {R : Type u} {S : Type v} {K : Type w} [comm_ring R] (f : polynomial R) [ K] [ R] [ R] [ R] :
@[protected, instance]
def adjoin_root.smul_comm_class {R : Type u} {S : Type v} {K : Type w} [comm_ring R] (f : polynomial R) [ R] [ R] [ R] :
@[simp]
theorem adjoin_root.algebra_map_eq {R : Type u} [comm_ring R] (f : polynomial R) :
theorem adjoin_root.algebra_map_eq' {R : Type u} (S : Type v) [comm_ring R] (f : polynomial R) [ R] :
theorem adjoin_root.finite_type {R : Type u} [comm_ring R] (f : polynomial R) :
noncomputable def adjoin_root.root {R : Type u} [comm_ring R] (f : polynomial R) :

Equations
@[protected, instance]
noncomputable def adjoin_root.has_coe_t {R : Type u} [comm_ring R] {f : polynomial R} :
Equations
@[ext]
theorem adjoin_root.alg_hom_ext {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [semiring S] [ S] {g₁ g₂ : →ₐ[R] S} (h : g₁ = g₂ ) :
g₁ = g₂

Two R-alg_hom from adjoin_root f to the same R-algebra are the same iff they agree on root f.

@[simp]
theorem adjoin_root.mk_eq_mk {R : Type u} [comm_ring R] {f g h : polynomial R} :
g = h f g - h
@[simp]
theorem adjoin_root.mk_eq_zero {R : Type u} [comm_ring R] {f g : polynomial R} :
g = 0 f g
@[simp]
theorem adjoin_root.mk_self {R : Type u} [comm_ring R] {f : polynomial R} :
f = 0
@[simp]
theorem adjoin_root.mk_C {R : Type u} [comm_ring R] {f : polynomial R} (x : R) :
@[simp]
theorem adjoin_root.mk_X {R : Type u} [comm_ring R] {f : polynomial R} :
theorem adjoin_root.mk_ne_zero_of_degree_lt {R : Type u} [comm_ring R] {f : polynomial R} (hf : f.monic) {g : polynomial R} (h0 : g 0) (hd : g.degree < f.degree) :
g 0
theorem adjoin_root.mk_ne_zero_of_nat_degree_lt {R : Type u} [comm_ring R] {f : polynomial R} (hf : f.monic) {g : polynomial R} (h0 : g 0) (hd : g.nat_degree < f.nat_degree) :
g 0
@[simp]
theorem adjoin_root.aeval_eq {R : Type u} [comm_ring R] {f : polynomial R} (p : polynomial R) :
= p
@[simp]
theorem adjoin_root.eval₂_root {R : Type u} [comm_ring R] (f : polynomial R) :
= 0
theorem adjoin_root.is_root_root {R : Type u} [comm_ring R] (f : polynomial R) :
f).is_root
theorem adjoin_root.is_algebraic_root {R : Type u} [comm_ring R] {f : polynomial R} (hf : f 0) :
noncomputable def adjoin_root.lift {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] (i : R →+* S) (x : S) (h : f = 0) :

Lift a ring homomorphism i : R →+* S to adjoin_root f →+* S.

Equations
• h = _
@[simp]
theorem adjoin_root.lift_mk {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : f = 0) (g : polynomial R) :
a h) ( g) = g
@[simp]
theorem adjoin_root.lift_root {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : f = 0) :
a h) = a
@[simp]
theorem adjoin_root.lift_of {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : f = 0) {x : R} :
a h) x = i x
@[simp]
theorem adjoin_root.lift_comp_of {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] {i : R →+* S} {a : S} (h : f = 0) :
a h).comp = i
noncomputable def adjoin_root.lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [ S] (x : S) (hfx : f = 0) :

Produce an algebra homomorphism adjoin_root f →ₐ[R] S sending root f to a root of f in S.

Equations
@[simp]
theorem adjoin_root.coe_lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [ S] (x : S) (hfx : f = 0) :
hfx) = x hfx
@[simp]
theorem adjoin_root.aeval_alg_hom_eq_zero {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [ S] (ϕ : →ₐ[R] S) :
@[simp]
theorem adjoin_root.lift_hom_eq_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (f : polynomial R) (ϕ : →ₐ[R] S) :
(ϕ (adjoin_root.root f)) _ = ϕ
@[simp]
theorem adjoin_root.lift_hom_mk {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [ S] (hfx : f = 0) {g : polynomial R} :
hfx) ( g) = g
@[simp]
theorem adjoin_root.lift_hom_root {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [ S] (hfx : f = 0) :
hfx) = a
@[simp]
theorem adjoin_root.lift_hom_of {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [ S] (hfx : f = 0) {x : R} :
hfx) ( x) = S) x
@[simp]
theorem adjoin_root.root_is_inv {R : Type u} [comm_ring R] (r : R) :
theorem adjoin_root.alg_hom_subsingleton {R : Type u} [comm_ring R] {S : Type u_1} [comm_ring S] [ S] {r : R} :
theorem adjoin_root.is_domain_of_prime {R : Type u} [comm_ring R] {f : polynomial R} (hf : prime f) :
@[protected, instance]
@[protected, instance]
noncomputable def adjoin_root.field {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
Equations
theorem adjoin_root.coe_injective {K : Type w} [field K] {f : polynomial K} (h : f.degree 0) :
theorem adjoin_root.coe_injective' {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
theorem adjoin_root.mul_div_root_cancel {K : Type w} [field K] (f : polynomial K) [fact (irreducible f)] :
* f / =
@[protected, instance]
theorem adjoin_root.is_integral_root' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
noncomputable def adjoin_root.mod_by_monic_hom {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

adjoin_root.mod_by_monic_hom sends the equivalence class of f mod g to f %ₘ g.

This is a well-defined right inverse to adjoin_root.mk, see adjoin_root.mk_left_inverse.

Equations
@[simp]
theorem adjoin_root.mod_by_monic_hom_mk {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (f : polynomial R) :
( f) = f %ₘ g
theorem adjoin_root.mk_left_inverse {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
theorem adjoin_root.mk_surjective {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
noncomputable def adjoin_root.power_basis_aux' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

The elements 1, root g, ..., root g ^ (d - 1) form a basis for adjoin_root g, where g is a monic polynomial of degree d.

Equations
@[simp]
theorem adjoin_root.power_basis_aux'_repr_symm_apply {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (c : →₀ R) :
c = (finset.univ.sum (λ (i : , (c i)))

This lemma could be autogenerated by @[simps] but unfortunately that would require unfolding that causes a timeout.

@[simp]
theorem adjoin_root.power_basis_aux'_repr_apply_to_fun {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (f : adjoin_root g) (i : fin g.nat_degree) :
(.repr) f) i = f).coeff i

This lemma could be autogenerated by @[simps] but unfortunately that would require unfolding that causes a timeout.

@[simp]
theorem adjoin_root.power_basis'_dim {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
noncomputable def adjoin_root.power_basis' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :

The power basis 1, root g, ..., root g ^ (d - 1) for adjoin_root g, where g is a monic polynomial of degree d.

Equations
@[simp]
theorem adjoin_root.power_basis'_gen {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
theorem adjoin_root.is_integral_root {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
theorem adjoin_root.minpoly_root {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
=
noncomputable def adjoin_root.power_basis_aux {K : Type w} [field K] {f : polynomial K} (hf : f 0) :

The elements 1, root f, ..., root f ^ (d - 1) form a basis for adjoin_root f, where f is an irreducible polynomial over a field of degree d.

Equations
• = let f' : := in _
@[simp]
theorem adjoin_root.power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
noncomputable def adjoin_root.power_basis {K : Type w} [field K] {f : polynomial K} (hf : f 0) :

The power basis 1, root f, ..., root f ^ (d - 1) for adjoin_root f, where f is an irreducible polynomial over a field of degree d.

Equations
@[simp]
theorem adjoin_root.power_basis_dim {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
theorem adjoin_root.minpoly_power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
=
theorem adjoin_root.minpoly_power_basis_gen_of_monic {K : Type w} [field K] {f : polynomial K} (hf : f.monic) (hf' : f 0 := _) :
.gen = f
@[simp]
theorem adjoin_root.minpoly.to_adjoin_apply (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [ S] (x : S) (ᾰ : adjoin_root (minpoly R x)) :
= (adjoin_root.lift {x})) x, _⟩ _)
noncomputable def adjoin_root.minpoly.to_adjoin (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [ S] (x : S) :

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 adjoin_root.minpoly.equiv_adjoin.

Equations
theorem adjoin_root.minpoly.to_adjoin_apply' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} (a : adjoin_root (minpoly R x)) :
= (adjoin_root.lift_hom (minpoly R x) x, _⟩ _) a
theorem adjoin_root.minpoly.to_adjoin.apply_X {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} :
theorem adjoin_root.minpoly.to_adjoin.surjective (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [ S] (x : S) :
@[simp]
theorem adjoin_root.equiv'_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (g : polynomial R) (pb : S) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
pb h₁ h₂).symm) = (pb.lift h₁)
noncomputable def adjoin_root.equiv' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (g : polynomial R) (pb : S) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :

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

Compare power_basis.equiv_of_root, which would require h₂ : aeval pb.gen (minpoly R (root g)) = 0; that minimal polynomial is not guaranteed to be identical to g.

Equations
@[simp]
theorem adjoin_root.equiv'_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (g : polynomial R) (pb : S) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
pb h₁ h₂) = pb.gen h₂)
@[simp]
theorem adjoin_root.equiv'_to_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (g : polynomial R) (pb : S) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
pb h₁ h₂).to_alg_hom = h₂
@[simp]
theorem adjoin_root.equiv'_symm_to_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (g : polynomial R) (pb : S) (h₁ : (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
pb h₁ h₂).symm.to_alg_hom = pb.lift h₁
noncomputable def adjoin_root.equiv (L : Type u_1) (F : Type u_2) [field F] [field L] [ L] (f : polynomial F) (hf : f 0) :
→ₐ[F] L) {x // x (polynomial.map L) f).roots}

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

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

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
noncomputable def adjoin_root.polynomial.quot_quot_equiv_comm {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

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

The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : R[X] and I : ideal R.

Equations
@[simp]
theorem adjoin_root.quot_equiv_quot_map_apply {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) (ᾰ : I) :
@[simp]
theorem adjoin_root.quot_equiv_quot_map_symm_apply {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) (ᾰ : polynomial (R I) ) :
noncomputable def adjoin_root.quot_equiv_quot_map {R : Type u} [comm_ring R] (f : polynomial R) (I : ideal R) :

Promote adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot to an alg_equiv.

Equations
@[simp]
theorem adjoin_root.quot_equiv_quot_map_apply_mk {R : Type u} [comm_ring R] (f g : polynomial R) (I : ideal R) :
((ideal.quotient.mk I)) ( g)) = g)
@[simp]
noncomputable def power_basis.quotient_equiv_quotient_minpoly_map {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (pb : S) (I : ideal R) :

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
@[simp]
theorem power_basis.quotient_equiv_quotient_minpoly_map_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (pb : S) (I : ideal R) (ᾰ : S ideal.map S) I) :
@[simp]
theorem power_basis.quotient_equiv_quotient_minpoly_map_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] (pb : S) (I : ideal R) (ᾰ : polynomial (R I) ideal.span (minpoly R pb.gen)}) :
.symm) = (( I).symm) ᾰ)