# mathlib3documentation

ring_theory.ideal.prod

# Ideals in product rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ideal R) (J : ideal S) :
ideal (R × S)

I × J as an ideal of R × S.

Equations
@[simp]
theorem ideal.mem_prod {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (J : ideal S) {r : R} {s : S} :
(r, s) I.prod J 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)) :
I = (ideal.map S) I).prod (ideal.map S) I)

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 : ideal R) (J : ideal S) :
ideal.map S) (I.prod J) = I
@[simp]
theorem ideal.map_snd_prod {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (J : ideal S) :
ideal.map S) (I.prod J) = J
@[simp]
theorem ideal.map_prod_comm_prod {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (J : ideal S) :
= J.prod I
def ideal.ideal_prod_equiv {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.

Equations
@[simp]
theorem ideal.ideal_prod_equiv_symm_apply {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (J : ideal S) :
theorem ideal.prod.ext_iff {R : Type u} {S : Type v} [ring R] [ring S] {I I' : ideal R} {J J' : ideal S} :
I.prod J = I'.prod J' I = I' J = J'
theorem ideal.is_prime_of_is_prime_prod_top {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal R} (h : (I.prod ).is_prime) :
theorem ideal.is_prime_of_is_prime_prod_top' {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal S} (h : (.prod I).is_prime) :
theorem ideal.is_prime_ideal_prod_top {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal R} [h : I.is_prime] :
theorem ideal.is_prime_ideal_prod_top' {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal S} [h : I.is_prime] :
theorem ideal.ideal_prod_prime_aux {R : Type u} {S : Type v} [ring R] [ring S] {I : ideal R} {J : ideal S} :
theorem ideal.ideal_prod_prime {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal (R × S)) :
I.is_prime ( (p : ideal R), p.is_prime I = p.prod ) (p : ideal S), p.is_prime I = .prod p

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.