mathlib documentation

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

ideal (R × S)

I × J as an ideal of R × S.

Equations

I.prod J = {carrier := {x : R × S | x.fst ∈ I ∧ x.snd ∈ J}, add_mem' := _, zero_mem' := _, smul_mem' := _}

@[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] :

⊤.prod ⊤ = ⊤

theorem ideal.ideal_prod_eq {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal (R × S)) :

I = (ideal.map (ring_hom.fst R S) I).prod (ideal.map (ring_hom.snd R 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 (ring_hom.fst R 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 (ring_hom.snd R 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) :

ideal.map ↑ring_equiv.prod_comm (I.prod J) = J.prod I

def ideal.ideal_prod_equiv {R : Type u} {S : Type v} [ring R] [ring S] :

ideal (R × S) ≃ ideal R × ideal S

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

Equations

ideal.ideal_prod_equiv = {to_fun := λ (I : ideal (R × S)), (ideal.map (ring_hom.fst R S) I, ideal.map (ring_hom.snd R S) I), inv_fun := λ (I : ideal R × ideal S), I.fst.prod I.snd, left_inv := _, right_inv := _}

@[simp]

theorem ideal.ideal_prod_equiv_symm_apply {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (J : ideal S) :

⇑(ideal.ideal_prod_equiv.symm) (I, J) = I.prod J

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] :

(I.prod ⊤).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] :

(⊤.prod 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} :

(I.prod J).is_prime → I = ⊤ ∨ J = ⊤

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.

noncomputable def ideal.prime_ideals_equiv (R : Type u) (S : Type v) [ring R] [ring S] :

{K // K.is_prime} ≃ {I // I.is_prime} ⊕ {J // J.is_prime}

The prime ideals of R × S are in bijection with the disjoint union of the prime ideals of R and the prime ideals of S.

Equations

ideal.prime_ideals_equiv R S = (equiv.of_bijective prime_ideals_equiv_impl _).symm

@[simp]

theorem ideal.prime_ideals_equiv_symm_inl {R : Type u} {S : Type v} [ring R] [ring S] (I : ideal R) (h : I.is_prime) :

⇑((ideal.prime_ideals_equiv R S).symm) (sum.inl ⟨I, h⟩) = ⟨I.prod ⊤, _⟩

@[simp]

theorem ideal.prime_ideals_equiv_symm_inr {R : Type u} {S : Type v} [ring R] [ring S] (J : ideal S) (h : J.is_prime) :

⇑((ideal.prime_ideals_equiv R S).symm) (sum.inr ⟨J, h⟩) = ⟨⊤.prod J, _⟩