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

I × J as an ideal of R × S.

Equations
Instances For
    @[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] :
    @[simp]
    theorem Ideal.prod_bot_bot {R : Type u} {S : Type v} [Semiring R] [Semiring S] :
    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) :
    def Ideal.idealProdEquiv {R : Type u} {S : Type v} [Semiring R] [Semiring 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.
    Instances For
      @[simp]
      theorem Ideal.idealProdEquiv_symm_apply {R : Type u} {S : Type v} [Semiring R] [Semiring S] (I : Ideal R) (J : Ideal S) :
      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'
      @[deprecated Ideal.prod_inj (since := "2025-05-22")]
      theorem Ideal.prod.ext_iff {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'

      Alias of Ideal.prod_inj.

      @[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) :
      theorem Ideal.isPrime_of_isPrime_prod_top' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} (h : (.prod I).IsPrime) :
      theorem Ideal.isPrime_ideal_prod_top {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal R} [h : I.IsPrime] :
      theorem Ideal.isPrime_ideal_prod_top' {R : Type u} {S : Type v} [Semiring R] [Semiring S] {I : Ideal S} [h : 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).IsPrimeI = 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.