# 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.

## 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) :
Type u

Adjoin a root of a polynomial f to a commutative ring R. We define the new ring as the quotient of polynomial R 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) :
theorem adjoin_root.finite_presentation {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_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} :
@[simp]
theorem adjoin_root.aeval_eq {R : Type u} [comm_ring R] {f : polynomial R} (p : polynomial R) :
= p
theorem adjoin_root.adjoin_root_eq_top {R : Type u} [comm_ring R] {f : polynomial R} :
@[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} :
@[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]
def adjoin_root.is_noetherian_ring {R : Type u} [comm_ring R] {f : polynomial R} :
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) (ᾰ : →₀ R) :
= (finset.univ.sum (λ (x : , (ᾰ x)))
@[simp]
theorem adjoin_root.power_basis_aux'_repr_apply_support_val {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (ᾰ : adjoin_root g) :
@[simp]
theorem adjoin_root.power_basis_aux'_repr_apply_to_fun {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (ᾰ : adjoin_root g) (ᾰ_1 : fin g.nat_degree) :
(.repr) ᾰ) ᾰ_1 = ᾰ).coeff ᾰ_1
@[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) :
theorem adjoin_root.minpoly.to_adjoin.injective {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) :
@[simp]
theorem adjoin_root.minpoly.equiv_adjoin_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) (ᾰ : adjoin_root (minpoly R x)) :
= (adjoin_root.lift {x})) x, _⟩ _)
noncomputable def adjoin_root.minpoly.equiv_adjoin {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) :

The algebra isomorphism adjoin_root (minpoly R x) ≃ₐ[R] adjoin R x

Equations
@[simp]
theorem adjoin_root.minpoly.equiv_adjoin_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) (ᾰ : {x})) :
=
@[simp]
theorem algebra.adjoin.power_basis'_dim {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) :
@[simp]
theorem algebra.adjoin.power_basis'_gen {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) :
= x, _⟩
noncomputable def algebra.adjoin.power_basis' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (hx : x) :
{x})

The power_basis of adjoin R {x} given by x. See algebra.adjoin.power_basis for a version over a field.

Equations
@[simp]
theorem power_basis.of_gen_mem_adjoin'_gen {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (B : S) (hint : x) (hx : B.gen {x}) :
noncomputable def power_basis.of_gen_mem_adjoin' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (B : S) (hint : x) (hx : B.gen {x}) :
S

The power basis given by x if B.gen ∈ adjoin R {x}.

Equations
@[simp]
theorem power_basis.of_gen_mem_adjoin'_dim {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [ S] {x : S} [is_domain R] [is_domain S] (B : S) (hint : x) (hx : B.gen {x}) :
@[simp]
theorem adjoin_root.equiv'_symm_apply {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [comm_ring S] [is_domain 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] [is_domain R] [comm_ring S] [is_domain 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] [is_domain R] [comm_ring S] [is_domain 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] [is_domain R] [comm_ring S] [is_domain 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] [is_domain R] [comm_ring S] [is_domain 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 : polynomial R 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 : polynomial R 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 : polynomial R and I : ideal R

Equations
@[simp]
@[simp]
noncomputable def adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :

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

Equations