mathlib documentation

ring_theory.polynomial.quotient

Quotients of polynomial rings #

source
noncomputable def polynomial.quotient_span_X_sub_C_alg_equiv {R : Type u_1} [comm_ring R] (x : R) :
(polynomial R ⧸ ideal.span {polynomial.X - ⇑polynomial.C x}) ≃ₐ[R] R

For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$.

Equations
source
@[simp]
theorem polynomial.quotient_span_X_sub_C_alg_equiv_mk {R : Type u_1} [comm_ring R] (x : R) (p : polynomial R) :
⇑(polynomial.quotient_span_X_sub_C_alg_equiv x) (⇑(ideal.quotient.mk (ideal.span {polynomial.X - ⇑polynomial.C x})) p) = polynomial.eval x p
source
@[simp]
theorem polynomial.quotient_span_X_sub_C_alg_equiv_symm_apply {R : Type u_1} [comm_ring R] (x y : R) :
⇑((polynomial.quotient_span_X_sub_C_alg_equiv x).symm) y = ⇑(algebra_map R (polynomial R ⧸ ideal.span {polynomial.X - ⇑polynomial.C x})) y
source
theorem ideal.quotient_map_C_eq_zero {R : Type u_1} [comm_ring R] {I : ideal R} (a : R) (H : a ∈ I) :
⇑((ideal.quotient.mk (ideal.map polynomial.C I)).comp polynomial.C) a = 0
source
theorem ideal.eval₂_C_mk_eq_zero {R : Type u_1} [comm_ring R] {I : ideal R} (f : polynomial R) (H : f ∈ ideal.map polynomial.C I) :
⇑(polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) f = 0
source
noncomputable def ideal.polynomial_quotient_equiv_quotient_polynomial {R : Type u_1} [comm_ring R] (I : ideal R) :
polynomial (R ⧸ I) ≃+* polynomial R ⧸ ideal.map polynomial.C I

If I is an ideal of R, then the ring polynomials over the quotient ring I.quotient is isomorphic to the quotient of R[X] by the ideal map C I, where map C I contains exactly the polynomials whose coefficients all lie in I

Equations
source
@[simp]
theorem ideal.polynomial_quotient_equiv_quotient_polynomial_symm_mk {R : Type u_1} [comm_ring R] (I : ideal R) (f : polynomial R) :
⇑(I.polynomial_quotient_equiv_quotient_polynomial.symm) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f) = polynomial.map (ideal.quotient.mk I) f
source
@[simp]
theorem ideal.polynomial_quotient_equiv_quotient_polynomial_map_mk {R : Type u_1} [comm_ring R] (I : ideal R) (f : polynomial R) :
⇑(I.polynomial_quotient_equiv_quotient_polynomial) (polynomial.map (ideal.quotient.mk I) f) = ⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f
source
theorem ideal.is_domain_map_C_quotient {R : Type u_1} [comm_ring R] {P : ideal R} (H : P.is_prime) :
is_domain (polynomial R ⧸ ideal.map polynomial.C P)

If P is a prime ideal of R, then R[x]/(P) is an integral domain.

source
theorem ideal.eq_zero_of_polynomial_mem_map_range {R : Type u_1} [comm_ring R] (I : ideal (polynomial R)) (x : ↥(((ideal.quotient.mk I).comp polynomial.C).range)) (hx : ⇑polynomial.C x ∈ ideal.map (polynomial.map_ring_hom ((ideal.quotient.mk I).comp polynomial.C).range_restrict) I) :
x = 0

Given any ring R and an ideal I of R[X], we get a map R → R[x] → R[x]/I. If we let R be the image of R in R[x]/I then we also have a map R[x] → R'[x]. In particular we can map I across this map, to get I' and a new map R' → R'[x] → R'[x]/I. This theorem shows I' will not contain any non-zero constant polynomials

source
theorem mv_polynomial.quotient_map_C_eq_zero {R : Type u_1} {σ : Type u_2} [comm_ring R] {I : ideal R} {i : R} (hi : i ∈ I) :
⇑((ideal.quotient.mk (ideal.map mv_polynomial.C I)).comp mv_polynomial.C) i = 0
source
theorem mv_polynomial.eval₂_C_mk_eq_zero {R : Type u_1} {σ : Type u_2} [comm_ring R] {I : ideal R} {a : mv_polynomial σ R} (ha : a ∈ ideal.map mv_polynomial.C I) :
⇑(mv_polynomial.eval₂_hom (mv_polynomial.C.comp (ideal.quotient.mk I)) mv_polynomial.X) a = 0
source
noncomputable def mv_polynomial.quotient_equiv_quotient_mv_polynomial {R : Type u_1} {σ : Type u_2} [comm_ring R] (I : ideal R) :
mv_polynomial σ (R ⧸ I) ≃ₐ[R] mv_polynomial σ R ⧸ ideal.map mv_polynomial.C I

If I is an ideal of R, then the ring mv_polynomial σ I.quotient is isomorphic as an R-algebra to the quotient of mv_polynomial σ R by the ideal generated by I.

Equations