ring_theory.adjoin_root

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

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

adjoin_root f = (R[X] ⧸ ideal.span {f})

source

@[protected, instance]

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

comm_ring (adjoin_root f)

Equations

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

source

@[protected, instance]

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

inhabited (adjoin_root f)

Equations

adjoin_root.inhabited f = {default := 0}

source

@[protected, instance]

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

decidable_eq (adjoin_root f)

Equations

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

source

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

R[X] →+* 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 : R[X]) {C : adjoin_root f → Prop} (x : adjoin_root f) (ih : ∀ (p : R[X]), C (⇑(adjoin_root.mk f) p)) :

C x

source

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

R →+* adjoin_root f

Embedding of the original ring R into adjoin_root f.

Equations

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

source

@[protected, instance]

noncomputable def adjoin_root.algebra {R : Type u} {S : Type v} [comm_ring R] (f : R[X]) [comm_semiring S] [algebra S R] :

algebra S (adjoin_root f)

Equations

adjoin_root.algebra f = ideal.quotient.algebra S

source

@[protected, instance]

def adjoin_root.is_scalar_tower {R : Type u} {S : Type v} {K : Type w} [comm_ring R] (f : R[X]) [comm_semiring S] [comm_semiring K] [has_scalar 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 : R[X]) [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 : R[X]) :

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 : R[X]) [comm_semiring S] [algebra S R] :

algebra_map S (adjoin_root f) = (adjoin_root.of f).comp (algebra_map S R)

source

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

adjoin_root f

The adjoined root.

Equations

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

source

@[protected, instance]

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

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_eq_mk {R : Type u} [comm_ring R] {f g h : R[X]} :

⇑(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 : R[X]} :

⇑(adjoin_root.mk f) f = 0

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

⇑(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 : R[X]} :

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

source

@[simp]

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

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 : R[X]) :

(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 : R[X]} (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 : R[X]} [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

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 : R[X]} [comm_ring S] {i : R →+* S} {a : S} (h : polynomial.eval₂ i a f = 0) (g : R[X]) :

