Extension and contraction away from an ideal contained in a subring

Let S be a subring of a commutative ring R, and let C be an ideal of R contained in S. Extension and contraction are inverse for ideals coprime to C, and the inclusion induces isomorphisms of their quotient rings. In particular, extension preserves primality on this restricted family. Taking C to be the conductor compares ideals and residue rings of an order with those of its normalization. That an ideal is coprime to C exactly when its contraction is coprime to the contraction of C holds more generally in any ring.

The argument generalizes the monogenic conductor calculation in Mathlib's comap_map_eq_map_adjoin_of_coprime_conductor and quotAdjoinEquivQuotMap to arbitrary subrings. No integrality or finiteness assumption is needed.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §12.
• G. S. Kopp and J. C. Lagarias, Class Field Theory for Orders of Number Fields, §2.

theorem TauCeti.comap_sup_comap_eq_top_iff {R : Type u_1} [Ring R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {J : Ideal R} : Ideal.comap S.subtype J ⊔ Ideal.comap S.subtype C = ⊤ ↔ J ⊔ C = ⊤

An ideal is coprime to an ideal contained in the subring if and only if their contractions are coprime.

theorem TauCeti.mul_mem_image_of_mem_map_of_le {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {I : Ideal ↥S} {c : R} (hc : c ∈ C) {x : R} (hx : x ∈ Ideal.map S.subtype I) : c * x ∈ ⇑S.subtype '' ↑I

Multiplying an element of an extended ideal by an element of an ideal contained in the subring lands in the image of the original ideal.

theorem TauCeti.comap_map_of_coprime_comap {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {I : Ideal ↥S} (hI : I ⊔ Ideal.comap S.subtype C = ⊤) : Ideal.comap S.subtype (Ideal.map S.subtype I) = I

Contracting an extended ideal recovers it when it is coprime to the contraction of an ambient ideal contained in the subring.

theorem TauCeti.map_comap_of_coprime {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {J : Ideal R} (hJ : J ⊔ C = ⊤) : Ideal.map S.subtype (Ideal.comap S.subtype J) = J

Extending a contracted ideal recovers it when it is coprime to an ideal contained in the subring.

theorem TauCeti.surjective_quotient_mk_comp_of_coprime {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {J : Ideal R} (hJ : J ⊔ C = ⊤) : Function.Surjective ⇑((Ideal.Quotient.mk J).comp S.subtype)

Every residue class modulo an ideal coprime to an ideal contained in the subring has a representative in the subring.

noncomputable def TauCeti.quotientComapEquivOfCoprime {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {J : Ideal R} (hJ : J ⊔ C = ⊤) : ↥S ⧸ Ideal.comap S.subtype J ≃+* R ⧸ J

Inclusion induces an isomorphism on quotient rings for an ideal coprime to an ideal contained in the subring.

@[simp]

theorem TauCeti.quotientComapEquivOfCoprime_apply_mk {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {J : Ideal R} (hJ : J ⊔ C = ⊤) (x : ↥S) : (quotientComapEquivOfCoprime hC hJ) ((Ideal.Quotient.mk (Ideal.comap S.subtype J)) x) = (Ideal.Quotient.mk J) ↑x

The quotient-ring equivalence sends the residue class of a subring element to the residue class of the same element in the ambient ring.

theorem TauCeti.isPrime_map_iff_of_coprime_comap {R : Type u_1} [CommRing R] {S : Subring R} {C : Ideal R} (hC : ↑C ⊆ ↑S) {I : Ideal ↥S} (hI : I ⊔ Ideal.comap S.subtype C = ⊤) : (Ideal.map S.subtype I).IsPrime ↔ I.IsPrime

Extension preserves and reflects primality for ideals coprime to the contraction of an ambient ideal contained in the subring.