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} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal (R × S)

I × J as an ideal of R × S.

Equations

• Ideal.prod I J = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : R × S | x.1 ∈ I ∧ x.2 ∈ J}, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

@[simp]

theorem Ideal.mem_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) {r : R} {s : S} : (r, s) ∈ Ideal.prod I J ↔ r ∈ I ∧ s ∈ J

@[simp]

theorem Ideal.prod_top_top {R : Type u} {S : Type v} [Semiring R] [Semiring S] : Ideal.prod ⊤ ⊤ = ⊤

theorem Ideal.ideal_prod_eq {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal (R × S)) : I = Ideal.prod (Ideal.map (RingHom.fst R S) I) (Ideal.map (RingHom.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} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (RingHom.fst R S) (Ideal.prod I J) = I

@[simp]

theorem Ideal.map_snd_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (RingHom.snd R S) (Ideal.prod I J) = J

@[simp]

theorem Ideal.map_prodComm_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.map (↑RingEquiv.prodComm) (Ideal.prod I J) = Ideal.prod J I

def Ideal.idealProdEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.idealProdEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : Ideal.idealProdEquiv.symm (I, J) = Ideal.prod I J

theorem Ideal.prod.ext_iff {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {I' : Ideal R} {J : Ideal S} {J' : Ideal S} : Ideal.prod I J = Ideal.prod I' J' ↔ I = I' ∧ J = J'

theorem Ideal.isPrime_of_isPrime_prod_top {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} (h : Ideal.IsPrime (Ideal.prod I ⊤)) : Ideal.IsPrime I

theorem Ideal.isPrime_of_isPrime_prod_top' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} (h : Ideal.IsPrime (Ideal.prod ⊤ I)) : Ideal.IsPrime I

theorem Ideal.isPrime_ideal_prod_top {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} [h : Ideal.IsPrime I] : Ideal.IsPrime (Ideal.prod I ⊤)

theorem Ideal.isPrime_ideal_prod_top' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} [h : Ideal.IsPrime I] : Ideal.IsPrime (Ideal.prod ⊤ I)

theorem Ideal.ideal_prod_prime_aux {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {J : Ideal S} : Ideal.IsPrime (Ideal.prod I J) → I = ⊤ ∨ J = ⊤

theorem Ideal.ideal_prod_prime {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal (R × S)) : Ideal.IsPrime I ↔ (∃ (p : Ideal R), Ideal.IsPrime p ∧ I = Ideal.prod p ⊤) ∨ ∃ (p : Ideal S), Ideal.IsPrime p ∧ I = Ideal.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.