Ideal intersections and saturations by adjoining a variable

For ideals I and J of a commutative ring, their intersection is the contraction along Polynomial.C of X * I + (1 - X) * J. Here multiplication by a polynomial means multiplication by its principal ideal, and the ideals of coefficients are extended to the polynomial ring. The generator version makes this a reduction of intersection to elimination.

The saturation of an ideal I by an element r, the set of x with r ^ n * x ∈ I for some n, is the contraction along Polynomial.C of I[X] + (r X - 1). Since R[X] ⧸ (r X - 1) is the localization of R away from r (Localization.awayEquivAdjoin), this is the contraction of I from that localization, so saturation is also reduced to elimination.

No field or Noetherian hypothesis is needed.

Multiplication by c X - 1 on B[X] is injective, since its constant coefficient is a unit (Polynomial.mulLeft_C_mul_X_sub_one_injective).

Finally, Ideal.exists_poly_isRoot_mk_of_pow_four_dvd_cubic bounds the residues modulo a nonzero nonunit ϖ of the solutions of a cubic congruence modulo ϖ ^ 4 of the form (ϖ t)³ + a₂ (ϖ t)² + a₄ (ϖ t) + a₆ by the roots of a nonzero polynomial of degree at most 3.

References

• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, Chapter 4, §3, the added-variable construction for intersections of ideals, and Chapter 4, §4, the added-variable construction for saturations.

theorem Ideal.inf_eq_comap_C {R : Type u_1} [CommRing R] (I J : Ideal R) : I ⊓ J = comap Polynomial.C (span {Polynomial.X} * map Polynomial.C I ⊔ span {1 - Polynomial.X} * map Polynomial.C J)

The intersection of two ideals is obtained by eliminating the new variable from X * I + (1 - X) * J.

theorem Ideal.span_inf_span_eq_comap_C {R : Type u_1} [CommRing R] (s t : Set R) : span s ⊓ span t = comap Polynomial.C (span ((fun (f : R) => Polynomial.X * Polynomial.C f) '' s ∪ (fun (g : R) => (1 - Polynomial.X) * Polynomial.C g) '' t))

For chosen generating sets of two ideals, the added-variable intersection ideal is explicitly generated by X * C f and (1 - X) * C g.

theorem Ideal.mem_comap_C_map_C_sup_span_C_mul_X_sub_one_iff {R : Type u_1} [CommRing R] {I : Ideal R} {r x : R} : x ∈ comap Polynomial.C (map Polynomial.C I ⊔ span {Polynomial.C r * Polynomial.X - 1}) ↔ ∃ (n : ℕ), r ^ n * x ∈ I

Saturation by an added variable. An element x lies in the contraction along C of I[X] + (r X - 1) if and only if some power of r multiplies it into I.

theorem Ideal.comap_C_map_C_sup_span_C_mul_X_sub_one {R : Type u_1} [CommRing R] (I : Ideal R) (r : R) (S : Type u_2) [CommSemiring S] [Algebra R S] [IsLocalization.Away r S] : comap Polynomial.C (map Polynomial.C I ⊔ span {Polynomial.C r * Polynomial.X - 1}) = comap (algebraMap R S) (map (algebraMap R S) I)

The contraction along C of I[X] + (r X - 1) is the contraction of I from the localization S of R away from r.

theorem Ideal.ne_zero_of_coeff_mk_of_not_dvd {R : Type u_1} [CommRing R] {ϖ u : R} (hu : ¬ϖ ∣ u) (p : Polynomial (R ⧸ span {ϖ})) (n : ℕ) (h : p.coeff n = (Quotient.mk (span {ϖ})) u) : p ≠ 0

A polynomial over R ⧸ (ϖ) with a coefficient the residue of an element not divisible by ϖ is nonzero.

theorem Ideal.exists_poly_isRoot_mk_of_pow_four_dvd_cubic {R : Type u_1} [CommRing R] [IsDomain R] {ϖ : R} (hϖ0 : ϖ ≠ 0) (hϖ : ¬IsUnit ϖ) (a₂ a₄ a₆ : R) : ∃ (p : Polynomial (R ⧸ span {ϖ})), p ≠ 0 ∧ p.natDegree ≤ 3 ∧ ∀ (t : R), ϖ ^ 4 ∣ (ϖ * t) ^ 3 + a₂ * (ϖ * t) ^ 2 + a₄ * (ϖ * t) + a₆ → p.IsRoot ((Quotient.mk (span {ϖ})) t)

Over an integral domain R with a nonzero nonunit ϖ, the residues t modulo ϖ for which ϖ ^ 4 divides (ϖ t)³ + a₂ (ϖ t)² + a₄ (ϖ t) + a₆ are among the roots of a nonzero polynomial of degree at most 3 over R ⧸ (ϖ).

theorem Polynomial.mulLeft_C_mul_X_sub_one_injective (R : Type u_1) [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (c : B) : Function.Injective ⇑(LinearMap.mulLeft R (C c * X - 1))

Multiplication by c X - 1 on B[X] is injective: its constant coefficient -1 is a unit, so it is a non-zero-divisor.