From 221ec606133b565e8469c4a3cf9b8e7297860cb2 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 5 Oct 2020 19:45:13 +0000 Subject: [PATCH] feat(ring_theory/ideal): ideals in product rings (#4431) --- src/algebra/group/prod.lean | 16 ++ src/algebra/ring/prod.lean | 22 +++ src/algebraic_geometry/prime_spectrum.lean | 22 ++- src/ring_theory/ideal/operations.lean | 7 + src/ring_theory/ideal/prod.lean | 199 +++++++++++++++++++++ 5 files changed, 265 insertions(+), 1 deletion(-) create mode 100644 src/ring_theory/ideal/prod.lean diff --git a/src/algebra/group/prod.lean b/src/algebra/group/prod.lean index 6f31202a40b9d..0de87e8041f65 100644 --- a/src/algebra/group/prod.lean +++ b/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 diff --git a/src/algebra/ring/prod.lean b/src/algebra/ring/prod.lean index 2a575eeb2c572..fd359d60d86dc 100644 --- a/src/algebra/ring/prod.lean +++ b/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 diff --git a/src/algebraic_geometry/prime_spectrum.lean b/src/algebraic_geometry/prime_spectrum.lean index 35c54069462b0..d73f5be921f10 100644 --- a/src/algebraic_geometry/prime_spectrum.lean +++ b/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 diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean index a0f2f5c6e32bd..f3ddc0a80c658 100644 --- a/src/ring_theory/ideal/operations.lean +++ b/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 diff --git a/src/ring_theory/ideal/prod.lean b/src/ring_theory/ideal/prod.lean new file mode 100644 index 0000000000000..35c80b432c4d5 --- /dev/null +++ b/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