Mathlib.RingTheory.Ideal.Prod

Ideal.prod definition

: Ideal (R × S)

Full source

/-- `I × J` as an ideal of `R × S`. -/
def prod : Ideal (R × S) := I.comap (RingHom.fst R S) ⊓ J.comap (RingHom.snd R S)

Product of ideals in a product ring

Informal description

For commutative rings $ R $ and $ S $ and ideals $ I \subseteq R $, $ J \subseteq S $, the product ideal $ I \times J $ is defined as the intersection of the preimages of $ I $ and $ J $ under the projection homomorphisms $ \text{fst} : R \times S \to R $ and $ \text{snd} : R \times S \to S $, respectively. This construction yields an ideal in the product ring $ R \times S $.

Ideal.mem_prod theorem

{r : R} {s : S} : (⟨r, s⟩ : R × S) ∈ prod I J ↔ r ∈ I ∧ s ∈ J

Full source

@[simp]
theorem mem_prod {r : R} {s : S} : (⟨r, s⟩ : R × S) ∈ prod I J(⟨r, s⟩ : R × S) ∈ prod I J ↔ r ∈ I ∧ s ∈ J :=
  Iff.rfl

Membership Criterion for Product Ideal: $(r, s) \in I \times J \leftrightarrow r \in I \land s \in J$

Informal description

For any elements $r \in R$ and $s \in S$, the pair $(r, s)$ belongs to the product ideal $I \times J$ in $R \times S$ if and only if $r \in I$ and $s \in J$.

Ideal.prod_top_top theorem

: prod (⊤ : Ideal R) (⊤ : Ideal S) = ⊤

Full source

@[simp]
theorem prod_top_top : prod (⊤ : Ideal R) (⊤ : Ideal S) = ⊤ :=
  Ideal.ext <| by simp

Product of Top Ideals is Top Ideal in Product Ring

Informal description

The product of the top ideals in commutative rings $R$ and $S$ is equal to the top ideal in the product ring $R \times S$, i.e., $(\top : \text{Ideal } R) \times (\top : \text{Ideal } S) = \top$.

Ideal.ideal_prod_eq theorem

(I : Ideal (R × S)) : I = Ideal.prod (map (RingHom.fst R S) I : Ideal R) (map (RingHom.snd R S) I)

Full source

