mathlib3 documentation

ring_theory.adjoin_root

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.

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

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

@[simp]

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

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
@[simp]
theorem adjoin_root.equiv'_symm_apply {R : Type u} {S : Type v} [comm_ring R] [comm_ring 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] [comm_ring 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] [comm_ring 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] [comm_ring 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] [comm_ring 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