mathlib documentation

ring_theory.adjoin_root

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.

@[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 : adjoin_root f Prop} (x : adjoin_root f) (ih : (p : polynomial R), C ((adjoin_root.mk f) 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) [comm_semiring S] [algebra S 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) [comm_semiring S] [comm_semiring K] [has_smul S K] [algebra S R] [algebra K R] [is_scalar_tower S K R] :
@[protected, instance]
def adjoin_root.smul_comm_class {R : Type u} {S : Type v} {K : Type w} [comm_ring R] (f : polynomial R) [comm_semiring S] [comm_semiring K] [algebra S R] [algebra K R] [smul_comm_class S K R] :
noncomputable def adjoin_root.root {R : Type u} [comm_ring R] (f : polynomial R) :

The adjoined root.

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] [algebra R S] {g₁ g₂ : adjoin_root f →ₐ[R] S} (h : g₁ (adjoin_root.root f) = g₂ (adjoin_root.root f)) :
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} :
@[simp]
theorem adjoin_root.mk_self {R : Type u} [comm_ring R] {f : polynomial R} :
@[simp]
theorem adjoin_root.mk_C {R : Type u} [comm_ring R] {f : polynomial R} (x : R) :
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 : polynomial.eval₂ i x f = 0) :

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

Equations
@[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 : polynomial.eval₂ i a f = 0) (g : polynomial R) :
@[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 : polynomial.eval₂ i a f = 0) :
@[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 : polynomial.eval₂ i a f = 0) {x : R} :
@[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 : polynomial.eval₂ i a f = 0) :
noncomputable def adjoin_root.lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [algebra R S] (x : S) (hfx : (polynomial.aeval x) 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] [algebra R S] (x : S) (hfx : (polynomial.aeval x) f = 0) :
@[simp]
@[simp]
theorem adjoin_root.lift_hom_eq_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (f : polynomial R) (ϕ : adjoin_root f →ₐ[R] S) :
@[simp]
theorem adjoin_root.lift_hom_mk {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : (polynomial.aeval a) f = 0) {g : polynomial R} :
@[simp]
theorem adjoin_root.lift_hom_root {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : (polynomial.aeval a) f = 0) :
@[simp]
theorem adjoin_root.lift_hom_of {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] {a : S} [algebra R S] (hfx : (polynomial.aeval a) f = 0) {x : R} :
@[protected, instance]
@[protected, instance]
noncomputable def adjoin_root.field {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
Equations
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
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
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
theorem adjoin_root.is_integral_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
@[simp]
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_of_monic {K : Type w} [field K] {f : polynomial K} (hf : f.monic) (hf' : f 0 := _) :
@[simp]
theorem adjoin_root.minpoly.to_adjoin_apply (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) (ᾰ : adjoin_root (minpoly R x)) :
noncomputable def adjoin_root.minpoly.to_adjoin (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R 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

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

Equations
noncomputable def algebra.adjoin.power_basis' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} [is_domain R] [normalized_gcd_monoid R] [is_domain S] [no_zero_smul_divisors R S] (hx : is_integral R 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] [algebra R S] {x : S} [is_domain R] [normalized_gcd_monoid R] [is_domain S] [no_zero_smul_divisors R S] (B : power_basis R S) (hint : is_integral R x) (hx : B.gen algebra.adjoin R {x}) :
(B.of_gen_mem_adjoin' hint hx).gen = x
noncomputable def power_basis.of_gen_mem_adjoin' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} [is_domain R] [normalized_gcd_monoid R] [is_domain S] [no_zero_smul_divisors R S] (B : power_basis R S) (hint : is_integral R x) (hx : B.gen algebra.adjoin R {x}) :

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] [algebra R S] {x : S} [is_domain R] [normalized_gcd_monoid R] [is_domain S] [no_zero_smul_divisors R S] (B : power_basis R S) (hint : is_integral R x) (hx : B.gen algebra.adjoin R {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] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : (polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
((adjoin_root.equiv' g pb h₁ h₂).symm) = (pb.lift (adjoin_root.root g) h₁)
noncomputable def adjoin_root.equiv' {R : Type u} {S : Type v} [comm_ring R] [is_domain R] [comm_ring S] [is_domain S] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : (polynomial.aeval (adjoin_root.root g)) (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] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : (polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
(adjoin_root.equiv' g pb h₁ h₂) = (adjoin_root.lift_hom g 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] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : (polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
@[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] [algebra R S] (g : polynomial R) (pb : power_basis R S) (h₁ : (polynomial.aeval (adjoin_root.root g)) (minpoly R pb.gen) = 0) (h₂ : (polynomial.aeval pb.gen) g = 0) :
noncomputable def adjoin_root.equiv (L : Type u_1) (F : Type u_2) [field F] [field L] [algebra F L] (f : polynomial F) (hf : f 0) :

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

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