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

Equations
@[simp]

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

The adjoined root.

Equations
@[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]

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

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.alg_hom {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (f : polynomial R) (x : S) :

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_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) :

@[instance]
def adjoin_root.is_maximal_span {K : Type w} [field K] {f : polynomial K} [irreducible f] :

@[instance]
def adjoin_root.field {K : Type w} [field K] {f : polynomial K} [irreducible f] :

Equations