⇑(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 : R[X]} [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 : R[X]} [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 : R[X]} [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 : R[X]) [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

adjoin_root.lift_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_lift_hom {R : Type u} {S : Type v} [comm_ring R] (f : R[X]) [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 : R[X]) [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 : R[X]) (ϕ : 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 : R[X]) [comm_ring S] {a : S} [algebra R S] (hfx : ⇑(polynomial.aeval a) f = 0) {g : R[X]} :

⇑(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 : R[X]) [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 : R[X]) [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

@[protected, instance]

def adjoin_root.is_maximal_span {K : Type w} [field K] {f : K[X]} [irreducible f] :

(ideal.span {f}).is_maximal

source

@[protected, instance]

noncomputable def adjoin_root.field {K : Type w} [field K] {f : K[X]} [irreducible f] :

field (adjoin_root f)

Equations

adjoin_root.field = {add := comm_ring.add (adjoin_root.comm_ring f), add_assoc := _, zero := comm_ring.zero (adjoin_root.comm_ring f), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (adjoin_root.comm_ring f), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (adjoin_root.comm_ring f), sub := comm_ring.sub (adjoin_root.comm_ring f), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (adjoin_root.comm_ring f), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul (adjoin_root.comm_ring f), mul_assoc := _, one := comm_ring.one (adjoin_root.comm_ring f), one_mul := _, mul_one := _, npow := comm_ring.npow (adjoin_root.comm_ring f), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv (ideal.quotient.field (ideal.span {f})), div := field.div (ideal.quotient.field (ideal.span {f})), div_eq_mul_inv := _, zpow := field.zpow (ideal.quotient.field (ideal.span {f})), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

theorem adjoin_root.coe_injective {K : Type w} [field K] {f : K[X]} [irreducible f] :

function.injective coe

source

theorem adjoin_root.mul_div_root_cancel {K : Type w} [field K] (f : K[X]) [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

theorem adjoin_root.is_integral_root' {R : Type u} [comm_ring R] {g : R[X]} (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 : R[X]} (hg : g.monic) :

adjoin_root g →ₗ[R] R[X]

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

adjoin_root.mod_by_monic_hom hg = ((submodule.restrict_scalars R (ideal.span {g})).liftq g.mod_by_monic_hom _).comp (submodule.quotient.restrict_scalars_equiv R (ideal.span {g})).symm.to_linear_map

source

@[simp]

theorem adjoin_root.mod_by_monic_hom_mk {R : Type u} [comm_ring R] {g : R[X]} (hg : g.monic) (f : R[X]) :

⇑(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 : R[X]} (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 : R[X]} (hg : g.monic) :

function.surjective ⇑(adjoin_root.mk g)

source

noncomputable def adjoin_root.power_basis_aux' {R : Type u} [comm_ring R] {g : R[X]} (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

adjoin_root.power_basis_aux' hg = basis.of_equiv_fun {to_fun := λ (f : adjoin_root g) (i : fin g.nat_degree), (⇑(adjoin_root.mod_by_monic_hom hg) f).coeff ↑i, map_add' := _, map_smul' := _, inv_fun := λ (c : fin g.nat_degree → R), ⇑(adjoin_root.mk g) (∑ (i : fin g.nat_degree), ⇑(polynomial.monomial ↑i) (c i)), left_inv := _, right_inv := _}

source

@[simp]

theorem adjoin_root.power_basis_aux'_repr_symm_apply {R : Type u} [comm_ring R] {g : R[X]} (hg : g.monic) (ᾰ : fin g.nat_degree →₀ R) :

⇑((adjoin_root.power_basis_aux' hg).repr.symm) ᾰ = ⇑(adjoin_root.mk g) (∑ (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 : R[X]} (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 : R[X]} (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 : R[X]} (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 : R[X]} (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

adjoin_root.power_basis' hg = {gen := adjoin_root.root g, dim := g.nat_degree, basis := adjoin_root.power_basis_aux' hg, basis_eq_pow := _}

source

@[simp]

theorem adjoin_root.power_basis'_gen {R : Type u} [comm_ring R] {g : R[X]} (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 : K[X]} (hf : f ≠ 0) :

is_integral K (adjoin_root.root f)

source

theorem adjoin_root.minpoly_root {K : Type w} [field K] {f : K[X]} (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 : K[X]} (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

adjoin_root.power_basis_aux hf = let f' : K[X] := f * ⇑polynomial.C (f.leading_coeff)⁻¹ in basis.mk _ _

source

@[simp]

theorem adjoin_root.power_basis_gen {K : Type w} [field K] {f : K[X]} (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 : K[X]} (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

adjoin_root.power_basis hf = {gen := adjoin_root.root f, dim := f.nat_degree, basis := adjoin_root.power_basis_aux hf, basis_eq_pow := _}

source

@[simp]

theorem adjoin_root.power_basis_dim {K : Type w} [field K] {f : K[X]} (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 : K[X]} (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 : K[X]} (hf : f.monic) (hf' : f ≠ 0 := _) :

minpoly K (adjoin_root.power_basis hf').gen = f

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 : R[X]) (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 : R[X]) (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

adjoin_root.equiv' g pb h₁ h₂ = {to_fun := ⇑(adjoin_root.lift_hom g pb.gen h₂), inv_fun := ⇑(pb.lift (adjoin_root.root g) h₁), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

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 : R[X]) (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 : R[X]) (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 : R[X]) (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 : F[X]) (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

adjoin_root.equiv L F f hf = (adjoin_root.power_basis hf).lift_equiv'.trans ((equiv.refl L).subtype_equiv _)

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 : R[X]) :

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

adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f = ideal.quot_equiv_of_eq _

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 : R[X]) (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

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 : R[X]) :

adjoin_root f ⧸ ideal.map (ideal.quotient.mk (ideal.span {f})) (ideal.map polynomial.C I) ≃+* (R[X] ⧸ 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

adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f = double_quot.quot_quot_equiv_comm (ideal.span {f}) (ideal.map polynomial.C I)

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 : R[X]) :

⇑(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

noncomputable def adjoin_root.polynomial.quot_quot_equiv_comm {R : Type u} [comm_ring R] (I : ideal R) (f : R[X]) :

(R ⧸ I)[X] ⧸ ideal.span {polynomial.map (ideal.quotient.mk I) f} ≃+* (R[X] ⧸ 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

adjoin_root.polynomial.quot_quot_equiv_comm I f = (ideal.span {polynomial.map (ideal.quotient.mk I) f}).quotient_equiv (ideal.span {⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f}) I.polynomial_quotient_equiv_quotient_polynomial _

source

@[simp]

theorem adjoin_root.polynomial.quot_quot_equiv_comm_mk_mk {R : Type u} [comm_ring R] (I : ideal R) (f p : R[X]) :

⇑((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_map_of_equiv {R : Type u} [comm_ring R] (I : ideal R) (f : R[X]) :

adjoin_root f ⧸ ideal.map (adjoin_root.of f) I ≃+* (R ⧸ I)[X] ⧸ 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

adjoin_root.quot_map_of_equiv I f = (adjoin_root.quot_map_of_equiv_quot_map_C_map_span_mk I f).trans ((adjoin_root.quot_map_C_map_span_mk_equiv_quot_map_C_quot_map_span_mk I f).trans ((ideal.quot_equiv_of_eq _).trans (adjoin_root.polynomial.quot_quot_equiv_comm I f).symm))

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 : R[X]) :

⇑(adjoin_root.quot_map_of_equiv 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)

mathlib documentation

Adjoining roots of polynomials #

Main definitions and results #