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 : polynomial R →+* 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.

source

def adjoin_root {R : Type u} [comm_ring R] :

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 R by the principal ideal of f.

Equations

adjoin_root f = (ideal.span {f}).quotient

source

@[instance]

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

comm_ring (adjoin_root f)

Equations

adjoin_root.comm_ring f = ideal.quotient.comm_ring (ideal.span {f})

source

@[instance]

def adjoin_root.inhabited {R : Type u} [comm_ring R] (f : polynomial R) :

inhabited (adjoin_root f)

Equations

adjoin_root.inhabited f = {default := 0}

source

@[instance]

def adjoin_root.decidable_eq {R : Type u} [comm_ring R] (f : polynomial R) :

decidable_eq (adjoin_root f)

Equations

adjoin_root.decidable_eq f = classical.dec_eq (adjoin_root f)

source

def adjoin_root.mk {R : Type u} [comm_ring R] (f : polynomial R) :

polynomial R →+* adjoin_root f

Ring homomorphism from R[x] to adjoin_root f sending X to the root.

Equations

adjoin_root.mk f = ideal.quotient.mk (ideal.span {f})

source

theorem adjoin_root.induction_on {R : Type u} [comm_ring R] (f : polynomial R) {C : adjoin_root f → Prop} (x : adjoin_root f) :

(∀ (p : polynomial R), C (⇑(adjoin_root.mk f) p)) → C x

source

def adjoin_root.of {R : Type u} [comm_ring R] (f : polynomial R) :

R →+* adjoin_root f

Embedding of the original ring R into adjoin_root f.

Equations

adjoin_root.of f = (adjoin_root.mk f).comp (ring_hom.of ⇑polynomial.C)

source

@[instance]

def adjoin_root.algebra {R : Type u} [comm_ring R] (f : polynomial R) :

algebra R (adjoin_root f)

Equations

adjoin_root.algebra f = (adjoin_root.of f).to_algebra

source

@[simp]

theorem adjoin_root.algebra_map_eq {R : Type u} [comm_ring R] (f : polynomial R) :

algebra_map R (adjoin_root f) = adjoin_root.of f

source

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

adjoin_root f

The adjoined root.

Equations

adjoin_root.root f = ⇑(adjoin_root.mk f) polynomial.X

source

@[instance]

def adjoin_root.adjoin_root.has_coe_t {R : Type u} [comm_ring R] {f : polynomial R} :

has_coe_t R (adjoin_root f)

Equations

adjoin_root.adjoin_root.has_coe_t = {coe := ⇑(adjoin_root.of f)}

source

@[simp]

theorem adjoin_root.mk_self {R : Type u} [comm_ring R] {f : polynomial R} :

⇑(adjoin_root.mk f) f = 0

source

@[simp]

theorem adjoin_root.mk_C {R : Type u} [comm_ring R] {f : polynomial R} (x : R) :

⇑(adjoin_root.mk f) (⇑polynomial.C x) = ↑x

source

@[simp]

theorem adjoin_root.mk_X {R : Type u} [comm_ring R] {f : polynomial R} :

⇑(adjoin_root.mk f) polynomial.X = adjoin_root.root f

source

@[simp]

theorem adjoin_root.aeval_eq {R : Type u} [comm_ring R] {f : polynomial R} (p : polynomial R) :

⇑(polynomial.aeval (adjoin_root.root f)) p = ⇑(adjoin_root.mk f) p

source

theorem adjoin_root.adjoin_root_eq_top {R : Type u} [comm_ring R] {f : polynomial R} :

algebra.adjoin R {adjoin_root.root f} = ⊤

source

@[simp]

theorem adjoin_root.eval₂_root {R : Type u} [comm_ring R] (f : polynomial R) :

polynomial.eval₂ (adjoin_root.of f) (adjoin_root.root f) f = 0

source

theorem adjoin_root.is_root_root {R : Type u} [comm_ring R] (f : polynomial R) :

(polynomial.map (adjoin_root.of f) f).is_root (adjoin_root.root f)

source

def adjoin_root.lift {R : Type u} {S : Type v} [comm_ring R] {f : polynomial R} [comm_ring S] (i : R →+* S) (x : S) :

polynomial.eval₂ i x f = 0 → adjoin_root f →+* S

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

Equations

adjoin_root.lift i x h = ideal.quotient.lift (ideal.span {f}) (polynomial.eval₂_ring_hom i x) _

source

@[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} :

⇑(adjoin_root.lift i a h) (⇑(adjoin_root.mk f) g) = polynomial.eval₂ i a g

source

@[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} :

⇑(adjoin_root.lift i a h) (adjoin_root.root f) = a

source

@[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} :

⇑(adjoin_root.lift i a h) ↑x = ⇑i x

source

@[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} :

(adjoin_root.lift i a h).comp (adjoin_root.of f) = i

source

def adjoin_root.alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (f : polynomial R) (x : S) :

⇑(polynomial.aeval x) f = 0 → (adjoin_root f →ₐ[R] S)

Produce an algebra homomorphism adjoin_root f →ₐ[R] S sending root f to a root of f in S.

Equations

adjoin_root.alg_hom f x hfx = {to_fun := (adjoin_root.lift (algebra_map R S) x hfx).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem adjoin_root.coe_alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (f : polynomial R) (x : S) (hfx : ⇑(polynomial.aeval x) f = 0) :

↑(adjoin_root.alg_hom f x hfx) = adjoin_root.lift (algebra_map R S) x hfx

source

@[instance]