/-- 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. -/
theorem ideal_prod_eq (I : Ideal (R × S)) :
    I = Ideal.prod (map (RingHom.fst R S) I : Ideal R) (map (RingHom.snd R S) I) := by
  apply Ideal.ext
  rintro ⟨r, s⟩
  rw [mem_prod, mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective,
    mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
  refine ⟨fun h => ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, ?_⟩
  rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩
  simpa using I.add_mem (I.mul_mem_left (1, 0) h₁) (I.mul_mem_left (0, 1) h₂)

Classification of Ideals in Product Rings: $I = \pi_1(I) \times \pi_2(I)$

Informal description

Let $R$ and $S$ be commutative rings. For any ideal $I$ of the product ring $R \times S$, we have \[ I = I_1 \times I_2 \] where $I_1$ is the image of $I$ under the first projection $\pi_1: R \times S \to R$ and $I_2$ is the image of $I$ under the second projection $\pi_2: R \times S \to S$.

Ideal.map_fst_prod theorem

(I : Ideal R) (J : Ideal S) : map (RingHom.fst R S) (prod I J) = I

Full source

@[simp]
theorem map_fst_prod (I : Ideal R) (J : Ideal S) : map (RingHom.fst R S) (prod I J) = I := by
  ext x
  rw [mem_map_iff_of_surjective (RingHom.fst R S) Prod.fst_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.1, fun h => ⟨⟨x, 0⟩, ⟨⟨h, Ideal.zero_mem _⟩, rfl⟩⟩⟩

First Projection of Product Ideal Equals First Factor

Informal description

For any ideals $I$ in a commutative ring $R$ and $J$ in a commutative ring $S$, the image of the product ideal $I \times J$ under the first projection homomorphism $\operatorname{fst} \colon R \times S \to R$ equals $I$.

Ideal.map_snd_prod theorem

(I : Ideal R) (J : Ideal S) : map (RingHom.snd R S) (prod I J) = J

Full source

@[simp]
theorem map_snd_prod (I : Ideal R) (J : Ideal S) : map (RingHom.snd R S) (prod I J) = J := by
  ext x
  rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]
  exact
    ⟨by
      rintro ⟨x, ⟨h, rfl⟩⟩
      exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩

Second Projection of Product Ideal Equals Second Factor

Informal description

For any ideals $I$ in a commutative ring $R$ and $J$ in a commutative ring $S$, the image of the product ideal $I \times J$ under the second projection ring homomorphism $\operatorname{snd} : R \times S \to S$ is equal to $J$.

Ideal.map_prodComm_prod theorem

: map ((RingEquiv.prodComm : R × S ≃+* S × R) : R × S →+* S × R) (prod I J) = prod J I

Full source

@[simp]
theorem map_prodComm_prod :
    map ((RingEquiv.prodComm : R × SR × S ≃+* S × R) : R × SR × S →+* S × R) (prod I J) = prod J I := by
  refine Trans.trans (ideal_prod_eq _) ?_
  simp [map_map]

Image of Product Ideal under Component Swap Equals Swapped Product Ideal

Informal description

Let $R$ and $S$ be commutative rings, and let $I \subseteq R$ and $J \subseteq S$ be ideals. The image of the product ideal $I \times J$ under the ring isomorphism $\text{prodComm} \colon R \times S \to S \times R$ (which swaps the components) is equal to the product ideal $J \times I$.

Ideal.idealProdEquiv definition

: Ideal (R × S) ≃o Ideal R × Ideal S

Full source

/-- Ideals of `R × S` are in one-to-one correspondence with pairs of ideals of `R` and ideals of
    `S`. -/
def idealProdEquiv : IdealIdeal (R × S) ≃o Ideal R × Ideal S where
  toFun I := ⟨map (RingHom.fst R S) I, map (RingHom.snd R S) I⟩
  invFun I := prod I.1 I.2
  left_inv I := (ideal_prod_eq I).symm
  right_inv := fun ⟨I, J⟩ => by simp
  map_rel_iff' {I J} := by
    simp only [Equiv.coe_fn_mk, ge_iff_le, Prod.mk_le_mk]
    refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩
    rw [ideal_prod_eq I, ideal_prod_eq J]
    exact inf_le_inf (comap_mono h.1) (comap_mono h.2)

Order isomorphism between ideals in product rings and pairs of ideals

Informal description

The order isomorphism between the lattice of ideals in the product ring $R \times S$ and the product lattice of ideals in $R$ and ideals in $S$. Specifically, it maps an ideal $I$ of $R \times S$ to the pair of ideals obtained by projecting $I$ onto $R$ and $S$ via the first and second projection homomorphisms, respectively. The inverse map takes a pair of ideals $(I, J)$ in $R \times S$ to the product ideal $I \times J$ in $R \times S$.

Ideal.idealProdEquiv_symm_apply theorem

(I : Ideal R) (J : Ideal S) : idealProdEquiv.symm ⟨I, J⟩ = prod I J

Full source

@[simp]
theorem idealProdEquiv_symm_apply (I : Ideal R) (J : Ideal S) :
    idealProdEquiv.symm ⟨I, J⟩ = prod I J :=
  rfl

Inverse of Ideal Product Order Isomorphism Maps to Product Ideal

Informal description

For any ideals $I$ of a commutative ring $R$ and $J$ of a commutative ring $S$, the inverse of the order isomorphism $\text{idealProdEquiv}$ applied to the pair $(I, J)$ is equal to the product ideal $I \times J$ in the ring $R \times S$.

Ideal.prod.ext_iff theorem

{I I' : Ideal R} {J J' : Ideal S} : prod I J = prod I' J' ↔ I = I' ∧ J = J'

Full source

theorem prod.ext_iff {I I' : Ideal R} {J J' : Ideal S} :
    prodprod I J = prod I' J' ↔ I = I' ∧ J = J' := by
  simp only [← idealProdEquiv_symm_apply, idealProdEquiv.symm.injective.eq_iff, Prod.mk_inj]

Equality of Product Ideals in Product Rings

Informal description

For any ideals $I, I'$ in a commutative ring $R$ and $J, J'$ in a commutative ring $S$, the product ideals $I \times J$ and $I' \times J'$ in $R \times S$ are equal if and only if $I = I'$ and $J = J'$.

Ideal.isPrime_of_isPrime_prod_top theorem

{I : Ideal R} (h : (Ideal.prod I (⊤ : Ideal S)).IsPrime) : I.IsPrime

Full source

theorem isPrime_of_isPrime_prod_top {I : Ideal R} (h : (Ideal.prod I (⊤ : Ideal S)).IsPrime) :
    I.IsPrime := by
  constructor
  · contrapose! h
    rw [h, prod_top_top, isPrime_iff]
    simp [isPrime_iff, h]
  · intro x y hxy
    have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤ := by
      rw [Prod.mk_mul_mk, mul_one, mem_prod]
      exact ⟨hxy, trivial⟩
    simpa using h.mem_or_mem this

Prime Ideal Property Transfer: $I \times S$ prime implies $I$ prime

Informal description

Let $R$ and $S$ be commutative rings, and let $I$ be an ideal of $R$. If the product ideal $I \times S$ in $R \times S$ is prime, then $I$ is a prime ideal of $R$.

Ideal.isPrime_of_isPrime_prod_top' theorem

{I : Ideal S} (h : (Ideal.prod (⊤ : Ideal R) I).IsPrime) : I.IsPrime

Full source

theorem isPrime_of_isPrime_prod_top' {I : Ideal S} (h : (Ideal.prod (⊤ : Ideal R) I).IsPrime) :
    I.IsPrime := by
  apply isPrime_of_isPrime_prod_top (S := R)
  rw [← map_prodComm_prod]
  -- Note: couldn't synthesize the right instances without the `R` and `S` hints
  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := R) (S := S))

