# Adjoining roots of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.has_smul {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] [ R] :
Equations
@[protected, instance]
noncomputable def adjoin_root.distrib_smul {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] [ R] :
Equations
@[simp]
theorem adjoin_root.smul_mk {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] [ R] (a : S) (x : polynomial R) :
a x = (a x)
theorem adjoin_root.smul_of {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] [ R] (a : S) (x : R) :
a x = (a x)
@[protected, instance]
def adjoin_root.is_scalar_tower {R : Type u} [comm_ring R] (R₁ : Type u_1) (R₂ : Type u_2) [has_smul R₁ R₂] [ R] [ R] [ R R] [ R R] [ R₂ R] (f : polynomial R) :
@[protected, instance]
def adjoin_root.smul_comm_class {R : Type u} [comm_ring R] (R₁ : Type u_1) (R₂ : Type u_2) [ R] [ R] [ R R] [ R R] [ R₂ R] (f : polynomial R) :
@[protected, instance]
def adjoin_root.is_scalar_tower_right {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] [ R] :
@[protected, instance]
noncomputable def adjoin_root.distrib_mul_action {R : Type u} {S : Type v} [comm_ring R] [monoid S] [ R] [ R] (f : polynomial R) :
Equations
@[protected, instance]
noncomputable def adjoin_root.algebra {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [ R] :
Equations
@[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) ᾰ)