Coprime representatives of invertible ideal classes

Let R be a domain, 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 class of invertible ideals of R is then represented by an integral ideal coprime to 𝔞. This is the class-group form of FractionalIdeal.exists_coeIdeal_eq_spanSingleton_mul_and_sup_eq_top.

No Dedekind hypothesis is made. The motivating case is a non-maximal order O in a number field and the conductor of O, where the result says that the Picard group of O is generated by ideals coprime to the conductor. Those are the ideals that extension and contraction match with ideals of the maximal order.

Main results

• ClassGroup.exists_mk_eq_and_sup_eq_top: every class of invertible ideals is the class of an invertible 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 ClassGroup.exists_mk_eq_and_sup_eq_top {R : Type u_1} {K : Type u_2} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] {𝔞 : Ideal R} (h𝔞 : {P : Ideal R | P.IsMaximal ∧ 𝔞 ≤ P}.Finite) (c : ClassGroup R) : ∃ (I : Ideal R) (hI : IsUnit ↑I), (mk K) hI.unit = c ∧ I ⊔ 𝔞 = ⊤

Coprime representatives of ideal classes. If an ideal 𝔞 of a domain R lies in only finitely many maximal ideals, then every class of invertible ideals of R is the class of an invertible integral ideal coprime to 𝔞.