From 0a5cedd720a41d799d0a411a6a4179d1516c1ffd Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 09:53:40 -0500 Subject: [PATCH 01/22] feat: port RingTheory.Ideal.MinimalPrime From ce6f32a6bc052ac5d607b0f67082773d1044779b Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 09:53:40 -0500 Subject: [PATCH 02/22] Initial file copy from mathport --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 241 +++++++++++++++++++++ 1 file changed, 241 insertions(+) create mode 100644 Mathlib/RingTheory/Ideal/MinimalPrime.lean diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean new file mode 100644 index 0000000000000..5a078d944e6b6 --- /dev/null +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -0,0 +1,241 @@ +/- +Copyright (c) 2022 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang + +! This file was ported from Lean 3 source module ring_theory.ideal.minimal_prime +! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.RingTheory.Localization.AtPrime +import Mathbin.Order.Minimal + +/-! + +# Minimal primes + +We provide various results concerning the minimal primes above an ideal + +## Main results +- `ideal.minimal_primes`: `I.minimal_primes` is the set of ideals that are minimal primes over `I`. +- `minimal_primes`: `minimal_primes R` is the set of minimal primes of `R`. +- `ideal.exists_minimal_primes_le`: Every prime ideal over `I` contains a minimal prime over `I`. +- `ideal.radical_minimal_primes`: The minimal primes over `I.radical` are precisely + the minimal primes over `I`. +- `ideal.Inf_minimal_primes`: The intersection of minimal primes over `I` is `I.radical`. +- `ideal.exists_minimal_primes_comap_eq` If `p` is a minimal prime over `f ⁻¹ I`, then it is the + preimage of some minimal prime over `I`. +- `ideal.minimal_primes_eq_comap`: The minimal primes over `I` are precisely the preimages of + minimal primes of `R ⧸ I`. + + +-/ + + +section + +variable {R S : Type _} [CommRing R] [CommRing S] (I J : Ideal R) + +/-- `I.minimal_primes` is the set of ideals that are minimal primes over `I`. -/ +def Ideal.minimalPrimes : Set (Ideal R) := + minimals (· ≤ ·) { p | p.IsPrime ∧ I ≤ p } +#align ideal.minimal_primes Ideal.minimalPrimes + +/-- `minimal_primes R` is the set of minimal primes of `R`. +This is defined as `ideal.minimal_primes ⊥`. -/ +def minimalPrimes (R : Type _) [CommRing R] : Set (Ideal R) := + Ideal.minimalPrimes ⊥ +#align minimal_primes minimalPrimes + +variable {I J} + +theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J := + by + suffices + ∃ m ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p }, + OrderDual.toDual J ≤ m ∧ ∀ z ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p }, m ≤ z → z = m + by + obtain ⟨p, h₁, h₂, h₃⟩ := this + simp_rw [← @eq_comm _ p] at h₃ + exact ⟨p, ⟨h₁, fun a b c => (h₃ a b c).le⟩, h₂⟩ + apply zorn_nonempty_partialOrder₀ + swap + · refine' ⟨show J.is_prime by infer_instance, e⟩ + rintro (c : Set (Ideal R)) hc hc' J' hJ' + refine' + ⟨OrderDual.toDual (Inf c), + ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩ + · rw [OrderDual.ofDual_toDual] + convert le_sInf _ + intro x hx + exact (hc hx).2 + · rintro z hz + rw [OrderDual.le_toDual] + exact sInf_le hz +#align ideal.exists_minimal_primes_le Ideal.exists_minimalPrimes_le + +@[simp] +theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes := + by + rw [Ideal.minimalPrimes, Ideal.minimalPrimes] + congr + ext p + exact ⟨fun ⟨a, b⟩ => ⟨a, ideal.le_radical.trans b⟩, fun ⟨a, b⟩ => ⟨a, a.radical_le_iff.mpr b⟩⟩ +#align ideal.radical_minimal_primes Ideal.radical_minimalPrimes + +@[simp] +theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := + by + rw [I.radical_eq_Inf] + apply le_antisymm + · intro x hx + rw [Ideal.mem_sInf] at hx⊢ + rintro J ⟨e, hJ⟩ + skip + obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e + exact hp' (hx hp) + · apply sInf_le_sInf _ + intro I hI + exact hI.1.symm +#align ideal.Inf_minimal_primes Ideal.sInf_minimalPrimes + +/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » minimal_primes[minimal_primes] R) -/ +theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} + (hf : Function.Injective f) (p) (_ : p ∈ minimalPrimes R) : + ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := + by + haveI := H.1.1 + have : Nontrivial (Localization (Submonoid.map f p.prime_compl)) := + by + refine' ⟨⟨1, 0, _⟩⟩ + convert(IsLocalization.map_injective_of_injective p.prime_compl (Localization.AtPrime p) + (Localization <| p.prime_compl.map f) hf).Ne + one_ne_zero + · rw [map_one] + · rw [map_zero] + obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.prime_compl)) + skip + refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.prime_compl)), inferInstance, _⟩ + rw [Ideal.comap_comap, ← + @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.prime_compl.le_comap_map _ + Localization.isLocalization, + ← Ideal.comap_comap] + suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this) + intro x hx + by_contra h + apply hM.ne_top + apply M.eq_top_of_is_unit_mem hx + apply IsUnit.map + apply IsLocalization.map_units _ (show p.prime_compl from ⟨x, h⟩) + infer_instance +#align ideal.exists_comap_eq_of_mem_minimal_primes_of_injective Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective + +/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ +theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) + (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := + by + haveI := H.1.1 + let f' := I.Quotient.mk.comp f + have e : (I.Quotient.mk.comp f).ker = I.comap f := + by + ext1 + exact Submodule.Quotient.mk_eq_zero _ + have : (I.Quotient.mk.comp f).ker.Quotient.mk.ker ≤ p := + by + rw [Ideal.mk_ker, e] + exact H.1.2 + obtain ⟨p', hp₁, hp₂⟩ := + Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective + (I.Quotient.mk.comp f).ker_lift_injective (p.map (I.Quotient.mk.comp f).ker.Quotient.mk) _ + · skip + refine' ⟨p'.comap I.Quotient.mk, Ideal.IsPrime.comap _, _, _⟩ + · exact ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) + convert congr_arg (Ideal.comap (I.Quotient.mk.comp f).ker.Quotient.mk) hp₂ + rwa [Ideal.comap_map_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk + Ideal.Quotient.mk_surjective, + eq_comm, sup_eq_left] + refine' ⟨⟨_, bot_le⟩, _⟩ + · apply Ideal.map_isPrime_of_surjective _ this + exact Ideal.Quotient.mk_surjective + · rintro q ⟨hq, -⟩ hq' + rw [← + Ideal.map_comap_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk + Ideal.Quotient.mk_surjective q] + apply Ideal.map_mono + skip + apply H.2 + · refine' ⟨inferInstance, (ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩ + · refine' (Ideal.comap_mono hq').trans _ + rw [Ideal.comap_map_of_surjective] + exacts[sup_le rfl.le this, Ideal.Quotient.mk_surjective] +#align ideal.exists_comap_eq_of_mem_minimal_primes Ideal.exists_comap_eq_of_mem_minimalPrimes + +/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ +theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) + (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := + by + obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H + skip + obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂ + refine' ⟨q, hq, Eq.symm _⟩ + haveI := hq.1.1 + have := (Ideal.comap_mono hq').trans_eq h₃ + exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this +#align ideal.exists_minimal_primes_comap_eq Ideal.exists_minimalPrimes_comap_eq + +theorem Ideal.mimimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f) + {I J : Ideal S} (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes := + by + haveI := h.1.1 + refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩ + rintro K ⟨hK, e₁⟩ e₂ + have : f.ker ≤ K := (Ideal.comap_mono bot_le).trans e₁ + rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf] + apply Ideal.comap_mono _ + apply h.2 _ _ + · exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩ + · exact Ideal.map_le_of_le_comap e₂ +#align ideal.mimimal_primes_comap_of_surjective Ideal.mimimal_primes_comap_of_surjective + +theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Function.Surjective f) + (I : Ideal S) : (I.comap f).minimalPrimes = Ideal.comap f '' I.minimalPrimes := + by + ext J + constructor + · intro H + obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H + exact ⟨p, h, rfl⟩ + · rintro ⟨J, hJ, rfl⟩ + exact Ideal.mimimal_primes_comap_of_surjective hf hJ +#align ideal.comap_minimal_primes_eq_of_surjective Ideal.comap_minimalPrimes_eq_of_surjective + +theorem Ideal.minimalPrimes_eq_comap : + I.minimalPrimes = Ideal.comap I.Quotient.mk '' minimalPrimes (R ⧸ I) := by + rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, ← + RingHom.ker_eq_comap_bot, Ideal.mk_ker] +#align ideal.minimal_primes_eq_comap Ideal.minimalPrimes_eq_comap + +theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = {I.radical} := + by + ext J + constructor + · + exact fun H => + let e := H.1.1.radical_le_iff.mpr H.1.2 + (H.2 ⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩ e).antisymm e + · rintro (rfl : J = I.radical) + exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩ +#align ideal.minimal_primes_eq_subsingleton Ideal.minimalPrimes_eq_subsingleton + +theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = {I} := + by + ext J + constructor + · exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2 + · rintro (rfl : J = I) + refine' ⟨⟨inferInstance, rfl.le⟩, fun _ h _ => h.2⟩ +#align ideal.minimal_primes_eq_subsingleton_self Ideal.minimalPrimes_eq_subsingleton_self + +end + From d00745164535935eb5cdf66deb84c47956f8de79 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 09:53:40 -0500 Subject: [PATCH 03/22] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/RingTheory/Ideal/MinimalPrime.lean | 46 ++++++++-------------- 2 files changed, 17 insertions(+), 30 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index a878a30f10ec1..d3842c20c5923 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1853,6 +1853,7 @@ import Mathlib.RingTheory.Ideal.AssociatedPrime import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.IdempotentFG import Mathlib.RingTheory.Ideal.LocalRing +import Mathlib.RingTheory.Ideal.MinimalPrime import Mathlib.RingTheory.Ideal.Operations import Mathlib.RingTheory.Ideal.Prod import Mathlib.RingTheory.Ideal.Quotient diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 5a078d944e6b6..df570ee7bdcdb 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -8,8 +8,8 @@ Authors: Andrew Yang ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.RingTheory.Localization.AtPrime -import Mathbin.Order.Minimal +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.Order.Minimal /-! @@ -50,12 +50,10 @@ def minimalPrimes (R : Type _) [CommRing R] : Set (Ideal R) := variable {I J} -theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J := - by +theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.minimalPrimes, p ≤ J := by suffices ∃ m ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ OrderDual.ofDual p }, - OrderDual.toDual J ≤ m ∧ ∀ z ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p }, m ≤ z → z = m - by + OrderDual.toDual J ≤ m ∧ ∀ z ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p }, m ≤ z → z = m by obtain ⟨p, h₁, h₂, h₃⟩ := this simp_rw [← @eq_comm _ p] at h₃ exact ⟨p, ⟨h₁, fun a b c => (h₃ a b c).le⟩, h₂⟩ @@ -76,8 +74,7 @@ theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.mi #align ideal.exists_minimal_primes_le Ideal.exists_minimalPrimes_le @[simp] -theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes := - by +theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes := by rw [Ideal.minimalPrimes, Ideal.minimalPrimes] congr ext p @@ -85,8 +82,7 @@ theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes #align ideal.radical_minimal_primes Ideal.radical_minimalPrimes @[simp] -theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := - by +theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := by rw [I.radical_eq_Inf] apply le_antisymm · intro x hx @@ -103,11 +99,9 @@ theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » minimal_primes[minimal_primes] R) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} (hf : Function.Injective f) (p) (_ : p ∈ minimalPrimes R) : - ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := - by + ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := by haveI := H.1.1 - have : Nontrivial (Localization (Submonoid.map f p.prime_compl)) := - by + have : Nontrivial (Localization (Submonoid.map f p.prime_compl)) := by refine' ⟨⟨1, 0, _⟩⟩ convert(IsLocalization.map_injective_of_injective p.prime_compl (Localization.AtPrime p) (Localization <| p.prime_compl.map f) hf).Ne @@ -133,16 +127,13 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) - (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := - by + (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := by haveI := H.1.1 let f' := I.Quotient.mk.comp f - have e : (I.Quotient.mk.comp f).ker = I.comap f := - by + have e : (I.Quotient.mk.comp f).ker = I.comap f := by ext1 exact Submodule.Quotient.mk_eq_zero _ - have : (I.Quotient.mk.comp f).ker.Quotient.mk.ker ≤ p := - by + have : (I.Quotient.mk.comp f).ker.Quotient.mk.ker ≤ p := by rw [Ideal.mk_ker, e] exact H.1.2 obtain ⟨p', hp₁, hp₂⟩ := @@ -173,8 +164,7 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) - (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := - by + (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := by obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H skip obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂ @@ -185,8 +175,7 @@ theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) #align ideal.exists_minimal_primes_comap_eq Ideal.exists_minimalPrimes_comap_eq theorem Ideal.mimimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f) - {I J : Ideal S} (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes := - by + {I J : Ideal S} (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes := by haveI := h.1.1 refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩ rintro K ⟨hK, e₁⟩ e₂ @@ -199,8 +188,7 @@ theorem Ideal.mimimal_primes_comap_of_surjective {f : R →+* S} (hf : Function. #align ideal.mimimal_primes_comap_of_surjective Ideal.mimimal_primes_comap_of_surjective theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Function.Surjective f) - (I : Ideal S) : (I.comap f).minimalPrimes = Ideal.comap f '' I.minimalPrimes := - by + (I : Ideal S) : (I.comap f).minimalPrimes = Ideal.comap f '' I.minimalPrimes := by ext J constructor · intro H @@ -216,8 +204,7 @@ theorem Ideal.minimalPrimes_eq_comap : RingHom.ker_eq_comap_bot, Ideal.mk_ker] #align ideal.minimal_primes_eq_comap Ideal.minimalPrimes_eq_comap -theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = {I.radical} := - by +theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = {I.radical} := by ext J constructor · @@ -228,8 +215,7 @@ theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes exact ⟨⟨Ideal.isPrime_radical hI, Ideal.le_radical⟩, fun _ H _ => H.1.radical_le_iff.mpr H.2⟩ #align ideal.minimal_primes_eq_subsingleton Ideal.minimalPrimes_eq_subsingleton -theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = {I} := - by +theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = {I} := by ext J constructor · exact fun H => (H.2 ⟨inferInstance, rfl.le⟩ H.1.2).antisymm H.1.2 From ba82f6227dc788da40584b6269ce7fe215e4ad6e Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 15:07:13 +0000 Subject: [PATCH 04/22] Fix proof --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index df570ee7bdcdb..7c35ae8f0d0d1 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -56,10 +56,10 @@ theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.mi OrderDual.toDual J ≤ m ∧ ∀ z ∈ { p : (Ideal R)ᵒᵈ | Ideal.IsPrime p ∧ I ≤ p }, m ≤ z → z = m by obtain ⟨p, h₁, h₂, h₃⟩ := this simp_rw [← @eq_comm _ p] at h₃ - exact ⟨p, ⟨h₁, fun a b c => (h₃ a b c).le⟩, h₂⟩ + exact ⟨p, ⟨h₁, fun a b c => le_of_eq (h₃ a b c)⟩, h₂⟩ apply zorn_nonempty_partialOrder₀ swap - · refine' ⟨show J.is_prime by infer_instance, e⟩ + · refine' ⟨show J.IsPrime by infer_instance, e⟩ rintro (c : Set (Ideal R)) hc hc' J' hJ' refine' ⟨OrderDual.toDual (Inf c), @@ -224,4 +224,3 @@ theorem Ideal.minimalPrimes_eq_subsingleton_self [I.IsPrime] : I.minimalPrimes = #align ideal.minimal_primes_eq_subsingleton_self Ideal.minimalPrimes_eq_subsingleton_self end - From 1ac3acddacc234bd16db49b750482c40a649bd65 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 16:37:51 +0000 Subject: [PATCH 05/22] Fix proof --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 7c35ae8f0d0d1..b8ac8c2fffd64 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -37,13 +37,13 @@ section variable {R S : Type _} [CommRing R] [CommRing S] (I J : Ideal R) -/-- `I.minimal_primes` is the set of ideals that are minimal primes over `I`. -/ +/-- `I.minimalPrimes` is the set of ideals that are minimal primes over `I`. -/ def Ideal.minimalPrimes : Set (Ideal R) := minimals (· ≤ ·) { p | p.IsPrime ∧ I ≤ p } #align ideal.minimal_primes Ideal.minimalPrimes -/-- `minimal_primes R` is the set of minimal primes of `R`. -This is defined as `ideal.minimal_primes ⊥`. -/ +/-- `minimalPrimes R` is the set of minimal primes of `R`. +This is defined as `Ideal.minimalPrimes ⊥`. -/ def minimalPrimes (R : Type _) [CommRing R] : Set (Ideal R) := Ideal.minimalPrimes ⊥ #align minimal_primes minimalPrimes @@ -78,7 +78,13 @@ theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes rw [Ideal.minimalPrimes, Ideal.minimalPrimes] congr ext p - exact ⟨fun ⟨a, b⟩ => ⟨a, ideal.le_radical.trans b⟩, fun ⟨a, b⟩ => ⟨a, a.radical_le_iff.mpr b⟩⟩ + refine' ⟨_, _⟩ <;> rintro ⟨⟨a, ha⟩, b⟩ + . refine' ⟨⟨a, a.radical_le_iff.1 ha⟩, _⟩ + . simp only [Set.mem_setOf_eq, and_imp] at * + exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.2 h3) h4 + . refine' ⟨⟨a, a.radical_le_iff.2 ha⟩, _⟩ + . simp only [Set.mem_setOf_eq, and_imp] at * + exact fun _ h2 h3 h4 => b h2 (h2.radical_le_iff.1 h3) h4 #align ideal.radical_minimal_primes Ideal.radical_minimalPrimes @[simp] From f464a7247cef83f0c526897cb7a9e0c296d913fa Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 16:42:16 +0000 Subject: [PATCH 06/22] Fix docs --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index b8ac8c2fffd64..63be66e1ac8eb 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -18,15 +18,15 @@ import Mathlib.Order.Minimal We provide various results concerning the minimal primes above an ideal ## Main results -- `ideal.minimal_primes`: `I.minimal_primes` is the set of ideals that are minimal primes over `I`. -- `minimal_primes`: `minimal_primes R` is the set of minimal primes of `R`. -- `ideal.exists_minimal_primes_le`: Every prime ideal over `I` contains a minimal prime over `I`. -- `ideal.radical_minimal_primes`: The minimal primes over `I.radical` are precisely +- `Ideal.minimalPrimes`: `I.minimalPrimes` is the set of ideals that are minimal primes over `I`. +- `minimalPrimes`: `minimalPrimes R` is the set of minimal primes of `R`. +- `Ideal.exists_minimalPrimes_le`: Every prime ideal over `I` contains a minimal prime over `I`. +- `Ideal.radical_minimalPrimes`: The minimal primes over `I.radical` are precisely the minimal primes over `I`. -- `ideal.Inf_minimal_primes`: The intersection of minimal primes over `I` is `I.radical`. -- `ideal.exists_minimal_primes_comap_eq` If `p` is a minimal prime over `f ⁻¹ I`, then it is the +- `Ideal.sInf_minimalPrimes`: The intersection of minimal primes over `I` is `I.radical`. +- `Ideal.exists_minimalPrimes_comap_eq` If `p` is a minimal prime over `f ⁻¹ I`, then it is the preimage of some minimal prime over `I`. -- `ideal.minimal_primes_eq_comap`: The minimal primes over `I` are precisely the preimages of +- `Ideal.minimalPrimes_eq_comap`: The minimal primes over `I` are precisely the preimages of minimal primes of `R ⧸ I`. From c1925ae1113bc5ee1f655c571117bccfcfe8271c Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 16:43:57 +0000 Subject: [PATCH 07/22] Fix name --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 63be66e1ac8eb..3e243d46a8aad 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -89,7 +89,7 @@ theorem Ideal.radical_minimalPrimes : I.radical.minimalPrimes = I.minimalPrimes @[simp] theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := by - rw [I.radical_eq_Inf] + rw [I.radical_eq_sInf] apply le_antisymm · intro x hx rw [Ideal.mem_sInf] at hx⊢ From b941aeda650ab9ead512b16310c8af02a2353ea6 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 17:02:47 +0000 Subject: [PATCH 08/22] Add missing variable names --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 3e243d46a8aad..dc9afe62e5312 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -104,9 +104,9 @@ theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := by /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » minimal_primes[minimal_primes] R) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} - (hf : Function.Injective f) (p) (_ : p ∈ minimalPrimes R) : + (hf : Function.Injective f) (p) (H : p ∈ minimalPrimes R) : ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := by - haveI := H.1.1 + have := H.1.1 have : Nontrivial (Localization (Submonoid.map f p.prime_compl)) := by refine' ⟨⟨1, 0, _⟩⟩ convert(IsLocalization.map_injective_of_injective p.prime_compl (Localization.AtPrime p) @@ -133,8 +133,8 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) - (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := by - haveI := H.1.1 + (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := by + have := H.1.1 let f' := I.Quotient.mk.comp f have e : (I.Quotient.mk.comp f).ker = I.comap f := by ext1 @@ -170,19 +170,19 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) /- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) - (_ : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := by + (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := by obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H skip obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂ refine' ⟨q, hq, Eq.symm _⟩ - haveI := hq.1.1 + have := hq.1.1 have := (Ideal.comap_mono hq').trans_eq h₃ exact (H.2 ⟨inferInstance, Ideal.comap_mono hq.1.2⟩ this).antisymm this #align ideal.exists_minimal_primes_comap_eq Ideal.exists_minimalPrimes_comap_eq theorem Ideal.mimimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f) {I J : Ideal S} (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes := by - haveI := h.1.1 + have := h.1.1 refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩ rintro K ⟨hK, e₁⟩ e₂ have : f.ker ≤ K := (Ideal.comap_mono bot_le).trans e₁ From 10dcf689de74e26d408c4ddfbde919e5bedba86f Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 17:08:56 +0000 Subject: [PATCH 09/22] Fix capitalizaion --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index dc9afe62e5312..7bb447a45050e 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -107,18 +107,18 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} (hf : Function.Injective f) (p) (H : p ∈ minimalPrimes R) : ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := by have := H.1.1 - have : Nontrivial (Localization (Submonoid.map f p.prime_compl)) := by + have : Nontrivial (Localization (Submonoid.map f p.primeCompl)) := by refine' ⟨⟨1, 0, _⟩⟩ - convert(IsLocalization.map_injective_of_injective p.prime_compl (Localization.AtPrime p) - (Localization <| p.prime_compl.map f) hf).Ne + convert(IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p) + (Localization <| p.primeCompl.map f) hf).Ne one_ne_zero · rw [map_one] · rw [map_zero] - obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.prime_compl)) + obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl)) skip - refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.prime_compl)), inferInstance, _⟩ + refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩ rw [Ideal.comap_comap, ← - @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.prime_compl.le_comap_map _ + @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.primeCompl.le_comap_map _ Localization.isLocalization, ← Ideal.comap_comap] suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this) @@ -127,7 +127,7 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} apply hM.ne_top apply M.eq_top_of_is_unit_mem hx apply IsUnit.map - apply IsLocalization.map_units _ (show p.prime_compl from ⟨x, h⟩) + apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩) infer_instance #align ideal.exists_comap_eq_of_mem_minimal_primes_of_injective Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective From 64963d638332f1e883a65d4f2fa8a5563b2ca517 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 17:58:37 +0000 Subject: [PATCH 10/22] Add protected --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 7bb447a45050e..39ba78bb99e6a 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -38,7 +38,7 @@ section variable {R S : Type _} [CommRing R] [CommRing S] (I J : Ideal R) /-- `I.minimalPrimes` is the set of ideals that are minimal primes over `I`. -/ -def Ideal.minimalPrimes : Set (Ideal R) := +protected def Ideal.minimalPrimes : Set (Ideal R) := minimals (· ≤ ·) { p | p.IsPrime ∧ I ≤ p } #align ideal.minimal_primes Ideal.minimalPrimes From e4b309724fbea06be6bb9e6bc7f8caeeb50dd0c0 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:03:17 +0000 Subject: [PATCH 11/22] Inf -> sInf --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 39ba78bb99e6a..ff3c757dd1cda 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -62,7 +62,7 @@ theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.mi · refine' ⟨show J.IsPrime by infer_instance, e⟩ rintro (c : Set (Ideal R)) hc hc' J' hJ' refine' - ⟨OrderDual.toDual (Inf c), + ⟨OrderDual.toDual (sInf c), ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩ · rw [OrderDual.ofDual_toDual] convert le_sInf _ From 51664ddecee15c49327e875e2edc68c1e3f3e3d3 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:16:06 +0000 Subject: [PATCH 12/22] Fix proof --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index ff3c757dd1cda..64911fcb52e85 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -64,10 +64,8 @@ theorem Ideal.exists_minimalPrimes_le [J.IsPrime] (e : I ≤ J) : ∃ p ∈ I.mi refine' ⟨OrderDual.toDual (sInf c), ⟨Ideal.sInf_isPrime_of_isChain ⟨J', hJ'⟩ hc'.symm fun x hx => (hc hx).1, _⟩, _⟩ - · rw [OrderDual.ofDual_toDual] - convert le_sInf _ - intro x hx - exact (hc hx).2 + · rw [OrderDual.ofDual_toDual, le_sInf_iff] + exact fun _ hx => (hc hx).2 · rintro z hz rw [OrderDual.le_toDual] exact sInf_le hz From 2d5ce2e0a14dcc2c2d51c98f1ed58d8df02ab709 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:30:09 +0000 Subject: [PATCH 13/22] Minor fixes --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 64911fcb52e85..4a872af6daeef 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -133,8 +133,8 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := by have := H.1.1 - let f' := I.Quotient.mk.comp f - have e : (I.Quotient.mk.comp f).ker = I.comap f := by + let f' := (Ideal.Quotient.mk I).comp f + have e : RingHom.ker f' = I.comap f := by ext1 exact Submodule.Quotient.mk_eq_zero _ have : (I.Quotient.mk.comp f).ker.Quotient.mk.ker ≤ p := by From f3e9ba32c9ee6ce306d72891c0e40817de28353c Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:30:45 +0000 Subject: [PATCH 14/22] Fix linter errors --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 4a872af6daeef..8f8bef1428f24 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -100,7 +100,6 @@ theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := by exact hI.1.symm #align ideal.Inf_minimal_primes Ideal.sInf_minimalPrimes -/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » minimal_primes[minimal_primes] R) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} (hf : Function.Injective f) (p) (H : p ∈ minimalPrimes R) : ∃ p' : Ideal S, p'.IsPrime ∧ p'.comap f = p := by @@ -129,7 +128,6 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} infer_instance #align ideal.exists_comap_eq_of_mem_minimal_primes_of_injective Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective -/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' : Ideal S, p'.IsPrime ∧ I ≤ p' ∧ p'.comap f = p := by have := H.1.1 @@ -166,7 +164,6 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) exacts[sup_le rfl.le this, Ideal.Quotient.mk_surjective] #align ideal.exists_comap_eq_of_mem_minimal_primes Ideal.exists_comap_eq_of_mem_minimalPrimes -/- ./././Mathport/Syntax/Translate/Basic.lean:635:2: warning: expanding binder collection (p «expr ∈ » (I.comap f).minimal_primes) -/ theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := by obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H From 8dc89b3d6dd198e89560f7b4de95907d3fced685 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:43:36 +0000 Subject: [PATCH 15/22] Fix proofs --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 8f8bef1428f24..8e259a1552c5a 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -135,12 +135,12 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) have e : RingHom.ker f' = I.comap f := by ext1 exact Submodule.Quotient.mk_eq_zero _ - have : (I.Quotient.mk.comp f).ker.Quotient.mk.ker ≤ p := by + have : RingHom.ker (Ideal.Quotient.mk (RingHom.ker f')) ≤ p := by rw [Ideal.mk_ker, e] exact H.1.2 obtain ⟨p', hp₁, hp₂⟩ := - Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective - (I.Quotient.mk.comp f).ker_lift_injective (p.map (I.Quotient.mk.comp f).ker.Quotient.mk) _ + Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective _ + (RingHom.kerLift_injective f' (p.map (Ideal.Quotient.mk (RingHom.ker f'))) _ · skip refine' ⟨p'.comap I.Quotient.mk, Ideal.IsPrime.comap _, _, _⟩ · exact ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) @@ -180,7 +180,7 @@ theorem Ideal.mimimal_primes_comap_of_surjective {f : R →+* S} (hf : Function. have := h.1.1 refine' ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, _⟩ rintro K ⟨hK, e₁⟩ e₂ - have : f.ker ≤ K := (Ideal.comap_mono bot_le).trans e₁ + have : RingHom.ker f ≤ K := (Ideal.comap_mono bot_le).trans e₁ rw [← sup_eq_left.mpr this, RingHom.ker_eq_comap_bot, ← Ideal.comap_map_of_surjective f hf] apply Ideal.comap_mono _ apply h.2 _ _ From 22cdbda151f123470c28077b35ad3c7160f2186b Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 18:52:07 +0000 Subject: [PATCH 16/22] Revert unmatched brackets --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 8e259a1552c5a..ef9f3e06bd531 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -139,8 +139,9 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) rw [Ideal.mk_ker, e] exact H.1.2 obtain ⟨p', hp₁, hp₂⟩ := - Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective _ - (RingHom.kerLift_injective f' (p.map (Ideal.Quotient.mk (RingHom.ker f'))) _ + Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective + -- (RingHom.kerLift_injective f' (p.map (I.Quotient.mk.comp f).ker.Quotient.mk)) _ + (I.Quotient.mk.comp f).ker_lift_injective (p.map (I.Quotient.mk.comp f).ker.Quotient.mk) _ · skip refine' ⟨p'.comap I.Quotient.mk, Ideal.IsPrime.comap _, _, _⟩ · exact ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) From 7857e374592e6de1ab5da4d46cab3a3be9a88f27 Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 22:42:38 +0000 Subject: [PATCH 17/22] More fixes --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index ef9f3e06bd531..06388bf7cbf6b 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -135,20 +135,17 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) have e : RingHom.ker f' = I.comap f := by ext1 exact Submodule.Quotient.mk_eq_zero _ - have : RingHom.ker (Ideal.Quotient.mk (RingHom.ker f')) ≤ p := by + have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p := by rw [Ideal.mk_ker, e] exact H.1.2 obtain ⟨p', hp₁, hp₂⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective - -- (RingHom.kerLift_injective f' (p.map (I.Quotient.mk.comp f).ker.Quotient.mk)) _ - (I.Quotient.mk.comp f).ker_lift_injective (p.map (I.Quotient.mk.comp f).ker.Quotient.mk) _ - · skip - refine' ⟨p'.comap I.Quotient.mk, Ideal.IsPrime.comap _, _, _⟩ - · exact ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) - convert congr_arg (Ideal.comap (I.Quotient.mk.comp f).ker.Quotient.mk) hp₂ - rwa [Ideal.comap_map_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk - Ideal.Quotient.mk_surjective, - eq_comm, sup_eq_left] + (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') _ + · refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩ + · exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) + . convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂ + rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') + Ideal.Quotient.mk_surjective, eq_comm, sup_eq_left] refine' ⟨⟨_, bot_le⟩, _⟩ · apply Ideal.map_isPrime_of_surjective _ this exact Ideal.Quotient.mk_surjective From 11e93a34f301f8c81bfb94cfd284ac755e1a1d0b Mon Sep 17 00:00:00 2001 From: Apurva Nakade Date: Sat, 20 May 2023 22:44:01 +0000 Subject: [PATCH 18/22] Fix --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 06388bf7cbf6b..e3e815349bcf8 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -198,7 +198,7 @@ theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Functio #align ideal.comap_minimal_primes_eq_of_surjective Ideal.comap_minimalPrimes_eq_of_surjective theorem Ideal.minimalPrimes_eq_comap : - I.minimalPrimes = Ideal.comap I.Quotient.mk '' minimalPrimes (R ⧸ I) := by + I.minimalPrimes = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I) := by rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker] #align ideal.minimal_primes_eq_comap Ideal.minimalPrimes_eq_comap From b6caefbfe9da5069b23045c6403133164d0a176d Mon Sep 17 00:00:00 2001 From: int-y1 Date: Sat, 20 May 2023 23:34:19 -0700 Subject: [PATCH 19/22] fix `Ne`, define `Localization.isLocalization` --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 20 +++++++------------- Mathlib/RingTheory/Localization/Basic.lean | 2 +- 2 files changed, 8 insertions(+), 14 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index e3e815349bcf8..edfd39f8fe031 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -92,7 +92,6 @@ theorem Ideal.sInf_minimalPrimes : sInf I.minimalPrimes = I.radical := by · intro x hx rw [Ideal.mem_sInf] at hx⊢ rintro J ⟨e, hJ⟩ - skip obtain ⟨p, hp, hp'⟩ := Ideal.exists_minimalPrimes_le e exact hp' (hx hp) · apply sInf_le_sInf _ @@ -106,16 +105,14 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} have := H.1.1 have : Nontrivial (Localization (Submonoid.map f p.primeCompl)) := by refine' ⟨⟨1, 0, _⟩⟩ - convert(IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p) - (Localization <| p.primeCompl.map f) hf).Ne - one_ne_zero + convert (IsLocalization.map_injective_of_injective p.primeCompl (Localization.AtPrime p) + (Localization <| p.primeCompl.map f) hf).ne one_ne_zero · rw [map_one] · rw [map_zero] obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl)) - skip refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩ - rw [Ideal.comap_comap, ← - @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.primeCompl.le_comap_map _ + rw [Ideal.comap_comap, + ← @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.primeCompl.le_comap_map _ Localization.isLocalization, ← Ideal.comap_comap] suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this) @@ -150,11 +147,9 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) · apply Ideal.map_isPrime_of_surjective _ this exact Ideal.Quotient.mk_surjective · rintro q ⟨hq, -⟩ hq' - rw [← - Ideal.map_comap_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk + rw [← Ideal.map_comap_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk Ideal.Quotient.mk_surjective q] apply Ideal.map_mono - skip apply H.2 · refine' ⟨inferInstance, (ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩ · refine' (Ideal.comap_mono hq').trans _ @@ -165,7 +160,6 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) theorem Ideal.exists_minimalPrimes_comap_eq {I : Ideal S} (f : R →+* S) (p) (H : p ∈ (I.comap f).minimalPrimes) : ∃ p' ∈ I.minimalPrimes, Ideal.comap f p' = p := by obtain ⟨p', h₁, h₂, h₃⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes f p H - skip obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le h₂ refine' ⟨q, hq, Eq.symm _⟩ have := hq.1.1 @@ -199,8 +193,8 @@ theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Functio theorem Ideal.minimalPrimes_eq_comap : I.minimalPrimes = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I) := by - rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, ← - RingHom.ker_eq_comap_bot, Ideal.mk_ker] + rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective, + ← RingHom.ker_eq_comap_bot, Ideal.mk_ker] #align ideal.minimal_primes_eq_comap Ideal.minimalPrimes_eq_comap theorem Ideal.minimalPrimes_eq_subsingleton (hI : I.IsPrimary) : I.minimalPrimes = {I.radical} := by diff --git a/Mathlib/RingTheory/Localization/Basic.lean b/Mathlib/RingTheory/Localization/Basic.lean index fff3450d49176..8477845b6949a 100644 --- a/Mathlib/RingTheory/Localization/Basic.lean +++ b/Mathlib/RingTheory/Localization/Basic.lean @@ -1005,7 +1005,7 @@ instance {S : Type _} [CommSemiring S] [Algebra S R] : Algebra S (Localization M simp only [← mk_one_eq_monoidOf_mk, mk_mul, Localization.smul_mk, one_mul, mul_one, Algebra.commutes] -instance : IsLocalization M (Localization M) where +instance isLocalization : IsLocalization M (Localization M) where map_units' := (Localization.monoidOf M).map_units surj' := (Localization.monoidOf M).surj eq_iff_exists' := (Localization.monoidOf M).eq_iff_exists From c7d70303918b5ea4072faefadec8ab48e70e1181 Mon Sep 17 00:00:00 2001 From: int-y1 Date: Sun, 21 May 2023 00:02:28 -0700 Subject: [PATCH 20/22] fix error with `@IsLocalization.map_comp` --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index edfd39f8fe031..95589a31a767a 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -111,18 +111,16 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective {f : R →+* S} · rw [map_zero] obtain ⟨M, hM⟩ := Ideal.exists_maximal (Localization (Submonoid.map f p.primeCompl)) refine' ⟨M.comap (algebraMap S <| Localization (Submonoid.map f p.primeCompl)), inferInstance, _⟩ - rw [Ideal.comap_comap, - ← @IsLocalization.map_comp _ _ _ _ Localization.isLocalization _ p.primeCompl.le_comap_map _ - Localization.isLocalization, + rw [Ideal.comap_comap, ← @IsLocalization.map_comp _ _ _ _ _ _ _ _ Localization.isLocalization + _ _ _ _ p.primeCompl.le_comap_map _ Localization.isLocalization, ← Ideal.comap_comap] suffices _ ≤ p by exact this.antisymm (H.2 ⟨inferInstance, bot_le⟩ this) intro x hx by_contra h apply hM.ne_top - apply M.eq_top_of_is_unit_mem hx + apply M.eq_top_of_isUnit_mem hx apply IsUnit.map apply IsLocalization.map_units _ (show p.primeCompl from ⟨x, h⟩) - infer_instance #align ideal.exists_comap_eq_of_mem_minimal_primes_of_injective Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) (p) From 5d245868c2d3b372bb71e1e6f18760b2058a44ba Mon Sep 17 00:00:00 2001 From: int-y1 Date: Sun, 21 May 2023 00:15:37 -0700 Subject: [PATCH 21/22] fix `exists_comap_eq_of_mem_minimalPrimes` --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index 95589a31a767a..c4d20fe6210c8 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -133,23 +133,24 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p := by rw [Ideal.mk_ker, e] exact H.1.2 - obtain ⟨p', hp₁, hp₂⟩ := - Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective - (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') _ - · refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩ + suffices map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f') by + have ⟨p', hp₁, hp₂⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective + (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this + refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩ · exact Ideal.mk_ker.symm.trans_le (Ideal.comap_mono bot_le) . convert congr_arg (Ideal.comap <| Ideal.Quotient.mk <| RingHom.ker f') hp₂ - rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') + rwa [Ideal.comap_map_of_surjective (Ideal.Quotient.mk <| RingHom.ker f') Ideal.Quotient.mk_surjective, eq_comm, sup_eq_left] refine' ⟨⟨_, bot_le⟩, _⟩ · apply Ideal.map_isPrime_of_surjective _ this exact Ideal.Quotient.mk_surjective · rintro q ⟨hq, -⟩ hq' - rw [← Ideal.map_comap_of_surjective (I.Quotient.mk.comp f).ker.Quotient.mk + rw [← Ideal.map_comap_of_surjective + (Ideal.Quotient.mk (RingHom.ker ((Ideal.Quotient.mk I).comp f))) Ideal.Quotient.mk_surjective q] apply Ideal.map_mono apply H.2 - · refine' ⟨inferInstance, (ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩ + · refine' ⟨inferInstance, (Ideal.mk_ker.trans e).symm.trans_le (Ideal.comap_mono bot_le)⟩ · refine' (Ideal.comap_mono hq').trans _ rw [Ideal.comap_map_of_surjective] exacts[sup_le rfl.le this, Ideal.Quotient.mk_surjective] From f8b2e9a9285d29353e145cb35a1421fa42004ab5 Mon Sep 17 00:00:00 2001 From: int-y1 Date: Sun, 21 May 2023 00:17:49 -0700 Subject: [PATCH 22/22] golf --- Mathlib/RingTheory/Ideal/MinimalPrime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/Ideal/MinimalPrime.lean b/Mathlib/RingTheory/Ideal/MinimalPrime.lean index c4d20fe6210c8..b8db5754d8148 100644 --- a/Mathlib/RingTheory/Ideal/MinimalPrime.lean +++ b/Mathlib/RingTheory/Ideal/MinimalPrime.lean @@ -133,7 +133,7 @@ theorem Ideal.exists_comap_eq_of_mem_minimalPrimes {I : Ideal S} (f : R →+* S) have : RingHom.ker (Ideal.Quotient.mk <| RingHom.ker f') ≤ p := by rw [Ideal.mk_ker, e] exact H.1.2 - suffices map (Quotient.mk (RingHom.ker f')) p ∈ minimalPrimes (R ⧸ RingHom.ker f') by + suffices _ by have ⟨p', hp₁, hp₂⟩ := Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective (RingHom.kerLift_injective f') (p.map <| Ideal.Quotient.mk <| RingHom.ker f') this refine' ⟨p'.comap <| Ideal.Quotient.mk I, Ideal.IsPrime.comap _, _, _⟩