# Documentation

Mathlib.RingTheory.Ideal.Prod

# Ideals in product rings #

For commutative rings R and S and ideals I ≤ R, J ≤ S, we define Ideal.prod I J as the product I × J, viewed as an ideal of R × S. In ideal_prod_eq we show that every ideal of R × S is of this form. Furthermore, we show that every prime ideal of R × S is of the form p × S or R × p, where p is a prime ideal.

def Ideal.prod {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) :
Ideal (R × S)

I × J as an ideal of R × S.

Instances For
@[simp]
theorem Ideal.mem_prod {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) {r : R} {s : S} :
(r, s) r I s J
@[simp]
theorem Ideal.prod_top_top {R : Type u} {S : Type v} [Ring R] [Ring S] :
theorem Ideal.ideal_prod_eq {R : Type u} {S : Type v} [Ring R] [Ring S] (I : Ideal (R × S)) :

Every ideal of the product ring is of the form I × J, where I and J can be explicitly given as the image under the projection maps.

@[simp]
theorem Ideal.map_fst_prod {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) :
Ideal.map () () = I
@[simp]
theorem Ideal.map_snd_prod {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) :
Ideal.map () () = J
@[simp]
theorem Ideal.map_prodComm_prod {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) :
Ideal.map (RingEquiv.prodComm) () =
def Ideal.idealProdEquiv {R : Type u} {S : Type v} [Ring R] [Ring S] :
Ideal (R × S) ×

Ideals of R × S are in one-to-one correspondence with pairs of ideals of R and ideals of S.

Instances For
@[simp]
theorem Ideal.idealProdEquiv_symm_apply {R : Type u} {S : Type v} [Ring R] [Ring S] (I : ) (J : ) :
Ideal.idealProdEquiv.symm (I, J) =
theorem Ideal.prod.ext_iff {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } {I' : } {J : } {J' : } :
= Ideal.prod I' J' I = I' J = J'
theorem Ideal.isPrime_of_isPrime_prod_top {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } (h : ) :
theorem Ideal.isPrime_of_isPrime_prod_top' {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } (h : ) :
theorem Ideal.isPrime_ideal_prod_top {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } [h : ] :
theorem Ideal.isPrime_ideal_prod_top' {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } [h : ] :
theorem Ideal.ideal_prod_prime_aux {R : Type u} {S : Type v} [Ring R] [Ring S] {I : } {J : } :
Ideal.IsPrime ()I = J =
theorem Ideal.ideal_prod_prime {R : Type u} {S : Type v} [Ring R] [Ring S] (I : Ideal (R × S)) :
(p, I = ) p, I =

Classification of prime ideals in product rings: the prime ideals of R × S are precisely the ideals of the form p × S or R × p, where p is a prime ideal of R or S.