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.

@[simp]

theorem Ideal.coe_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) : ↑(I.prod J) = ↑I ×ˢ ↑J

@[simp]

theorem Ideal.mem_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) {x : R × S} : x ∈ I.prod J ↔ x.1 ∈ I ∧ x.2 ∈ J

@[simp]

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

@[simp]

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

theorem Ideal.prod_mono {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I₁ I₂ : Ideal R} {J₁ J₂ : Ideal S} (hI : I₁ ≤ I₂) (hJ : J₁ ≤ J₂) : I₁.prod J₁ ≤ I₂.prod J₂

theorem Ideal.prod_mono_left {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I₁ I₂ : Ideal R} {J : Ideal S} (hI : I₁ ≤ I₂) : I₁.prod J ≤ I₂.prod J

theorem Ideal.prod_mono_right {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} {J₁ J₂ : Ideal S} (hJ : J₁ ≤ J₂) : I.prod J₁ ≤ I.prod J₂

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

@[simp]

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

@[simp]

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

def Ideal.idealProdEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring S] : Ideal (R × S) ≃o Ideal R × Ideal S

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

@[simp]

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

theorem Ideal.span_prod_le {R : Type u} {S : Type v} [Semiring R] [Semiring S] {s : Set R} {t : Set S} : span (s ×ˢ t) ≤ (span s).prod (span t)

theorem Ideal.span_prod {R : Type u} {S : Type v} [Semiring R] [Semiring S] {s : Set R} {t : Set S} (hst : s.Nonempty ↔ t.Nonempty) : span (s ×ˢ t) = (span s).prod (span t)

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

instance instIsPrincipalIdealRingProd {R : Type u} {S : Type v} [Semiring R] [Semiring S] [IsPrincipalIdealRing R] [IsPrincipalIdealRing S] : IsPrincipalIdealRing (R × S)