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.

source
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
Instances for adjoin_root
source
@[protected, instance]
noncomputable def adjoin_root.comm_ring {R : Type u} [comm_ring R] (f : polynomial R) :
comm_ring (adjoin_root f)
Equations
source
@[protected, instance]
noncomputable def adjoin_root.inhabited {R : Type u} [comm_ring R] (f : polynomial R) :
inhabited (adjoin_root f)
Equations
source
@[protected, instance]
noncomputable def adjoin_root.decidable_eq {R : Type u} [comm_ring R] (f : polynomial R) :
decidable_eq (adjoin_root f)
Equations
source
@[protected]
theorem adjoin_root.nontrivial {R : Type u} [comm_ring R] (f : polynomial R) [is_domain R] (h : f.degree ≠ 0) :
nontrivial (adjoin_root f)
source
noncomputable 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
source
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
source
noncomputable 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
source
@[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] :
algebra S (adjoin_root f)
Equations
source
@[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] :
is_scalar_tower S K (adjoin_root f)
source
@[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] :
smul_comm_class S K (adjoin_root f)
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
theorem adjoin_root.algebra_map_eq' {R : Type u} (S : Type v) [comm_ring R] (f : polynomial R) [comm_semiring S] [algebra S R] :
algebra_map S (adjoin_root f) = (adjoin_root.of f).comp (algebra_map S R)
source
theorem adjoin_root.finite_type {R : Type u} [comm_ring R] (f : polynomial R) :
algebra.finite_type R (adjoin_root f)
source
theorem adjoin_root.finite_presentation {R : Type u} [comm_ring R] (f : polynomial R) :
algebra.finite_presentation R (adjoin_root f)
source
noncomputable def adjoin_root.root {R : Type u} [comm_ring R] (f : polynomial R) :
adjoin_root f

The adjoined root.

Equations
source
@[protected, instance]
noncomputable def adjoin_root.has_coe_t {R : Type u} [comm_ring R] {f : polynomial R} :
has_coe_t R (adjoin_root f)
Equations
source
@[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.

source
@[simp]
theorem adjoin_root.mk_eq_mk {R : Type u} [comm_ring R] {f g h : polynomial R} :
⇑(adjoin_root.mk f) g = ⇑(adjoin_root.mk f) h ↔ f ∣ g - h
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
theorem adjoin_root.is_algebraic_root {R : Type u} [comm_ring R] {f : polynomial R} (hf : f ≠ 0) :
is_algebraic R (adjoin_root.root f)
source
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) :
adjoin_root f →+* S

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