Prime Ideal Property Transfer: $R \times I$ prime implies $I$ prime

Informal description

Let $R$ and $S$ be commutative rings, and let $I$ be an ideal of $S$. If the product ideal $R \times I$ in $R \times S$ is prime, then $I$ is a prime ideal of $S$.

Ideal.isPrime_ideal_prod_top theorem

{I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Ideal S)).IsPrime

Full source

theorem isPrime_ideal_prod_top {I : Ideal R} [h : I.IsPrime] : (prod I (⊤ : Ideal S)).IsPrime := by
  constructor
  · rcases h with ⟨h, -⟩
    contrapose! h
    rw [← prod_top_top, prod.ext_iff] at h
    exact h.1
  rintro ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, _⟩
  rcases h.mem_or_mem h₁ with h | h
  · exact Or.inl ⟨h, trivial⟩
  · exact Or.inr ⟨h, trivial⟩

Prime Ideal Property of $I \times S$ for Prime Ideal $I$

Informal description

Let $R$ and $S$ be commutative rings, and let $I$ be a prime ideal of $R$. Then the product ideal $I \times S$ in $R \times S$ is a prime ideal.

Ideal.isPrime_ideal_prod_top' theorem

{I : Ideal S} [h : I.IsPrime] : (prod (⊤ : Ideal R) I).IsPrime

Full source

theorem isPrime_ideal_prod_top' {I : Ideal S} [h : I.IsPrime] : (prod (⊤ : Ideal R) I).IsPrime := by
  letI : IsPrime (prod I (⊤ : Ideal R)) := isPrime_ideal_prod_top
  rw [← map_prodComm_prod]
  -- Note: couldn't synthesize the right instances without the `R` and `S` hints
  exact map_isPrime_of_equiv (RingEquiv.prodComm (R := S) (S := R))

Prime Ideal Property of $R \times I$ for Prime Ideal $I$

Informal description

Let $R$ and $S$ be commutative rings, and let $I$ be a prime ideal of $S$. Then the product ideal $R \times I$ in $R \times S$ is a prime ideal.

Ideal.ideal_prod_prime_aux theorem

{I : Ideal R} {J : Ideal S} : (Ideal.prod I J).IsPrime → I = ⊤ ∨ J = ⊤

Full source

theorem ideal_prod_prime_aux {I : Ideal R} {J : Ideal S} :
    (Ideal.prod I J).IsPrime → I = ⊤ ∨ J = ⊤ := by
  contrapose!
  simp only [ne_top_iff_one, isPrime_iff, not_and, not_forall, not_or]
  exact fun ⟨hI, hJ⟩ _ => ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩

Prime Product Ideal Implies Full Ring in One Component

Informal description

Let $R$ and $S$ be commutative rings, and let $I \subseteq R$ and $J \subseteq S$ be ideals. If the product ideal $I \times J$ is a prime ideal in $R \times S$, then either $I$ is the entire ring $R$ or $J$ is the entire ring $S$.

Ideal.ideal_prod_prime theorem

 (I : Ideal (R × S)) :
  I.IsPrime ↔ (∃ p : Ideal R, p.IsPrime ∧ I = Ideal.prod p ⊤) ∨ ∃ p : Ideal S, p.IsPrime ∧ I = Ideal.prod ⊤ p

Full source

/-- 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`. -/
theorem ideal_prod_prime (I : Ideal (R × S)) :
    I.IsPrime ↔
      (∃ p : Ideal R, p.IsPrime ∧ I = Ideal.prod p ⊤) ∨
        ∃ p : Ideal S, p.IsPrime ∧ I = Ideal.prod ⊤ p := by
  constructor
  · rw [ideal_prod_eq I]
    intro hI
    rcases ideal_prod_prime_aux hI with (h | h)
    · right
      rw [h] at hI ⊢
      exact ⟨_, ⟨isPrime_of_isPrime_prod_top' hI, rfl⟩⟩
    · left
      rw [h] at hI ⊢
      exact ⟨_, ⟨isPrime_of_isPrime_prod_top hI, rfl⟩⟩
  · rintro (⟨p, ⟨h, rfl⟩⟩ | ⟨p, ⟨h, rfl⟩⟩)
    · exact isPrime_ideal_prod_top
    · exact isPrime_ideal_prod_top'

Classification of Prime Ideals in Product Rings: $I$ prime $\iff$ $I = p \times S$ or $I = R \times p$ for $p$ prime

Informal description

Let $R$ and $S$ be commutative rings. An ideal $I$ of the product ring $R \times S$ is prime if and only if it is of the form $I = p \times S$ for some prime ideal $p$ of $R$, or $I = R \times p$ for some prime ideal $p$ of $S$.