Ideal.isDomain_map_C_quotient
theorem Ideal.isDomain_map_C_quotient :
∀ {R : Type u_1} [inst : CommRing R] {P : Ideal R},
P.IsPrime → IsDomain (Polynomial R ⧸ Ideal.map Polynomial.C P)
This theorem states that if `P` is a prime ideal in a commutative ring `R`, then the quotient ring of the ring of polynomials over `R` by the ideal generated by the image of `P` under the constant polynomial function is an integral domain. In simpler terms, prime ideals in a commutative ring `R` correspond to the creation of integral domains when considering the polynomial version of the ring modulo the image of the prime ideal under the constant polynomial function.
More concisely: If `P` is a prime ideal in a commutative ring `R`, then the quotient ring of the polynomial ring over `R` by the ideal generated by the image of `P` under the constant polynomial function is an integral domain.
|
MvPolynomial.quotient_map_C_eq_zero
theorem MvPolynomial.quotient_map_C_eq_zero :
∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] {I : Ideal R} {i : R},
i ∈ I → ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) i = 0
The theorem `MvPolynomial.quotient_map_C_eq_zero` states that for any commutative ring `R`, any ideal `I` of `R`, any multivariate polynomial `σ`, and any element `i` of `R` that lies in `I`, the composition of the ring homomorphism from `R` to the quotient ring `R/I` and the constant polynomial function `MvPolynomial.C` evaluated at `i` is zero. In other words, if a constant `i` from a ring `R` is in an ideal `I`, then mapping `i` into the multivariate polynomial ring over `R` and then further mapping into the quotient ring `R/I` results in zero.
More concisely: For any commutative ring R, ideal I, multivariate polynomial σ, and element i in I, the constant polynomial function evaluated at i in the quotient ring R/I is zero (i.e., MvPolynomial.C(i) = 0).
|
Ideal.eq_zero_of_polynomial_mem_map_range
theorem Ideal.eq_zero_of_polynomial_mem_map_range :
∀ {R : Type u_1} [inst : CommRing R] (I : Ideal (Polynomial R))
(x : ↥((Ideal.Quotient.mk I).comp Polynomial.C).range),
Polynomial.C x ∈ Ideal.map (Polynomial.mapRingHom ((Ideal.Quotient.mk I).comp Polynomial.C).rangeRestrict) I →
x = 0
This theorem states that for any commutative ring `R` and any ideal `I` of the polynomial ring `R[X]`, we can define a series of maps from `R` to `R[X]`, then to the quotient ring `R[X]/I`. We can further define a map from `R[X]` to a new polynomial ring `R'[X]` by considering `R'` to be the image of `R` in `R[X]/I`. In turn, we can map the ideal `I` across this map, to obtain a new ideal `I'` and a new series of maps from `R'` to `R'[X]` and then to the quotient ring `R'[X]/I'`. The theorem asserts that if a constant polynomial (with coefficients from the image of `R` in `R[X]/I`) is in the ideal `I'`, then it must be the zero polynomial. In other words, this ideal `I'` does not contain any non-zero constant polynomials.
More concisely: For any commutative ring `R`, ideal `I` of `R[X]`, and the image `R'` of `R` in `R[X]/I`, the image of `I` in `R'[X]` is the ideal consisting only of the zero polynomial.
|
Polynomial.quotientSpanXSubCAlgEquivAux2.proof_2
theorem Polynomial.quotientSpanXSubCAlgEquivAux2.proof_2 :
∀ {R : Type u_1} [inst : CommRing R] (x x_1 : R), Polynomial.eval x (Polynomial.C x_1) = x_1
This theorem states that for any commutative ring `R` and any elements `x` and `x_1` from `R`, the evaluation of the constant polynomial `x_1` at `x` is equal to `x_1`. In mathematical language, if we have a constant polynomial `P(x) = x_1` then `P(x) = x_1` for all `x` in our commutative ring `R`.
More concisely: For any commutative ring `R` and elements `x, x_1` in `R`, the constant polynomial `x_1` evaluates to `x_1` at `x`.
|
MvPolynomial.quotientEquivQuotientMvPolynomial.proof_1
theorem MvPolynomial.quotientEquivQuotientMvPolynomial.proof_1 :
∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] (I : Ideal R) (r : R),
(MvPolynomial.eval₂Hom
(Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯) fun i =>
(Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)) (MvPolynomial.X i))
(MvPolynomial.C ((Ideal.Quotient.mk I) r)) =
(Ideal.Quotient.lift I ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) ⋯)
((Ideal.Quotient.mk I) r)
The theorem `MvPolynomial.quotientEquivQuotientMvPolynomial.proof_1` states that for any commutative ring `R`, type `σ`, ideal `I` of `R`, and ring element `r`, the value of the multivariate polynomial `MvPolynomial.C ((Ideal.Quotient.mk I) r)` under the evaluation map `MvPolynomial.eval₂Hom` is equal to the image of `((Ideal.Quotient.mk I) r)` under the lift of a ring homomorphism from `R` to the quotient ring `R/I`. This evaluation map is constructed with a ring homomorphism that maps an element of `R` to the constant polynomial with that element as coefficient, and a function which maps each index `i` to the degree `1` monomial in the quotient ring `R/I`. This lift of a ring homomorphism is also constructed with the same ring homomorphism as the evaluation map.
More concisely: For any commutative ring `R`, ideal `I` of `R`, and ring element `r`, the evaluation of the multivariate polynomial `MvPolynomial.C ((Ideal.Quotient.mk I) r)` under `MvPolynomial.eval₂Hom` equals the image of `((Ideal.Quotient.mk I) r)` under the homomorphism-induced evaluation homomorphism from `R` to `R/I`.
|