The elements of one ideal congruent to one modulo another

For ideals I and J of a commutative ring, the elements of I congruent to 1 modulo J form a coset of I ⊓ J inside I, translated by any one of them. Such an element exists exactly when I and J are coprime, and coprimality also turns I ⊓ J into I * J.

This is the shape a counting argument wants: the set is a translate of a fixed subgroup, so it can be enumerated by translating that subgroup once.

Main results

• Ideal.isCoprime_iff_exists_mem_and_sub_one_mem: the set is nonempty exactly when I and J are coprime;
• Ideal.setOf_mem_and_sub_one_mem_eq_vadd_inf: the set is a coset of I ⊓ J;
• Ideal.setOf_mem_and_sub_one_mem_eq_vadd_mul: the same coset written over I * J.

theorem Ideal.setOf_mem_and_sub_one_mem_eq_vadd_inf {R : Type u_1} [Ring R] {I J : Ideal R} {ξ : R} (hξI : ξ ∈ I) (hξJ : ξ - 1 ∈ J) : {x : R | x ∈ I ∧ x - 1 ∈ J} = ξ +ᵥ ↑(I ⊓ J)

The set is a coset of I ⊓ J. The elements of I congruent to 1 modulo J are a translate of I ⊓ J by any one of them. Only the additive structure of the ideals is used.

theorem Ideal.isCoprime_iff_exists_mem_and_sub_one_mem {R : Type u_1} [CommRing R] {I J : Ideal R} : IsCoprime I J ↔ ∃ x ∈ I, x - 1 ∈ J

Coprimality is the existence of an element of I congruent to one modulo J. Writing 1 as a sum of an element of each ideal is the same data as such an element.

theorem Ideal.setOf_mem_and_sub_one_mem_eq_vadd_mul {R : Type u_1} [CommRing R] {I J : Ideal R} {ξ : R} (hξI : ξ ∈ I) (hξJ : ξ - 1 ∈ J) : {x : R | x ∈ I ∧ x - 1 ∈ J} = ξ +ᵥ ↑(I * J)

The set is a coset of I * J. The elements of I congruent to 1 modulo J are a translate of I * J by any one of them.