Equations
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
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) :
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
source
@[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) :
↑(adjoin_root.lift_hom f x hfx) = adjoin_root.lift (algebra_map R S) x hfx
source
@[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) :
⇑(polynomial.aeval (⇑ϕ (adjoin_root.root f))) f = 0
source
@[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) :
adjoin_root.lift_hom f (⇑ϕ (adjoin_root.root f)) _ = ϕ
source
@[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} :
⇑(adjoin_root.lift_hom f a hfx) (⇑(adjoin_root.mk f) g) = ⇑(polynomial.aeval a) g
source
@[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) :
⇑(adjoin_root.lift_hom f a hfx) (adjoin_root.root f) = a
source
@[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} :
⇑(adjoin_root.lift_hom f a hfx) (⇑(adjoin_root.of f) x) = ⇑(algebra_map R S) x
source
@[simp]
theorem adjoin_root.root_is_inv {R : Type u} [comm_ring R] (r : R) :
⇑(adjoin_root.of (⇑polynomial.C r * polynomial.X - 1)) r * adjoin_root.root (⇑polynomial.C r * polynomial.X - 1) = 1
source
theorem adjoin_root.alg_hom_subsingleton {R : Type u} [comm_ring R] {S : Type u_1} [comm_ring S] [algebra R S] {r : R} :
subsingleton (adjoin_root (⇑polynomial.C r * polynomial.X - 1) →ₐ[R] S)
source
@[protected, instance]
def adjoin_root.span_maximal_of_irreducible {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
(ideal.span {f}).is_maximal
source
@[protected, instance]
noncomputable def adjoin_root.field {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
field (adjoin_root f)
Equations
source
theorem adjoin_root.coe_injective {K : Type w} [field K] {f : polynomial K} (h : f.degree ≠ 0) :
function.injective coe
source
theorem adjoin_root.coe_injective' {K : Type w} [field K] {f : polynomial K} [fact (irreducible f)] :
function.injective coe
source
theorem adjoin_root.mul_div_root_cancel {K : Type w} [field K] (f : polynomial K) [fact (irreducible f)] :
(polynomial.X - ⇑polynomial.C (adjoin_root.root f)) * (polynomial.map (adjoin_root.of f) f / (polynomial.X - ⇑polynomial.C (adjoin_root.root f))) = polynomial.map (adjoin_root.of f) f
source
@[protected, instance]
def adjoin_root.is_noetherian_ring {R : Type u} [comm_ring R] [is_noetherian_ring R] {f : polynomial R} :
is_noetherian_ring (adjoin_root f)
source
theorem adjoin_root.is_integral_root' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
is_integral R (adjoin_root.root g)
source
noncomputable def adjoin_root.mod_by_monic_hom {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
adjoin_root g →ₗ[R] polynomial R

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
source
@[simp]
theorem adjoin_root.mod_by_monic_hom_mk {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (f : polynomial R) :
⇑(adjoin_root.mod_by_monic_hom hg) (⇑(adjoin_root.mk g) f) = f %ₘ g
source
theorem adjoin_root.mk_left_inverse {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
function.left_inverse ⇑(adjoin_root.mk g) ⇑(adjoin_root.mod_by_monic_hom hg)
source
theorem adjoin_root.mk_surjective {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
function.surjective ⇑(adjoin_root.mk g)
source
noncomputable def adjoin_root.power_basis_aux' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
basis (fin g.nat_degree) R (adjoin_root g)

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
source
@[simp]
theorem adjoin_root.power_basis_aux'_repr_symm_apply {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (ᾰ : fin g.nat_degree →₀ R) :
⇑((adjoin_root.power_basis_aux' hg).repr.symm) ᾰ = ⇑(adjoin_root.mk g) (finset.univ.sum (λ (x : fin g.nat_degree), ⇑(polynomial.monomial ↑x) (⇑ᾰ x)))
source
@[simp]
theorem adjoin_root.power_basis_aux'_repr_apply_support_val {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (ᾰ : adjoin_root g) :
(⇑((adjoin_root.power_basis_aux' hg).repr) ᾰ).support.val = multiset.filter (λ (a : fin g.nat_degree), ¬(⇑(adjoin_root.mod_by_monic_hom hg) ᾰ).coeff ↑a = 0) finset.univ.val
source
@[simp]
theorem adjoin_root.power_basis_aux'_repr_apply_to_fun {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) (ᾰ : adjoin_root g) (ᾰ_1 : fin g.nat_degree) :
⇑(⇑((adjoin_root.power_basis_aux' hg).repr) ᾰ) ᾰ_1 = (⇑(adjoin_root.mod_by_monic_hom hg) ᾰ).coeff ↑ᾰ_1
source
@[simp]
theorem adjoin_root.power_basis'_dim {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
(adjoin_root.power_basis' hg).dim = g.nat_degree
source
noncomputable def adjoin_root.power_basis' {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
power_basis R (adjoin_root g)

The power basis 1, root g, ..., root g ^ (d - 1) for adjoin_root g, where g is a monic polynomial of degree d.

Equations
source
@[simp]
theorem adjoin_root.power_basis'_gen {R : Type u} [comm_ring R] {g : polynomial R} (hg : g.monic) :
(adjoin_root.power_basis' hg).gen = adjoin_root.root g
source
theorem adjoin_root.is_integral_root {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
is_integral K (adjoin_root.root f)
source
theorem adjoin_root.minpoly_root {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
minpoly K (adjoin_root.root f) = f * ⇑polynomial.C (f.leading_coeff)⁻¹
source
noncomputable def adjoin_root.power_basis_aux {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
basis (fin f.nat_degree) K (adjoin_root f)

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
source
@[simp]
theorem adjoin_root.power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
(adjoin_root.power_basis hf).gen = adjoin_root.root f
source
noncomputable def adjoin_root.power_basis {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
power_basis K (adjoin_root f)

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
source
@[simp]
theorem adjoin_root.power_basis_dim {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
(adjoin_root.power_basis hf).dim = f.nat_degree
source
theorem adjoin_root.minpoly_power_basis_gen {K : Type w} [field K] {f : polynomial K} (hf : f ≠ 0) :
minpoly K (adjoin_root.power_basis hf).gen = f * ⇑polynomial.C (f.leading_coeff)⁻¹
source
theorem adjoin_root.minpoly_power_basis_gen_of_monic {K : Type w} [field K] {f : polynomial K} (hf : f.monic) (hf' : f ≠ 0 := _) :
minpoly K (adjoin_root.power_basis hf').gen = f
source
@[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)) :
⇑(adjoin_root.minpoly.to_adjoin R x) ᾰ = ⇑(adjoin_root.lift (algebra_map R ↥(algebra.adjoin R {x})) ⟨x, _⟩ _) ᾰ
source
noncomputable def adjoin_root.minpoly.to_adjoin (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) :
adjoin_root (minpoly R x) →ₐ[R] ↥(algebra.adjoin R {x})

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
source
theorem adjoin_root.minpoly.to_adjoin_apply' {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} (a : adjoin_root (minpoly R x)) :
⇑(adjoin_root.minpoly.to_adjoin R x) a = ⇑(adjoin_root.lift_hom (minpoly R x) ⟨x, _⟩ _) a
source
theorem adjoin_root.minpoly.to_adjoin.apply_X {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] {x : S} :
⇑(adjoin_root.minpoly.to_adjoin R x) (⇑(adjoin_root.mk (minpoly R x)) polynomial.X) = ⟨x, _⟩
source
theorem adjoin_root.minpoly.to_adjoin.surjective (R : Type u) {S : Type v} [comm_ring R] [comm_ring S] [algebra R S] (x : S) :
function.surjective ⇑(adjoin_root.minpoly.to_adjoin R x)
source
theorem adjoin_root.minpoly.to_adjoin.injective {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) :
function.injective ⇑(adjoin_root.minpoly.to_adjoin R x)
source
@[simp]
theorem adjoin_root.minpoly.equiv_adjoin_apply {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) (ᾰ : adjoin_root (minpoly R x)) :
⇑(adjoin_root.minpoly.equiv_adjoin hx) ᾰ = ⇑(adjoin_root.lift (algebra_map R ↥(algebra.adjoin R {x})) ⟨x, _⟩ _) ᾰ
source
noncomputable def adjoin_root.minpoly.equiv_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] (hx : is_integral R x) :
adjoin_root (minpoly R x) ≃ₐ[R] ↥(algebra.adjoin R {x})

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

Equations
source
@[simp]
theorem adjoin_root.minpoly.equiv_adjoin_symm_apply {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) (ᾰ : ↥(algebra.adjoin R {x})) :
⇑((adjoin_root.minpoly.equiv_adjoin hx).symm) ᾰ = ⇑((ring_equiv.of_bijective ↑(adjoin_root.minpoly.to_adjoin R x) _).symm) ᾰ
source
@[simp]
theorem algebra.adjoin.power_basis'_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] (hx : is_integral R x) :
(algebra.adjoin.power_basis' hx).dim = (minpoly R x).nat_degree
source
@[simp]
theorem algebra.adjoin.power_basis'_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] (hx : is_integral R x) :
(algebra.adjoin.power_basis' hx).gen = ⟨x, _⟩
source
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) :
power_basis R ↥(algebra.adjoin R {x})

The power_basis of adjoin R {x} given by x. See algebra.adjoin.power_basis for a version over a field.

Equations
source
@[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
source
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}) :
power_basis R S

The power basis given by x if B.gen ∈ adjoin R {x}.

Equations
source
@[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}) :
(B.of_gen_mem_adjoin' hint hx).dim = (minpoly R x).nat_degree
source
@[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₁)
source
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) :
adjoin_root g ≃ₐ[R] S

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
source
@[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₂)
source
@[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) :
(adjoin_root.equiv' g pb h₁ h₂).to_alg_hom = adjoin_root.lift_hom g pb.gen h₂
source
@[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) :
(adjoin_root.equiv' g pb h₁ h₂).symm.to_alg_hom = pb.lift (adjoin_root.root g) h₁
source
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) :
(adjoin_root f →ₐ[F] L) ≃ {x // x ∈ (polynomial.map (algebra_map F L) f).roots}

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
source
noncomputable def adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
adjoin_root f ⧸ ideal.map (adjoin_root.of f) I ≃+* adjoin_root f ⧸ ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I)

The natural isomorphism R[α]/(I[α]) ≅ R[α]/((I[x] ⊔ (f)) / (f)) for α a root of f : polynomial R and I : ideal R.

See adjoin_root.quot_map_of_equiv for the isomorphism with (R/I)[X] / (f mod I).

Equations
source
@[simp]
theorem adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) (x : adjoin_root f) :
⇑(adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f) (⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) x) = ⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) x
source
theorem adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk_symm_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) (x : adjoin_root f) :
⇑((adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f).symm) (⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) x) = ⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) x
source
noncomputable def adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
adjoin_root f ⧸ ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I) ≃+* (polynomial R ⧸ ideal.map polynomial.C I) ⧸ ideal.map (ideal.quotient.mk (ideal.map polynomial.C I)) (ideal.span {f})

The natural isomorphism R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x]) for α a root of f : polynomial R and I : ideal R

Equations
source
@[simp]
theorem adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑(adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f) (⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) (⇑(adjoin_root.mk f) p)) = ⇑(double_quot.quot_quot_mk (ideal.map polynomial.C I) (ideal.span {f})) p
source
@[simp]
theorem adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk_symm_quot_quot_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑((adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f).symm) (⇑(double_quot.quot_quot_mk (ideal.map polynomial.C I) (ideal.span {f})) p) = ⇑(ideal.quotient.mk (ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I))) (⇑(adjoin_root.mk f) p)
source
noncomputable def adjoin_root.polynomial.quot_quot_equiv_comm {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f} ≃+* (polynomial R ⧸ ideal.map polynomial.C I) ⧸ ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f}

The natural isomorphism (R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x]) where f : polynomial R and I : ideal R

Equations
source
@[simp]
theorem adjoin_root.polynomial.quot_quot_equiv_comm_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑(adjoin_root.polynomial.quot_quot_equiv_comm I f) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)) = ⇑(ideal.quotient.mk (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f})) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) p)
source
@[simp]
theorem adjoin_root.polynomial.quot_quot_equiv_comm_symm_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑((adjoin_root.polynomial.quot_quot_equiv_comm I f).symm) (⇑(ideal.quotient.mk (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f})) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) p)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)
source
noncomputable def adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot {R : Type u} [comm_ring R] (I : ideal R) (f : polynomial R) :
adjoin_root f ⧸ ideal.map (adjoin_root.of f) I ≃+* polynomial (R ⧸ I) ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f}

The natural isomorphism R[α]/I[α] ≅ (R/I)[X]/(f mod I) for α a root of f : polynomial R and I : ideal R

Equations
source
@[simp]
theorem adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_mk_of {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑(adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f) (⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) p)) = ⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)
source
@[simp]
theorem adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot_symm_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : polynomial R) :
⇑((adjoin_root.quot_adjoin_root_equiv_quot_polynomial_quot I f).symm) (⇑(ideal.quotient.mk (ideal.span {polynomial.map (ideal.quotient.mk I) f})) (polynomial.map (ideal.quotient.mk I) p)) = ⇑(ideal.quotient.mk (ideal.map (adjoin_root.of f) I)) (⇑(adjoin_root.mk f) p)