feat(ring_theory/ideal): ideals in product rings (#4431)

src/algebra/group/prod.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon, Patrick Massot, Yury Kudryashov
 -/
 import algebra.group.hom
+import data.equiv.mul_add
 import data.prod
 
 /-!
@@ -229,3 +230,18 @@ ext $ λ x, by simp
 end coprod
 
 end monoid_hom
+
+namespace mul_equiv
+variables (M N) [monoid M] [monoid N]
+
+/-- The equivalence between `M × N` and `N × M` given by swapping the components is multiplicative. -/
+@[to_additive prod_comm "The equivalence between `M × N` and `N × M` given by swapping the components is
+additive."]
+def prod_comm : M × N ≃* N × M :=
+{ map_mul' := λ ⟨x₁, y₁⟩ ⟨x₂, y₂⟩, rfl, ..equiv.prod_comm M N }
+
+@[simp, to_additive coe_prod_comm] lemma coe_prod_comm : ⇑(prod_comm M N) = prod.swap := rfl
+@[simp, to_additive coe_prod_comm_symm] lemma coe_prod_comm_symm :
+  ⇑((prod_comm M N).symm) = prod.swap := rfl
+
+end mul_equiv

src/algebra/ring/prod.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
 -/
 import algebra.group.prod
 import algebra.ring.basic
+import data.equiv.ring
 
 /-!
 # Semiring, ring etc structures on `R × S`
@@ -103,3 +104,24 @@ rfl
 end prod_map
 
 end ring_hom
+
+namespace ring_equiv
+variables (R S) [semiring R] [semiring S]
+
+/-- Swapping components as an equivalence of (semi)rings. -/
+def prod_comm : R × S ≃+* S × R :=
+{ ..add_equiv.prod_comm R S, ..mul_equiv.prod_comm R S }
+
+@[simp] lemma coe_prod_comm : ⇑(prod_comm R S) = prod.swap := rfl
+@[simp] lemma coe_prod_comm_symm : ⇑((prod_comm R S).symm) = prod.swap := rfl
+@[simp] lemma coe_coe_prod_comm : ⇑(prod_comm R S : R × S →+* S × R) = prod.swap := rfl
+@[simp] lemma coe_coe_prod_comm_symm : ⇑((prod_comm R S).symm : S × R →+* R × S) = prod.swap := rfl
+
+@[simp] lemma fst_comp_coe_prod_comm :
+  (ring_hom.fst S R).comp (prod_comm R S : R × S →+* S × R) = ring_hom.snd R S :=
+ring_hom.ext $ λ _, rfl
+@[simp] lemma snd_comp_coe_prod_comm :
+  (ring_hom.snd S R).comp (prod_comm R S : R × S →+* S × R) = ring_hom.fst R S :=
+ring_hom.ext $ λ _, rfl
+
+end ring_equiv

src/algebraic_geometry/prime_spectrum.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 import topology.opens
-import ring_theory.ideal.operations
+import ring_theory.ideal.prod
 import linear_algebra.finsupp
 import algebra.punit_instances
 
@@ -73,6 +73,26 @@ The prime spectrum of the zero ring is empty.
 lemma punit (x : prime_spectrum punit) : false :=
 x.1.ne_top_iff_one.1 x.2.1 $ subsingleton.elim (0 : punit) 1 ▸ x.1.zero_mem
 
+section
+variables (R) (S : Type v) [comm_ring S]
+
+/-- The prime spectrum of `R × S` is in bijection with the disjoint unions of the prime spectrum of
+    `R` and the prime spectrum of `S`. -/
+noncomputable def prime_spectrum_prod :
+  prime_spectrum (R × S) ≃ prime_spectrum R ⊕ prime_spectrum S :=
+ideal.prime_ideals_equiv R S
+
+variables {R S}
+
+@[simp] lemma prime_spectrum_prod_symm_inl_as_ideal (x : prime_spectrum R) :
+  ((prime_spectrum_prod R S).symm (sum.inl x)).as_ideal = ideal.prod x.as_ideal ⊤ :=
+by { cases x, refl }
+@[simp] lemma prime_spectrum_prod_symm_inr_as_ideal (x : prime_spectrum S) :
+  ((prime_spectrum_prod R S).symm (sum.inr x)).as_ideal = ideal.prod ⊤ x.as_ideal :=
+by { cases x, refl }
+
+end
+
 @[ext] lemma ext {x y : prime_spectrum R} :
   x = y ↔ x.as_ideal = y.as_ideal :=
 subtype.ext_iff_val

src/ring_theory/ideal/operations.lean

@@ -830,6 +830,9 @@ by rw [submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq_ze
 lemma not_one_mem_ker [nontrivial S] (f : R →+* S) : (1:R) ∉ ker f :=
 by { rw [mem_ker, f.map_one], exact one_ne_zero }
 
+@[simp] lemma ker_coe_equiv (f : R ≃+* S) : ker (f : R →+* S) = ⊥ :=
+by simpa only [←injective_iff_ker_eq_bot] using f.injective
+
 end comm_ring
 
 /-- The kernel of a homomorphism to an integral domain is a prime ideal.-/
@@ -893,6 +896,10 @@ begin
     exact (H.right this).imp (λ h, ha ▸ mem_map_of_mem h) (λ h, hb ▸ mem_map_of_mem h) }
 end
 
+theorem map_is_prime_of_equiv (f : R ≃+* S) {I : ideal R} [is_prime I] :
+  is_prime (map (f : R →+* S) I) :=
+map_is_prime_of_surjective f.surjective $ by simp
+
 theorem map_radical_of_surjective {f : R →+* S} (hf : function.surjective f) {I : ideal R}
   (h : ring_hom.ker f ≤ I) : map f (I.radical) = (map f I).radical :=
 begin

src/ring_theory/ideal/prod.lean

@@ -0,0 +1,199 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import ring_theory.ideal.operations
+
+/-!
+# 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.
+-/
+
+universes u v
+variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S] (I I' : ideal R) (J J' : ideal S)
+
+namespace ideal
+
+/-- `I × J` as an ideal of `R × S`. -/
+def prod : ideal (R × S) :=
+{ carrier := { x | x.fst ∈ I ∧ x.snd ∈ J },
+  zero_mem' := by simp,
+  add_mem' :=
+  begin
+    rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨ha₁, ha₂⟩ ⟨hb₁, hb₂⟩,
+    refine ⟨ideal.add_mem _ _ _, ideal.add_mem _ _ _⟩;
+    simp only [ha₁, ha₂, hb₁, hb₂]
+  end,
+  smul_mem' :=
+  begin
+    rintros ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ⟨hb₁, hb₂⟩,
+    refine ⟨ideal.mul_mem_left _ _, ideal.mul_mem_left _ _⟩;
+    simp only [hb₁, hb₂]
+  end }
+
+@[simp] lemma mem_prod {r : R} {s : S} : (⟨r, s⟩ : R × S) ∈ prod I J ↔ r ∈ I ∧ s ∈ J := iff.rfl
+@[simp] lemma prod_top_top : prod (⊤ : ideal R) (⊤ : ideal S) = ⊤ := ideal.ext $ by simp
+
+/-- 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 (ring_hom.fst R S) I) (map (ring_hom.snd R S) I) :=
+begin
+  apply ideal.ext,
+  rintro ⟨r, s⟩,
+  rw [mem_prod, mem_map_iff_of_surjective (ring_hom.fst R S) prod.fst_surjective,
+    mem_map_iff_of_surjective (ring_hom.snd R S) prod.snd_surjective],
+  refine ⟨λ h, ⟨⟨_, ⟨h, rfl⟩⟩, ⟨_, ⟨h, rfl⟩⟩⟩, _⟩,
+  rintro ⟨⟨⟨r, s'⟩, ⟨h₁, rfl⟩⟩, ⟨⟨r', s⟩, ⟨h₂, rfl⟩⟩⟩,
+  have hr : (r, s') * (1, 0) ∈ I := ideal.mul_mem_right _ h₁,
+  have hs : (r', s) * (0, 1) ∈ I := ideal.mul_mem_right _ h₂,
+  simpa using ideal.add_mem _ hr hs
+end
+
+@[simp] lemma map_fst_prod (I : ideal R) (J : ideal S) : map (ring_hom.fst R S) (prod I J) = I :=
+begin
+  ext,
+  rw mem_map_iff_of_surjective (ring_hom.fst R S) prod.fst_surjective,
+  exact ⟨by { rintro ⟨x, ⟨h, rfl⟩⟩, exact h.1 }, λ h, ⟨⟨x, 0⟩, ⟨⟨h, ideal.zero_mem _⟩, rfl⟩⟩⟩
+end
+
+@[simp] lemma map_snd_prod (I : ideal R) (J : ideal S) : map (ring_hom.snd R S) (prod I J) = J :=
+begin
+  ext,
+  rw mem_map_iff_of_surjective (ring_hom.snd R S) prod.snd_surjective,
+  exact ⟨by { rintro ⟨x, ⟨h, rfl⟩⟩, exact h.2 }, λ h, ⟨⟨0, x⟩, ⟨⟨ideal.zero_mem _, h⟩, rfl⟩⟩⟩
+end
+
+@[simp] lemma map_prod_comm_prod :
+  map (ring_equiv.prod_comm R S : R × S →+* S × R) (prod I J) = prod J I :=
+begin
+  rw [ideal_prod_eq (map (ring_equiv.prod_comm R S : R × S →+* S × R) (prod I J))],
+  simp [map_map]
+end
+
+/-- Ideals of `R × S` are in one-to-one correspondence with pairs of ideals of `R` and ideals of
+    `S`. -/
+def ideal_prod_equiv : ideal (R × S) ≃ ideal R × ideal S :=
+{ to_fun := λ I, ⟨map (ring_hom.fst R S) I, map (ring_hom.snd R S) I⟩,
+  inv_fun := λ I, prod I.1 I.2,
+  left_inv := λ I, (ideal_prod_eq I).symm,
+  right_inv := λ ⟨I, J⟩, by simp }
+
+@[simp] lemma ideal_prod_equiv_symm_apply (I : ideal R) (J : ideal S) :
+  ideal_prod_equiv.symm ⟨I, J⟩ = prod I J := rfl
+
+lemma prod.ext_iff {I I' : ideal R} {J J' : ideal S} : prod I J = prod I' J' ↔ I = I' ∧ J = J' :=
+by simp only [←ideal_prod_equiv_symm_apply, ideal_prod_equiv.symm.injective.eq_iff, prod.mk.inj_iff]
+
+lemma is_prime_of_is_prime_prod_top {I : ideal R} (h : (ideal.prod I (⊤ : ideal S)).is_prime) :
+  I.is_prime :=
+begin
+  split,
+  { unfreezingI { contrapose! h },
+    simp [is_prime, h] },
+  { intros x y hxy,
+    have : (⟨x, 1⟩ : R × S) * ⟨y, 1⟩ ∈ prod I ⊤,
+    { rw [prod.mk_mul_mk, mul_one, mem_prod],
+      exact ⟨hxy, trivial⟩ },
+    simpa using h.mem_or_mem this }
+end
+
+lemma is_prime_of_is_prime_prod_top' {I : ideal S} (h : (ideal.prod (⊤ : ideal R) I).is_prime) :
+  I.is_prime :=
+begin
+  apply @is_prime_of_is_prime_prod_top _ R,
+  rw ←map_prod_comm_prod,
+  exact map_is_prime_of_equiv _
+end
+
+lemma is_prime_ideal_prod_top {I : ideal R} [h : I.is_prime] : (prod I (⊤ : ideal S)).is_prime :=
+begin
+  split,
+  { unfreezingI { rcases h with ⟨h, -⟩, contrapose! h },
+    rw [←prod_top_top, prod.ext_iff] at h,
+    exact h.1 },
+  rintros ⟨r₁, s₁⟩ ⟨r₂, s₂⟩ ⟨h₁, h₂⟩,
+  cases h.mem_or_mem h₁ with h h,
+  { exact or.inl ⟨h, trivial⟩ },
+  { exact or.inr ⟨h, trivial⟩ }
+end
+
+lemma is_prime_ideal_prod_top' {I : ideal S} [h : I.is_prime] : (prod (⊤ : ideal R) I).is_prime :=
+begin
+  rw ←map_prod_comm_prod,
+  apply map_is_prime_of_equiv _,
+  exact is_prime_ideal_prod_top,
+end
+
+lemma ideal_prod_prime_aux {I : ideal R} {J : ideal S} : (ideal.prod I J).is_prime →
+  I = ⊤ ∨ J = ⊤ :=
+begin
+  contrapose!,
+  simp only [ne_top_iff_one, is_prime, not_and, not_forall, not_or_distrib],
+  exact λ ⟨hI, hJ⟩ hIJ, ⟨⟨0, 1⟩, ⟨1, 0⟩, by simp, by simp [hJ], by simp [hI]⟩
+end
+
+/-- 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.is_prime ↔
+  ((∃ p : ideal R, p.is_prime ∧ I = ideal.prod p ⊤) ∨
+   (∃ p : ideal S, p.is_prime ∧ I = ideal.prod ⊤ p)) :=
+begin
+  split,
+  { rw ideal_prod_eq I,
+    introsI hI,
+    rcases ideal_prod_prime_aux hI with (h|h),
+    { right,
+      rw h at hI ⊢,
+      exact ⟨_, ⟨is_prime_of_is_prime_prod_top' hI, rfl⟩⟩ },
+    { left,
+      rw h at hI ⊢,
+      exact ⟨_, ⟨is_prime_of_is_prime_prod_top hI, rfl⟩⟩ } },
+  { rintro (⟨p, ⟨h, rfl⟩⟩|⟨p, ⟨h, rfl⟩⟩),
+    { exactI is_prime_ideal_prod_top },
+    { exactI is_prime_ideal_prod_top' } }
+end
+
+@[simp] private def prime_ideals_equiv_impl :
+  { I : ideal R // I.is_prime } ⊕ { J : ideal S // J.is_prime } →
+    { K : ideal (R × S) // K.is_prime }
+| (sum.inl ⟨I, hI⟩) := ⟨ideal.prod I ⊤, by exactI is_prime_ideal_prod_top⟩
+| (sum.inr ⟨J, hJ⟩) := ⟨ideal.prod ⊤ J, by exactI is_prime_ideal_prod_top'⟩
+
+section
+variables (R S)
+
+/-- 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`. -/
+noncomputable def prime_ideals_equiv : { K : ideal (R × S) // K.is_prime } ≃
+  { I : ideal R // I.is_prime } ⊕ { J : ideal S // J.is_prime } :=
+equiv.symm $ equiv.of_bijective prime_ideals_equiv_impl
+begin
+  split,
+  { rintros (⟨I, hI⟩|⟨J, hJ⟩) (⟨I',  hI'⟩|⟨J', hJ'⟩) h;
+    simp [prod.ext_iff] at h,
+    { simp [h] },
+    { exact false.elim (hI.1 h.1) },
+    { exact false.elim (hJ.1 h.2) },
+    { simp [h] } },
+  { rintro ⟨I, hI⟩,
+    rcases (ideal_prod_prime I).1 hI with (⟨p, ⟨hp, rfl⟩⟩|⟨p, ⟨hp, rfl⟩⟩),
+    { exact ⟨sum.inl ⟨p, hp⟩, rfl⟩ },
+    { exact ⟨sum.inr ⟨p, hp⟩, rfl⟩ } }
+end
+
+end
+
+@[simp] lemma prime_ideals_equiv_symm_inl (h : I.is_prime) :
+  (prime_ideals_equiv R S).symm (sum.inl ⟨I, h⟩) = ⟨prod I ⊤, by exactI is_prime_ideal_prod_top⟩ :=
+rfl
+@[simp] lemma prime_ideals_equiv_symm_inr (h : J.is_prime) :
+  (prime_ideals_equiv R S).symm (sum.inr ⟨J, h⟩) = ⟨prod ⊤ J, by exactI is_prime_ideal_prod_top'⟩ :=
+rfl
+
+end ideal