Coprime integral multiples of invertible fractional ideals

Let R be a nontrivial commutative ring with total fraction ring K, and let 𝔞 be an ideal of R contained in only finitely many maximal ideals, for instance an ideal with finite quotient ring (Ideal.finite_setOfPred_isMaximal_and_le). Every invertible fractional ideal J of R then has a nonzero multiple a J which is an integral ideal of R coprime to 𝔞.

No domain or Dedekind hypothesis is made, and non-invertible ideals play no role. The motivating case is a non-maximal order O in a number field and the conductor of O.

The element a is built by the Chinese remainder theorem. At each maximal ideal P ⊇ 𝔞, the equation J⁻¹ J = R provides y_P ∈ J⁻¹ and x_P ∈ J with y_P x_P ∉ P. Choosing e_P ∈ R congruent to 1 modulo P and to 0 modulo the other maximal ideals containing 𝔞, the element a = ∑ e_P y_P of J⁻¹ satisfies a x_P ≡ y_P x_P modulo P, so a J lies in none of them.

Main results

• FractionalIdeal.exists_mem_inv_exists_mem_mul_notMem: for an invertible fractional ideal J and a proper ideal P, some product y * x with y ∈ J⁻¹, x ∈ J is an element of R outside P.
• FractionalIdeal.exists_coeIdeal_eq_spanSingleton_mul_and_sup_eq_top: an invertible fractional ideal has a nonzero multiple which is an integral ideal coprime to 𝔞.

References

• D. A. Cox, Primes of the Form x² + ny², §7, Corollary 7.17 (orders in quadratic fields).
• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.

theorem FractionalIdeal.exists_mem_inv_exists_mem_mul_notMem {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ) {P : Ideal R} (hP : P ≠ ⊤) : ∃ y ∈ ↑J⁻¹, ∃ x ∈ ↑J, ∃ (r : R), (algebraMap R K) r = y * x ∧ r ∉ P

For an invertible fractional ideal J, some product y * x with y ∈ J⁻¹ and x ∈ J is an element of R outside a given proper ideal P.

theorem FractionalIdeal.exists_coeIdeal_eq_spanSingleton_mul_and_sup_eq_top {R : Type u_1} {K : Type u_2} [CommRing R] [CommRing K] [Algebra R K] [IsFractionRing R K] [Nontrivial R] (J : (FractionalIdeal (nonZeroDivisors R) K)ˣ) {𝔞 : Ideal R} (h𝔞 : {P : Ideal R | P.IsMaximal ∧ 𝔞 ≤ P}.Finite) : ∃ (a : K), a ≠ 0 ∧ ∃ (I : Ideal R), ↑I = (spanSingleton (nonZeroDivisors R)) a * ↑J ∧ I ⊔ 𝔞 = ⊤

Coprime representatives. Let J be an invertible fractional ideal of a nontrivial ring R, and let 𝔞 be an ideal of R contained in only finitely many maximal ideals. Then J has a nonzero multiple a J which is an integral ideal of R coprime to 𝔞.