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.

Main definitions and results #

The main definitions are in the adjoin_root namespace.

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
@[instance]
def adjoin_root.inhabited {R : Type u} [comm_ring R] (f : polynomial R) :
Equations
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
def adjoin_root.of {R : Type u} [comm_ring R] (f : polynomial R) :

Embedding of the original ring R into adjoin_root f.

Equations
@[simp]
def adjoin_root.root {R : Type u} [comm_ring R] (f : polynomial R) :

The adjoined root.

Equations
@[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) :
@[simp]
@[simp]
theorem adjoin_root.is_algebraic_root {R : Type u} [comm_ring R] {f : polynomial R} (hf : f 0) :
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) :
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]
theorem adjoin_root.aeval_alg_hom_eq_zero {R : Type u} {S : Type v} [comm_ring R] (f : polynomial R) [comm_ring S] [algebra R S] (ϕ : adjoin_root f →ₐ[R] S) :
@[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} :
@[instance]
def adjoin_root.is_maximal_span {K : Type w} [field K] {f : polynomial K} [irreducible f] :
theorem adjoin_root.is_integral_root' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
@[simp]
def adjoin_root.power_basis_aux' {R : Type u} [comm_ring R] {g : polynomial R} [nontrivial 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]
@[simp]
def adjoin_root.power_basis' {R : Type u} [comm_ring R] {g : polynomial R} [nontrivial 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.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) :
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]
@[simp]
theorem adjoin_root.power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f 0) :
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.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₁)
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) :
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