Elements coprime to an ideal with finite quotient

Let C be an ideal of a commutative ring R with finite quotient R ⧸ C. An element x with (x) + C = R is a unit modulo C, and the unit group of the finite ring R ⧸ C is finite, so some positive power of x is congruent to 1 modulo C.

Consequently coprimality to C descends along any ring homomorphism f : S →+* R: if f x is coprime to C, then x is coprime to the contraction C.comap f, since the inverse of x modulo C.comap f can be taken to be a power of x itself. For an order O in a number field and its conductor 𝔣, this says that an element of O coprime to 𝔣 in the maximal order is already coprime to 𝔣 in O.

Main results

• Ideal.Quotient.isUnit_mk_iff: the class of x is a unit modulo C exactly when (x) + C = R; no finiteness is needed here.
• Ideal.exists_pow_sub_one_mem_of_sup_eq_top: an element coprime to an ideal with finite quotient has a positive power congruent to 1.
• Ideal.span_singleton_sup_comap_eq_top: coprimality to an ideal with finite quotient descends along a ring homomorphism.

theorem Ideal.Quotient.isUnit_mk_iff {R : Type u_1} [CommRing R] {C : Ideal R} {x : R} : IsUnit ((mk C) x) ↔ span {x} ⊔ C = ⊤

The class of x is a unit of R ⧸ C exactly when x is coprime to C.

theorem Ideal.exists_pow_sub_one_mem_of_sup_eq_top {R : Type u_1} [CommRing R] {C : Ideal R} [Finite (R ⧸ C)] {x : R} (hx : span {x} ⊔ C = ⊤) : ∃ (n : ℕ), 0 < n ∧ x ^ n - 1 ∈ C

An element coprime to an ideal C with finite quotient ring has a positive power congruent to 1 modulo C.

theorem Ideal.span_singleton_sup_comap_eq_top {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {C : Ideal R} [Finite (R ⧸ C)] (f : S →+* R) {x : S} (hx : span {f x} ⊔ C = ⊤) : span {x} ⊔ comap f C = ⊤

Coprimality descends along a ring homomorphism to an ideal with finite quotient. If f x is coprime to an ideal C with finite quotient ring, then x is coprime to C.comap f.