Divisibility by an invertible ideal

An ideal of a domain which is invertible as a fractional ideal divides every principal ideal it contains, the cofactor being the integral ideal representing ⟨a⟩ * I⁻¹.

Over a Dedekind domain this is subsumed by Ideal.dvd_iff_le ("to contain is to divide"), which holds for every nonzero ideal. The statement here assumes no Dedekind hypothesis, only that the divisor is invertible, so it also applies to rings that are not integrally closed — coordinate rings of possibly singular affine curves, for instance.

Main results

• Ideal.exists_isUnit_eq_mul_of_le: an invertible ideal divides every invertible ideal it contains, over an arbitrary fraction ring.
• Ideal.exists_isUnit_span_singleton_eq_mul: the principal case, since a nonzero principal ideal is invertible.

theorem Ideal.exists_isUnit_eq_mul_of_le {R : Type u_1} [CommRing R] {K : Type u_2} [CommRing K] [Algebra R K] [IsFractionRing R K] {A I : Ideal R} (hAunit : IsUnit ↑A) (hIunit : IsUnit ↑I) (hle : A ≤ I) : ∃ (J : Ideal R), IsUnit ↑J ∧ A = I * J

An invertible ideal divides every invertible ideal it contains. If A ≤ I are ideals whose images in the fractional ideals are units, then A = I * J for an invertible J, namely the integral ideal representing A * I⁻¹. (Such a J is automatically nonzero whenever the fractional ideals are nontrivial; see exists_isUnit_span_singleton_eq_mul.)

theorem Ideal.exists_isUnit_span_singleton_eq_mul {R : Type u_3} [CommRing R] {K : Type u_4} [Field K] [Algebra R K] [IsFractionRing R K] (I : Ideal R) (hIunit : IsUnit ↑I) {a : R} (ha : a ≠ 0) (ha_mem : a ∈ I) : ∃ (J : Ideal R), IsUnit ↑J ∧ J ≠ ⊥ ∧ span {a} = I * J

An invertible ideal divides every principal ideal it contains, a nonzero principal ideal being invertible.