From 7173aefe8d9e171bac69d087b87a9276d30ba70b Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 17:43:16 +0000 Subject: [PATCH 01/21] changed type of 1 in dim_le_one_of_dimLEOne --- CommAlg/krull.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..27c3d7e 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -197,7 +197,8 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib applies only to dimension zero rings and domains of dimension 1. -/ -lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ℕ) := by +lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by + show _ → ((_ : WithBot ℕ∞) ≤ (1 : ℕ)) rw [krullDim_le_iff R 1] intro H p apply le_of_not_gt From 3c4cfeab65b8d9d4d1c07282cf30596f3d017231 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 20:28:19 +0000 Subject: [PATCH 02/21] proved dim_le_zero_iff --- CommAlg/grant.lean | 42 ++++++++++++++++++++ CommAlg/krull.lean | 97 +++++++++++++++++++++++++++++++++------------- 2 files changed, 111 insertions(+), 28 deletions(-) diff --git a/CommAlg/grant.lean b/CommAlg/grant.lean index c12b189..76a470c 100644 --- a/CommAlg/grant.lean +++ b/CommAlg/grant.lean @@ -171,6 +171,48 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : apply (IsCoatom.lt_iff H.out).mp exact hc2 --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) + +lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by + intro hp + apply IsPrime.ne_top hq + apply (IsCoatom.lt_iff hp.out).mp + exact h + +lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by + show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ + rw [krullDim_le_iff R 0] + constructor <;> intro h I + . contrapose! h + have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime) + let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R) + have hstrct : I < 𝔪p := by + apply lt_of_le_of_ne h𝔪.2 + intro hcontr + rw [hcontr] at h + exact h h𝔪.1 + use 𝔪p + show (_ : WithBot ℕ∞) > (0 : ℕ∞) + rw [_root_.lt_height_iff''] + use [I] + constructor + . exact List.chain'_singleton _ + . constructor + . intro I' hI' + simp at hI' + rwa [hI'] + . simp + . contrapose! h + change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h + rw [_root_.lt_height_iff''] at h + obtain ⟨c, _, hc2, hc3⟩ := h + norm_cast at hc3 + rw [List.length_eq_one] at hc3 + obtain ⟨𝔮, h𝔮⟩ := hc3 + use 𝔮 + specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl)) + apply not_maximal_of_lt_prime _ I.IsPrime + exact hc2 + end Krull section iSupWithBot diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 27c3d7e..d58a065 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -65,6 +65,34 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := exact I.2.1 . simp +lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + rcases n with _ | n + . constructor <;> intro h <;> exfalso + . exact (not_le.mpr h) le_top + . tauto + have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by + symm + show (n + 1 ≤ m ↔ _ ) + apply ENat.add_one_le_iff + exact ENat.coe_ne_top _ + rw [this] + unfold Ideal.height + show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) + rw [{J | J < 𝔭}.le_chainHeight_iff] + show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ + constructor <;> rintro ⟨c, hc⟩ <;> use c + . tauto + . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc + norm_cast at hc + tauto + +lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : +height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + show (_ < _) ↔ _ + rw [WithBot.coe_lt_coe] + exact lt_height_iff' + #check height_le_krullDim --some propositions that would be nice to be able to eventually @@ -99,6 +127,47 @@ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : lift (Ideal.krullDim R) to ℕ∞ using h with k use k +lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by + intro hp + apply IsPrime.ne_top hq + apply (IsCoatom.lt_iff hp.out).mp + exact h + +lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by + show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ + rw [krullDim_le_iff R 0] + constructor <;> intro h I + . contrapose! h + have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime) + let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R) + have hstrct : I < 𝔪p := by + apply lt_of_le_of_ne h𝔪.2 + intro hcontr + rw [hcontr] at h + exact h h𝔪.1 + use 𝔪p + show (_ : WithBot ℕ∞) > (0 : ℕ∞) + rw [lt_height_iff''] + use [I] + constructor + . exact List.chain'_singleton _ + . constructor + . intro I' hI' + simp at hI' + rwa [hI'] + . simp + . contrapose! h + change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h + rw [lt_height_iff''] at h + obtain ⟨c, _, hc2, hc3⟩ := h + norm_cast at hc3 + rw [List.length_eq_one] at hc3 + obtain ⟨𝔮, h𝔮⟩ := hc3 + use 𝔮 + specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl)) + apply not_maximal_of_lt_prime I.IsPrime + exact hc2 + lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by constructor <;> intro h . intro I @@ -167,34 +236,6 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = -- This lemma is false! lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry -lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : -height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by - rcases n with _ | n - . constructor <;> intro h <;> exfalso - . exact (not_le.mpr h) le_top - . tauto - have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by - symm - show (n + 1 ≤ m ↔ _ ) - apply ENat.add_one_le_iff - exact ENat.coe_ne_top _ - rw [this] - unfold Ideal.height - show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) - rw [{J | J < 𝔭}.le_chainHeight_iff] - show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ - constructor <;> rintro ⟨c, hc⟩ <;> use c - . tauto - . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc - norm_cast at hc - tauto - -lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : -height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by - show (_ < _) ↔ _ - rw [WithBot.coe_lt_coe] - exact lt_height_iff' - /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib applies only to dimension zero rings and domains of dimension 1. -/ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by From 46908891497cd2510c470a563e127b48843a2b76 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 21:35:36 +0000 Subject: [PATCH 03/21] proved dim_eq_zero_iff --- CommAlg/krull.lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index d58a065..b2d0230 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -169,11 +169,16 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal exact hc2 lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by - constructor <;> intro h - . intro I - sorry - . sorry - + rw [←dim_le_zero_iff] + obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R + have : n ≥ 0 := zero_le n + change _ ≤ _ at this + rw [←WithBot.coe_le_coe,←hn] at this + change (0 : WithBot ℕ∞) ≤ _ at this + constructor <;> intro h' + rw [h'] + exact le_antisymm h' this + @[simp] lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by constructor From 1981cccbaf3766ca22bdbd61c9a13a8ae44a5aaf Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Wed, 14 Jun 2023 14:36:10 -0700 Subject: [PATCH 04/21] hot garbage test file --- CommAlg/Leo.lean | 207 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 207 insertions(+) create mode 100644 CommAlg/Leo.lean diff --git a/CommAlg/Leo.lean b/CommAlg/Leo.lean new file mode 100644 index 0000000..ceb6002 --- /dev/null +++ b/CommAlg/Leo.lean @@ -0,0 +1,207 @@ +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Basic +import CommAlg.krull + +--trying and failing to prove ht p = dim R_p +section Localization + +variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) +variable {S : Type _} [CommRing S] [Algebra R S] [IsLocalization.AtPrime S I.asIdeal] + +open Ideal +open LocalRing +open PrimeSpectrum + +#check algebraMap R (Localization.AtPrime I.asIdeal) +#check PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) + +#check krullDim +#check dim_eq_bot_iff +#check height_le_krullDim + +variable (J₁ J₂ : PrimeSpectrum (Localization.AtPrime I.asIdeal)) +example (h : J₁ ≤ J₂) : PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₁ ≤ + PrimeSpectrum.comap (algebraMap R (Localization.AtPrime I.asIdeal)) J₂ := by + intro x hx + exact h hx + +def gadslfasd' : Ideal S := (IsLocalization.AtPrime.localRing S I.asIdeal).maximalIdeal + +-- instance gadslfasd : LocalRing S := IsLocalization.AtPrime.localRing S I.asIdeal + +example (f : α → β) (hf : Function.Injective f) (h : a₁ ≠ a₂) : f a₁ ≠ f a₂ := by library_search + +instance map_prime (J : PrimeSpectrum R) (hJ : J ≤ I) : + (Ideal.map (algebraMap R S) J.asIdeal : Ideal S).IsPrime where + ne_top' := by + intro h + rw [eq_top_iff_one, map, mem_span] at h + mem_or_mem' := sorry + +lemma comap_lt_of_lt (J₁ J₂ : PrimeSpectrum S) (J_lt : J₁ < J₂) : + PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂ := by + apply lt_of_le_of_ne + apply comap_mono (le_of_lt J_lt) + sorry + +lemma lt_of_comap_lt (J₁ J₂ : PrimeSpectrum S) +(hJ : PrimeSpectrum.comap (algebraMap R S) J₁ < PrimeSpectrum.comap (algebraMap R S) J₂) : +J₁ < J₂ := by + apply lt_of_le_of_ne + sorry + +/- If S = R_p, then height p = dim S -/ +lemma height_eq_height_comap (J : PrimeSpectrum S) : + height (PrimeSpectrum.comap (algebraMap R S) J) = height J := by + simp [height] + have H : {J_1 | J_1 < (PrimeSpectrum.comap (algebraMap R S)) J} = + (PrimeSpectrum.comap (algebraMap R S))'' {J_2 | J_2 < J} + . sorry + rw [H] + apply Set.chainHeight_image + intro x y + constructor + apply comap_lt_of_lt + apply lt_of_comap_lt + +lemma disjoint_primeCompl (I : PrimeSpectrum R) : + { p | Disjoint (I.asIdeal.primeCompl : Set R) p.asIdeal} = {p | p ≤ I} := by + ext p; apply Set.disjoint_compl_left_iff_subset + +theorem localizationPrime_comap_range [Algebra R S] (I : PrimeSpectrum R) [IsLocalization.AtPrime S I.asIdeal] : + Set.range (PrimeSpectrum.comap (algebraMap R S)) = { p | p ≤ I} := by + rw [← disjoint_primeCompl] + apply localization_comap_range + + +#check Set.chainHeight_image + +lemma height_eq_dim_localization : height I = krullDim S := by + --first show height I = height gadslfasd' + simp [@krullDim_eq_height _ _ (IsLocalization.AtPrime.localRing S I.asIdeal)] + simp [height] + let f := (PrimeSpectrum.comap (algebraMap R S)) + have H : {J | J < I} = f '' {J | J < closedPoint S} + +lemma height_eq_dim_localization' : + height I = krullDim (Localization.AtPrime I.asIdeal) := Ideal.height_eq_dim_localization I + +end Localization + + + + +section Polynomial + +open Ideal Polynomial +variables {R : Type _} [CommRing R] + +--given ideals I J, I ⊔ J is their sum +--given a in R, span {a} is the ideal generated by a +--the map R → R[X] is C →+* +--to show p[x] is prime, show p[x] is the kernel of the map R[x] → R → R/p +#check RingHom.ker_isPrime + +def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0) +def adjoin_x (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I) +def adjoin_x' (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where + asIdeal := adjoin_x I.asIdeal + IsPrime := RingHom.ker_isPrime _ + +@[simp] +lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by + ext x; simp [adj_x_map] + +lemma adjoin_x_eq (I : Ideal R) : adjoin_x I = I.map C ⊔ Ideal.span {X} := by + apply le_antisymm + . sorry + . rw [sup_le_iff] + constructor + . simp [adjoin_x, RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map] + . simp [span_le, adjoin_x, RingHom.mem_ker, adj_x_map] + +lemma adjoin_x_strictmono (I J : Ideal R) (h : I < J) : adjoin_x I < adjoin_x J := by + rw [lt_iff_le_and_ne] at h ⊢ + rw [adjoin_x_eq, adjoin_x_eq] + constructor + . apply sup_le_sup_right + apply map_mono h.1 + . intro H + have H' : Ideal.comap C (Ideal.map C I ⊔ span {X}) = Ideal.comap C (Ideal.map C J ⊔ span {X}) + . rw [H] + sorry + + +/- Given an ideal p in R, define the ideal p[x] in R[x] -/ +lemma ht_adjoin_x_eq_ht_add_one (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by + have H : ∀ l ∈ {J : PrimeSpectrum R | J < I}.subchain, ∃ + +lemma ne_bot_iff_exists (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by + cases' n with n; + simp + intro x hx + cases hx + simp + use n + rfl + +lemma ne_bot_iff_exists' (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by + convert WithBot.ne_bot_iff_exists using 3 + exact comm + + +lemma dim_le_dim_polynomial_add_one [Nontrivial R] : + krullDim R + (1 : ℕ∞) ≤ krullDim (Polynomial R) := by + cases' krullDim_nonneg_of_nontrivial R with n hn + rw [hn] + change ↑(n + 1) ≤ krullDim R[X] + have hn' := le_of_eq hn.symm + rw [le_krullDim_iff'] at hn' ⊢ + cases' hn' with I hI + use adjoin_x' I + apply WithBot.coe_mono + calc n + 1 ≤ height I + 1 := by + apply add_le_add_right + rw [WithBot.coe_le_coe] at hI + exact hI + _ ≤ height (adjoin_x' I) := ht_adjoin_x_eq_ht_add_one I + + +end Polynomial + +open Ideal + +variable {R : Type _} [CommRing R] + +lemma height_le_top_iff_exists {I : PrimeSpectrum R} (hI : height I ≤ ⊤) : + ∃ n : ℕ, true := by + sorry + +lemma eq_of_height_eq_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) (hJ : height J < ⊤) + (ht_eq : height I = height J) : I = J := by + by_cases h : I = J + . exact h + . have I_lt_J := lt_of_le_of_ne I_le_J h + exfalso + sorry + +section Quotient + +variables {R : Type _} [CommRing R] (I : Ideal R) + +#check List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I + +lemma comap_chain {l : List (PrimeSpectrum (R ⧸ I))} (hl : l.Chain' (· < ·)) : + List.Chain' (. < .) ((List.map <| PrimeSpectrum.comap <| Ideal.Quotient.mk I) l) := by + + +lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by + +end Quotient \ No newline at end of file From 08711d7689ae4112d2d6e6a5297b512d8b3ccab9 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Wed, 14 Jun 2023 22:36:08 +0000 Subject: [PATCH 05/21] not_maximal_of_lt_prime in dim_le_one_of_dimLEOne --- CommAlg/krull.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 8da4d27..83902bb 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -176,8 +176,8 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum rw [←WithBot.coe_le_coe,←hn] at this change (0 : WithBot ℕ∞) ≤ _ at this constructor <;> intro h' - rw [h'] - exact le_antisymm h' this + . rw [h'] + . exact le_antisymm h' this @[simp] lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by @@ -259,9 +259,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by change q0.asIdeal < q1.asIdeal at hc1 have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1 specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime - apply IsPrime.ne_top p.IsPrime - apply (IsCoatom.lt_iff H.out).mp - exact hc2 + exact (not_maximal_of_lt_prime p.IsPrime hc2) H lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] From 70007679cd8079faeb686adee1dbe8786c5bc42d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 17:01:34 -0700 Subject: [PATCH 06/21] Trying to break it down to smaller parts --- CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index 089c4b5..b321c4d 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -3,9 +3,11 @@ import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Ideal.MinimalPrime import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic +import Mathlib.Data.Set.Ncard namespace Ideal @@ -24,6 +26,13 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] : lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file +lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : height P ≠ ⊤ := by + sorry + +lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : + ∃S : Set R, Set.ncard s = height P ∧ P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S) := by + sorry + lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by rw [le_antisymm_iff] @@ -43,6 +52,7 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have : height P ≤ height P' := height_le_of_le PleP' simp only [WithBot.coe_le_coe] have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by + -- Prime avoidance is called subset_union_prime sorry obtain ⟨I, h⟩ := this From 89d7be5bc9a03189dd345fd63db0a8d4f7bac552 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Thu, 15 Jun 2023 00:40:57 +0000 Subject: [PATCH 07/21] added docstrings to krull.lean --- CommAlg/krull.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 83902bb..b4227aa 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -55,6 +55,7 @@ lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I +/-- The Krull dimension of a local ring is the height of its maximal ideal. -/ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by apply le_antisymm . rw [krullDim_le_iff'] @@ -65,6 +66,8 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := exact I.2.1 . simp only [height_le_krullDim] +/-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭` + with length `n + 1`. -/ lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by rcases n with _ | n @@ -87,6 +90,7 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ norm_cast at hc tauto +/-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by show (_ < _) ↔ _ @@ -96,9 +100,11 @@ height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' #check height_le_krullDim --some propositions that would be nice to be able to eventually +/-- The prime spectrum of the zero ring is empty. -/ lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False := x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem +/-- A CommRing has empty prime spectrum if and only if it is the zero ring. -/ lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by constructor . contrapose @@ -122,17 +128,20 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial +/-- Nonzero rings have Krull dimension in ℕ∞ -/ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by have h := dim_eq_bot_iff.not.mpr (not_subsingleton R) lift (Ideal.krullDim R) to ℕ∞ using h with k use k +/-- An ideal which is less than a prime is not a maximal ideal. -/ lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by intro hp apply IsPrime.ne_top hq apply (IsCoatom.lt_iff hp.out).mp exact h +/-- Krull dimension is ≤ 0 if and only if all primes are maximal. -/ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by show ((_ : WithBot ℕ∞) ≤ (0 : ℕ)) ↔ _ rw [krullDim_le_iff R 0] @@ -168,6 +177,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal apply not_maximal_of_lt_prime I.IsPrime exact hc2 +/-- For a nonzero ring, Krull dimension is 0 if and only if all primes are maximal. -/ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by rw [←dim_le_zero_iff] obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R @@ -179,6 +189,7 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum . rw [h'] . exact le_antisymm h' this +/-- In a field, the unique prime ideal is the zero ideal. -/ @[simp] lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by constructor @@ -190,6 +201,7 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = rw [botP] exact bot_prime +/-- In a field, all primes have height 0. -/ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by unfold height simp @@ -205,10 +217,12 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig have : J ≠ P := ne_of_lt JlP contradiction +/-- The Krull dimension of a field is 0. -/ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] +/-- A domain with Krull dimension 0 is a field. -/ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by by_contra x rw [Ring.not_isField_iff_exists_prime] at x @@ -230,6 +244,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim aesop contradiction +/-- A domain has Krull dimension 0 if and only if it is a field. -/ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor · exact domain_dim_zero.isField @@ -261,6 +276,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime exact (not_maximal_of_lt_prime p.IsPrime hc2) H +/-- The Krull dimension of a PID is at most 1. -/ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by rw [dim_le_one_iff] exact Ring.DimensionLEOne.principal_ideal_ring R From 999659039dc32f63b8069403b791035b4da5b577 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Wed, 14 Jun 2023 19:14:01 -0700 Subject: [PATCH 08/21] more stuff --- CommAlg/jayden(krull-dim-zero).lean | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 06dc873..eba40ab 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -19,7 +19,6 @@ import Mathlib.Util.PiNotation open PiNotation - namespace Ideal variable (R : Type _) [CommRing R] (P : PrimeSpectrum R) @@ -116,13 +115,30 @@ lemma power_zero_finite_length [Ideal.IsMaximal I] (h₁ : Ideal.FG I) [Module.F -- rcases power with ⟨n, npower⟩ -- how do I get a generating set? +open Finset -- Stacks Lemma 10.53.3: R is Artinian iff R has finitely many maximal ideals lemma Artinian_has_finite_max_ideal [IsArtinianRing R] : Finite (MaximalSpectrum R) := by by_contra infinite simp only [not_finite_iff_infinite] at infinite - + let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) + have m'inj := m'.injective + let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal + have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal = + (⊤ : Ideal R) := by + intro i j distinct + apply Ideal.IsMaximal.coprime_of_ne + sorry + sorry + -- by_contra equal + have : (m' i) ≠ (m' j) := by + exact Function.Injective.ne m'inj distinct + intro h + apply this + exact MaximalSpectrum.ext _ _ h + -- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal + -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent lemma Jacobson_of_Artinian_is_nilpotent From 40e26d86367baef91942d2aa1a7c9511afea3751 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Wed, 14 Jun 2023 21:32:22 -0700 Subject: [PATCH 09/21] Hahaha --- CommAlg/jayden(krull-dim-zero).lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index eba40ab..f75912a 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -125,19 +125,23 @@ lemma Artinian_has_finite_max_ideal let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) have m'inj := m'.injective let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal + let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal + let F : Fin n → Ideal R := fun k ↦ (m' k).asIdeal have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal = (⊤ : Ideal R) := by intro i j distinct apply Ideal.IsMaximal.coprime_of_ne - sorry - sorry - -- by_contra equal + exact (m' i).IsMaximal + exact (m' j).IsMaximal have : (m' i) ≠ (m' j) := by exact Function.Injective.ne m'inj distinct intro h apply this exact MaximalSpectrum.ext _ _ h - -- let g :`= Ideal.quotientInfRingEquivPiQuotient m' comaximal + have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by + sorry + -- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal) + -- let g := Ideal.quotientInfRingEquivPiQuotient f comaximal -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent @@ -193,7 +197,7 @@ lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : constructor apply finite_length_is_Noetherian rwa [IsArtinian_iff_finite_length] at RisArtinian - sorry + sorry -- can use Grant's lemma dim_eq_zero_iff From 947c28f00147380038595fb008bb426c9772077c Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 23:51:46 -0700 Subject: [PATCH 10/21] Tried to avoid the finiteness condition on height P --- CommAlg/krull.lean | 9 +++- ...yantan(dim_eq_dim_polynomial_add_one).lean | 48 ++++++++++++------- 2 files changed, 39 insertions(+), 18 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 8da4d27..2b86416 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -4,6 +4,7 @@ import Mathlib.Order.Height import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Ideal.MinimalPrime import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic @@ -270,8 +271,12 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : - krullDim R + 1 = krullDim (Polynomial R) := sorry +-- lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : +-- krullDim R + 1 = krullDim (Polynomial R) := sorry + +lemma krull_height_theorem [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) (S: Finset R) + (h: P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S)) : height P ≤ S.card := by + sorry lemma dim_mvPolynomial [Field K] (n : ℕ) : krullDim (MvPolynomial (Fin n) K) = n := sorry diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index b321c4d..94c93e2 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -8,38 +8,54 @@ import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Data.Set.Ncard +import CommAlg.krull namespace Ideal variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} -noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I -lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl -lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl -lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl +/-- +-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} +-- noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I + +-- lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl +-- lemma krullDim_def (R : Type) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl +-- lemma krullDim_def' (R : Type) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice -lemma dim_le_dim_polynomial_add_one [Nontrivial R] : - krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it +-- lemma dim_le_dim_polynomial_add_one [Nontrivial R] : +-- krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it -lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file +-- lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file -lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : height P ≠ ⊤ := by - sorry +-- lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] +-- (P: PrimeSpectrum R) : height P ≠ ⊤ := by +-- sorry +--/ -lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : +lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] + (P: PrimeSpectrum R) (h : height P < ⊤) : ∃S : Set R, Set.ncard s = height P ∧ P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S) := by sorry -lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : +lemma dim_eq_dim_polynomial_add_one [h1: Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by rw [le_antisymm_iff] constructor · exact dim_le_dim_polynomial_add_one - · unfold krullDim - have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by + · by_cases krullDim R = ⊤ + calc + krullDim (Polynomial R) ≤ ⊤ := le_top + _ ≤ krullDim R := top_le_iff.mpr h + _ ≤ krullDim R + 1 := by + apply le_of_eq + rw [h] + rfl + have h:= Ne.lt_top h + unfold krullDim + have htPBdd : ∀ (P : PrimeSpectrum (Polynomial R)), (height P : WithBot ℕ∞) + ≤ (⨆ (I : PrimeSpectrum R), ↑(height I + 1)) := by intro P have : ∃ (I : PrimeSpectrum R), (height P : WithBot ℕ∞) ≤ ↑(height I + 1) := by have : ∃ M, Ideal.IsMaximal M ∧ P.asIdeal ≤ M := by @@ -53,7 +69,6 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : simp only [WithBot.coe_le_coe] have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by -- Prime avoidance is called subset_union_prime - sorry obtain ⟨I, h⟩ := this use I @@ -62,7 +77,8 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by apply @le_iSup (WithBot ℕ∞) _ _ _ I exact ge_trans this IP - have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by + have oneOut : (⨆ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) + 1) + ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by have : ∀ P : PrimeSpectrum R, (height P : WithBot ℕ∞) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := fun P ↦ (by apply add_le_add_right (@le_iSup (WithBot ℕ∞) _ _ _ P) 1) apply iSup_le From 4e819719a62247ea1349ded767f63b528f448476 Mon Sep 17 00:00:00 2001 From: Sameer Savkar Date: Thu, 15 Jun 2023 10:26:31 -0700 Subject: [PATCH 11/21] Implemented FieldisArtinian lemma --- CommAlg/sameer(artinian-rings).lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/CommAlg/sameer(artinian-rings).lean b/CommAlg/sameer(artinian-rings).lean index 417cc96..e619c07 100644 --- a/CommAlg/sameer(artinian-rings).lean +++ b/CommAlg/sameer(artinian-rings).lean @@ -6,10 +6,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.RingTheory.DedekindDomain.DVR -lemma FieldisArtinian (R : Type _) [CommRing R] (h: IsField R) : - IsArtinianRing R := by sorry - - +lemma FieldisArtinian (R : Type _) [CommRing R] (h : IsField R) : + IsArtinianRing R := by + let inst := h.toField + rw [isArtinianRing_iff, isArtinian_iff_wellFounded] + apply WellFounded.intro + intro I + constructor + intro J hJI + constructor + intro K hKJ + exfalso + rcases Ideal.eq_bot_or_top J with rfl | rfl + . exact not_lt_bot hKJ + . exact not_top_lt hJI lemma ArtinianDomainIsField (R : Type _) [CommRing R] [IsDomain R] (IsArt : IsArtinianRing R) : IsField (R) := by From 2d5a7d3deb013b9a9b1325ef6f3e505b72776bc8 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Thu, 15 Jun 2023 20:35:28 +0000 Subject: [PATCH 12/21] defined codimension of an ideal --- CommAlg/krull.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index a559b1d..e068760 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -28,6 +28,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I +noncomputable def codimension (J : Ideal R) : WithBot ℕ∞ := ⨅ I ∈ {I : PrimeSpectrum R | J ≤ I.asIdeal}, height I + lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl lemma krullDim_def (R : Type _) [CommRing R] : krullDim R = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl From e93a53bd67732c7b09ea41d2d5a60b573b8724b4 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 15:18:22 -0700 Subject: [PATCH 13/21] Proved le_krullDim_iff --- CommAlg/krull.lean | 54 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 47 insertions(+), 7 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index a559b1d..bd9edb4 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,11 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic developed. -/ +lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by + cases a + . rfl + . cases h.not_le (WithBot.coe_le_coe.2 bot_le) + namespace Ideal open LocalRing @@ -46,16 +51,51 @@ lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) : lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) : krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞) -lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : - n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry - -lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : - n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry - @[simp] lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I +lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by + constructor + · unfold krullDim + intro H + by_contra H1 + push_neg at H1 + by_cases n ≤ 0 + · rw [Nat.le_zero] at h + rw [h] at H H1 + have : ∀ (I : PrimeSpectrum R), ↑(height I) = (⊥ : WithBot ℕ∞) := by + intro I + specialize H1 I + exact lt_bot_eq_WithBot_bot H1 + rw [←iSup_eq_bot] at this + have := le_of_le_of_eq H this + rw [le_bot_iff] at this + exact WithBot.coe_ne_bot this + · push_neg at h + have : (n: ℕ∞) > 0 := Nat.cast_pos.mpr h + replace H1 : ∀ (I : PrimeSpectrum R), height I ≤ n - 1 := by + intro I + specialize H1 I + apply ENat.le_of_lt_add_one + rw [←ENat.coe_one, ←ENat.coe_sub, ←ENat.coe_add, tsub_add_cancel_of_le] + exact WithBot.coe_lt_coe.mp H1 + exact h + replace H1 : ∀ (I : PrimeSpectrum R), (height I : WithBot ℕ∞) ≤ ↑(n - 1):= + fun _ ↦ (WithBot.coe_le rfl).mpr (H1 _) + rw [←iSup_le_iff] at H1 + have : ((n : ℕ∞) : WithBot ℕ∞) ≤ (((n - 1 : ℕ) : ℕ∞) : WithBot ℕ∞) := le_trans H H1 + norm_cast at this + have that : n - 1 < n := by refine Nat.sub_lt h (by norm_num) + apply lt_irrefl (n-1) (trans that this) + · rintro ⟨I, h⟩ + have : height I ≤ krullDim R := by apply height_le_krullDim + exact le_trans h this + +lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) : + n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry + /-- The Krull dimension of a local ring is the height of its maximal ideal. -/ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := by apply le_antisymm @@ -250,7 +290,7 @@ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krull constructor · exact domain_dim_zero.isField · intro fieldD - let h : Field D := IsField.toField fieldD + let h : Field D := fieldD.toField exact dim_field_eq_zero #check Ring.DimensionLEOne From c1b99a1b22b382f88d1b87b64a76e65be3252075 Mon Sep 17 00:00:00 2001 From: leopoldmayer Date: Thu, 15 Jun 2023 18:05:33 -0700 Subject: [PATCH 14/21] Finished last sorry on dim_le_dim_polynomial!!! --- CommAlg/Leo.lean | 165 +++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 146 insertions(+), 19 deletions(-) diff --git a/CommAlg/Leo.lean b/CommAlg/Leo.lean index ceb6002..10d63de 100644 --- a/CommAlg/Leo.lean +++ b/CommAlg/Leo.lean @@ -1,6 +1,7 @@ import Mathlib.RingTheory.Ideal.Operations import Mathlib.RingTheory.FiniteType import Mathlib.Order.Height +import Mathlib.RingTheory.Polynomial.Quotient import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.Ideal.Quotient @@ -9,6 +10,40 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.Order.ConditionallyCompleteLattice.Basic import CommAlg.krull +section AddToOrder + +open List hiding le_antisymm +open OrderDual + +universe u v + +variable {α β : Type _} +variable [LT α] [LT β] (s t : Set α) + +namespace Set + +theorem append_mem_subchain_iff : +l ++ l' ∈ s.subchain ↔ l ∈ s.subchain ∧ l' ∈ s.subchain ∧ ∀ a ∈ l.getLast?, ∀ b ∈ l'.head?, a < b := by + simp [subchain, chain'_append] + aesop + +end Set + +namespace List +#check Option + +theorem getLast?_map (l : List α) (f : α → β) : + (l.map f).getLast? = Option.map f (l.getLast?) := by + cases' l with a l + . rfl + induction' l with b l ih + . rfl + . simp [List.getLast?_cons_cons, ih] + + +end List +end AddToOrder + --trying and failing to prove ht p = dim R_p section Localization @@ -102,6 +137,8 @@ section Polynomial open Ideal Polynomial variables {R : Type _} [CommRing R] +variable (J : Ideal R[X]) +#check Ideal.comap C J --given ideals I J, I ⊔ J is their sum --given a in R, span {a} is the ideal generated by a @@ -109,48 +146,138 @@ variables {R : Type _} [CommRing R] --to show p[x] is prime, show p[x] is the kernel of the map R[x] → R → R/p #check RingHom.ker_isPrime -def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0) +def adj_x_map (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp constantCoeff +--def adj_x_map' (I : Ideal R) : R[X] →+* R ⧸ I := (Ideal.Quotient.mk I).comp (evalRingHom 0) def adjoin_x (I : Ideal R) : Ideal (Polynomial R) := RingHom.ker (adj_x_map I) def adjoin_x' (I : PrimeSpectrum R) : PrimeSpectrum (Polynomial R) where asIdeal := adjoin_x I.asIdeal IsPrime := RingHom.ker_isPrime _ +/- This somehow isn't in Mathlib? -/ +@[simp] +theorem span_singleton_one : span ({0} : Set R) = ⊥ := by simp only [span_singleton_eq_bot] + +theorem coeff_C_eq : RingHom.comp constantCoeff C = RingHom.id R := by ext; simp + +variable (I : PrimeSpectrum R) +#check RingHom.ker (C.comp (Ideal.Quotient.mk I.asIdeal)) +--#check Ideal.Quotient.mk I.asIdeal + +def map_prime' (I : PrimeSpectrum R) : IsPrime (I.asIdeal.map C) := Ideal.isPrime_map_C_of_isPrime I.IsPrime + +def map_prime'' (I : PrimeSpectrum R) : PrimeSpectrum R[X] := ⟨I.asIdeal.map C, map_prime' I⟩ + @[simp] lemma adj_x_comp_C (I : Ideal R) : RingHom.comp (adj_x_map I) C = Ideal.Quotient.mk I := by ext x; simp [adj_x_map] +-- ideal.mem_quotient_iff_mem_sup lemma adjoin_x_eq (I : Ideal R) : adjoin_x I = I.map C ⊔ Ideal.span {X} := by apply le_antisymm - . sorry + . rintro p hp + have h : ∃ q r, p = C r + X * q := ⟨p.divX, p.coeff 0, p.divX_mul_X_add.symm.trans $ by ring⟩ + obtain ⟨q, r, rfl⟩ := h + suffices : r ∈ I + . simp only [Submodule.mem_sup, Ideal.mem_span_singleton] + refine' ⟨C r, Ideal.mem_map_of_mem C this, X * q, ⟨q, rfl⟩, rfl⟩ + rw [adjoin_x, adj_x_map, RingHom.mem_ker, RingHom.comp_apply] at hp + rw [constantCoeff_apply, coeff_add, coeff_C_zero, coeff_X_mul_zero, add_zero] at hp + rwa [←RingHom.mem_ker, Ideal.mk_ker] at hp . rw [sup_le_iff] constructor . simp [adjoin_x, RingHom.ker, ←map_le_iff_le_comap, Ideal.map_map] . simp [span_le, adjoin_x, RingHom.mem_ker, adj_x_map] +lemma adjoin_x_inj {I J : Ideal R} (h : adjoin_x I = adjoin_x J) : I = J := by + simp [adjoin_x_eq] at h + have H : Ideal.map constantCoeff (Ideal.map C I ⊔ span {X}) = + Ideal.map constantCoeff (Ideal.map C J ⊔ span {X}) := by rw [h] + simp [Ideal.map_sup, Ideal.map_span, Ideal.map_map, coeff_C_eq] at H + exact H + + +lemma map_lt_adjoin_x (I : PrimeSpectrum R) : map_prime'' I < adjoin_x' I := by + simp [map_prime'', adjoin_x', adjoin_x_eq] + show Ideal.map C I.asIdeal < Ideal.map C I.asIdeal ⊔ span {X} + simp [Ideal.span_le, mem_map_C_iff] + use 1 + simp + intro h + apply I.IsPrime.ne_top' + rw [Ideal.eq_top_iff_one] + exact h + +lemma map_inj {I J : Ideal R} (h : I.map C = J.map C) : I = J := by + have H : Ideal.map constantCoeff (Ideal.map C I) = + Ideal.map constantCoeff (Ideal.map C J) := by rw [h] + simp [Ideal.map_map, coeff_C_eq] at H + exact H + +lemma map_strictmono (I J : Ideal R) (h : I < J) : I.map C < J.map C := by + rw [lt_iff_le_and_ne] at h ⊢ + constructor + . apply map_mono h.1 + . intro H + exact h.2 (map_inj H) + lemma adjoin_x_strictmono (I J : Ideal R) (h : I < J) : adjoin_x I < adjoin_x J := by rw [lt_iff_le_and_ne] at h ⊢ - rw [adjoin_x_eq, adjoin_x_eq] constructor - . apply sup_le_sup_right + . rw [adjoin_x_eq, adjoin_x_eq] + apply sup_le_sup_right apply map_mono h.1 . intro H - have H' : Ideal.comap C (Ideal.map C I ⊔ span {X}) = Ideal.comap C (Ideal.map C J ⊔ span {X}) - . rw [H] - sorry + exact h.2 (adjoin_x_inj H) +example (n : ℕ∞) : n + 0 = n := by simp? + +#eval List.Chain' (· < ·) [2,3] +example : [4,5] ++ [2] = [4,5,2] := rfl +#eval [2,4,5].map (λ n => n + n) /- Given an ideal p in R, define the ideal p[x] in R[x] -/ -lemma ht_adjoin_x_eq_ht_add_one (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by - have H : ∀ l ∈ {J : PrimeSpectrum R | J < I}.subchain, ∃ - -lemma ne_bot_iff_exists (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by - cases' n with n; - simp - intro x hx - cases hx - simp - use n - rfl +lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I + 1 ≤ height (adjoin_x' I) := by + suffices H : height I + (1 : ℕ) ≤ height (adjoin_x' I) + (0 : ℕ) + . norm_cast at H; rw [add_zero] at H; exact H + rw [height, height, Set.chainHeight_add_le_chainHeight_add {J | J < I} _ 1 0] + intro l hl + use ((l.map map_prime'') ++ [map_prime'' I]) + constructor + . simp [Set.append_mem_subchain_iff] + refine' ⟨_,_,_⟩ + . show (List.map map_prime'' l).Chain' (· < ·) ∧ ∀ i ∈ _, i ∈ _ + constructor + . apply List.chain'_map_of_chain' map_prime'' + intro a b hab + apply map_strictmono a.asIdeal b.asIdeal + exact hab + exact hl.1 + . intro i hi + rw [List.mem_map] at hi + obtain ⟨a, ha, rfl⟩ := hi + show map_prime'' a < adjoin_x' I + calc map_prime'' a < map_prime'' I := by apply map_strictmono; apply hl.2; apply ha + _ < adjoin_x' I := by apply map_lt_adjoin_x + . apply map_lt_adjoin_x + . intro a ha + have H : ∃ b : PrimeSpectrum R, b ∈ l ∧ map_prime'' b = a + . have H2 : l ≠ [] + . intro h + rw [h] at ha + tauto + use l.getLast H2 + refine' ⟨List.getLast_mem H2, _⟩ + have H3 : l.map map_prime'' ≠ [] + . intro hl + apply H2 + apply List.eq_nil_of_map_eq_nil hl + rw [List.getLast?_eq_getLast _ H3, Option.some_inj] at ha + simp [←ha, List.getLast_map _ H2] + obtain ⟨b, hb, rfl⟩ := H + apply map_strictmono + apply hl.2 + exact hb + . simp lemma ne_bot_iff_exists' (n : WithBot ℕ∞) : n ≠ ⊥ ↔ ∃ m : ℕ∞, n = m := by convert WithBot.ne_bot_iff_exists using 3 @@ -204,4 +331,4 @@ lemma comap_chain {l : List (PrimeSpectrum (R ⧸ I))} (hl : l.Chain' (· < ·)) lemma dim_quotient_le_dim : krullDim (R ⧸ I) ≤ krullDim R := by -end Quotient \ No newline at end of file +end Quotient From 24a0460566ef83a438757a8e3982a79770e2b4ae Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Fri, 16 Jun 2023 01:22:46 +0000 Subject: [PATCH 15/21] defined symbolicIdeal (generalized symbolic power) --- CommAlg/grant2.lean | 62 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 CommAlg/grant2.lean diff --git a/CommAlg/grant2.lean b/CommAlg/grant2.lean new file mode 100644 index 0000000..0e3092e --- /dev/null +++ b/CommAlg/grant2.lean @@ -0,0 +1,62 @@ +import Mathlib.Order.KrullDimension +import Mathlib.Order.JordanHolder +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.Height +import Mathlib.RingTheory.Noetherian +import CommAlg.krull + +variable (R : Type _) [CommRing R] [IsNoetherianRing R] + +lemma height_le_of_gt_height_lt {n : ℕ∞} (q : PrimeSpectrum R) + (h : ∀(p : PrimeSpectrum R), p < q → Ideal.height p ≤ n - 1) : Ideal.height q ≤ n := by + sorry + + +theorem height_le_one_of_minimal_over_principle (p : PrimeSpectrum R) (x : R): + p ∈ minimals (· < ·) {p | x ∈ p.asIdeal} → Ideal.height p ≤ 1 := by + intro h + apply height_le_of_gt_height_lt _ p + intro q qlep + by_contra hcontr + push_neg at hcontr + simp only [le_refl, tsub_eq_zero_of_le] at hcontr + + sorry + +#check (_ : Ideal R) ^ (_ : ℕ) +#synth Pow (Ideal R) (ℕ) + +def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where + carrier := {r : R | ∃ s : R, s ∉ Q ∧ s * r ∈ I} + zero_mem' := by + simp only [Set.mem_setOf_eq, mul_zero, Submodule.zero_mem, and_true] + use 1 + rw [←Q.ne_top_iff_one] + exact hin.ne_top + add_mem' := by + rintro a b ⟨sa, hsa1, hsa2⟩ ⟨sb, hsb1, hsb2⟩ + use sa * sb + constructor + . intro h + cases hin.mem_or_mem h <;> contradiction + ring_nf + apply I.add_mem --<;> simp only [I.mul_mem_left, hsa2, hsb2] + . rw [mul_comm sa, mul_assoc] + exact I.mul_mem_left sb hsa2 + . rw [mul_assoc] + exact I.mul_mem_left sa hsb2 + smul_mem' := by + intro c x + dsimp + rintro ⟨s, hs1, hs2⟩ + use s + constructor; exact hs1 + rw [←mul_assoc, mul_comm s, mul_assoc] + exact Ideal.mul_mem_left _ _ hs2 + +protected lemma LocalRing.height_le_one_of_minimal_over_principle + [LocalRing R] (q : PrimeSpectrum R) {x : R} + (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) : + q = closedPoint R ∨ Ideal.height q = 0 := by + + sorry \ No newline at end of file From 01bce563a54a421dd25d2ef8143ec319bc38de6e Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 19:33:24 -0700 Subject: [PATCH 16/21] One side of poly_over_field --- CommAlg/sayantan(poly_over_field).lean | 45 ++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) create mode 100644 CommAlg/sayantan(poly_over_field).lean diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean new file mode 100644 index 0000000..5379c52 --- /dev/null +++ b/CommAlg/sayantan(poly_over_field).lean @@ -0,0 +1,45 @@ +import CommAlg.krull +import Mathlib.RingTheory.Ideal.Operations +import Mathlib.RingTheory.FiniteType +import Mathlib.Order.Height +import Mathlib.RingTheory.PrincipalIdealDomain +import Mathlib.RingTheory.DedekindDomain.Basic +import Mathlib.RingTheory.Ideal.Quotient +import Mathlib.RingTheory.Ideal.MinimalPrime +import Mathlib.RingTheory.Localization.AtPrime +import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic +import Mathlib.Order.ConditionallyCompleteLattice.Basic + +namespace Ideal + +lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by + -- unfold krullDim + rw [le_antisymm_iff] + constructor + · sorry + · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) + · obtain ⟨I, h⟩ := this + have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by + apply @le_iSup (WithBot ℕ∞) _ _ _ I + exact le_trans h this + have primeX : Prime Polynomial.X := @Polynomial.prime_X K _ _ + let X := @Polynomial.X K _ + have : IsPrime (span {X}) := by + refine Iff.mpr (span_singleton_prime ?hp) primeX + exact Polynomial.X_ne_zero + let P := PrimeSpectrum.mk (span {X}) this + unfold height + use P + have : ⊥ ∈ {J | J < P} := by + simp only [Set.mem_setOf_eq] + rw [bot_lt_iff_ne_bot] + suffices : P.asIdeal ≠ ⊥ + · by_contra x + rw [PrimeSpectrum.ext_iff] at x + contradiction + by_contra x + simp only [span_singleton_eq_bot] at x + have := @Polynomial.X_ne_zero K _ _ + contradiction + have : {J | J < P}.Nonempty := Set.nonempty_of_mem this + rwa [←Set.one_le_chainHeight_iff, ←WithBot.one_le_coe] at this From e9fbb1a521ee4e39ea091544e35a44ccc7847f5c Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 19:34:20 -0700 Subject: [PATCH 17/21] Minor changes --- CommAlg/krull.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index bd9edb4..1c70814 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -86,7 +86,7 @@ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : fun _ ↦ (WithBot.coe_le rfl).mpr (H1 _) rw [←iSup_le_iff] at H1 have : ((n : ℕ∞) : WithBot ℕ∞) ≤ (((n - 1 : ℕ) : ℕ∞) : WithBot ℕ∞) := le_trans H H1 - norm_cast at this + norm_cast at this have that : n - 1 < n := by refine Nat.sub_lt h (by norm_num) apply lt_irrefl (n-1) (trans that this) · rintro ⟨I, h⟩ @@ -278,7 +278,7 @@ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this unfold height rw [←Set.one_le_chainHeight_iff] at this - exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) + exact not_le_of_gt (ENat.one_le_iff_pos.mp this) have nonpos_height : height P' ≤ 0 := by have := height_le_krullDim P' rw [h] at this From eb1e6118a05c375ee5d07150f9eedaede254e80c Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 19:36:02 -0700 Subject: [PATCH 18/21] Some changes to dim_eq_dim_poly_add_one --- CommAlg/sayantan(poly_over_field).lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 5379c52..987fe93 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -16,7 +16,8 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD -- unfold krullDim rw [le_antisymm_iff] constructor - · sorry + · + sorry · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) · obtain ⟨I, h⟩ := this have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by From 37d8991879f5fdccad630a28fe4282d042d12261 Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Thu, 15 Jun 2023 20:45:29 -0700 Subject: [PATCH 19/21] proved one direction --- CommAlg/jayden(krull-dim-zero).lean | 140 ++++++++++++++++++++++------ 1 file changed, 109 insertions(+), 31 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index f75912a..78bd648 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -16,6 +16,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic import Mathlib.Algebra.Ring.Pi import Mathlib.RingTheory.Finiteness import Mathlib.Util.PiNotation +import CommAlg.krull open PiNotation @@ -23,10 +24,10 @@ namespace Ideal variable (R : Type _) [CommRing R] (P : PrimeSpectrum R) -noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P} +-- noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < P} -noncomputable def krullDim (R : Type) [CommRing R] : - WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I +-- noncomputable def krullDim (R : Type) [CommRing R] : +-- WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height R I --variable {R} @@ -66,6 +67,8 @@ lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R ↔ TopologicalSpace.NoetherianSpace (PrimeSpectrum R) := by constructor intro RisNoetherian + sorry + sorry -- how do I apply an instance to prove one direction? @@ -99,9 +102,9 @@ lemma containment_radical_power_containment : -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is -- the same as the dimension as a vector space over R/I, -lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] - : I • (⊤ : Submodule R M) = 0 - → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry +-- lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] +-- : I • (⊤ : Submodule R M) = 0 +-- → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry -- Does lean know that M/IM is a R/I module? -- Use 10.52.5 @@ -125,30 +128,34 @@ lemma Artinian_has_finite_max_ideal let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) have m'inj := m'.injective let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal - let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal - let F : Fin n → Ideal R := fun k ↦ (m' k).asIdeal - have comaximal : ∀ i j : ℕ, i ≠ j → (m' i).asIdeal ⊔ (m' j).asIdeal = - (⊤ : Ideal R) := by - intro i j distinct - apply Ideal.IsMaximal.coprime_of_ne - exact (m' i).IsMaximal - exact (m' j).IsMaximal - have : (m' i) ≠ (m' j) := by - exact Function.Injective.ne m'inj distinct - intro h - apply this - exact MaximalSpectrum.ext _ _ h - have ∀ n : ℕ, (R ⧸ ⨅ (i : Fin n), (F n) i) ≃+* ((i : Fin n) → R ⧸ (F n) i) := by + -- let f : ℕ → MaximalSpectrum R := fun n : ℕ ↦ m' n + -- let F : (n : ℕ) → Fin n → MaximalSpectrum R := fun n k ↦ m' k + have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by + apply IsArtinian.monotone_stabilizes { + toFun := m'' + monotone' := sorry + } + cases' DCC with n DCCn + specialize DCCn (n+1) + specialize DCCn (Nat.le_succ n) + have containment1 : m'' n < (m' (n + 1)).asIdeal := by sorry + have : ∀ (j : ℕ), (j ≠ n + 1) → ∃ x, x ∈ (m' j).asIdeal ∧ x ∉ (m' (n+1)).asIdeal := by + intro j jnotn + have notcontain : ¬ (m' j).asIdeal ≤ (m' (n+1)).asIdeal := by + -- apply Ideal.IsMaximal (m' j).asIdeal + sorry sorry - -- (let F : Fin n → Ideal R := fun k : Fin n ↦ (m' k).asIdeal) - -- let g := Ideal.quotientInfRingEquivPiQuotient f comaximal - + sorry + -- have distinct : (m' j).asIdeal ≠ (m' (n+1)).asIdeal := by + -- intro h + -- apply Function.Injective.ne m'inj jnotn + -- exact MaximalSpectrum.ext _ _ h + -- simp + -- unfold + -- Stacks Lemma 10.53.4: R Artinian => Jacobson ideal of R is nilpotent -lemma Jacobson_of_Artinian_is_nilpotent - [IsArtinianRing R] : IsNilpotent (Ideal.jacobson (⊥ : Ideal R)) := by - have J := Ideal.jacobson (⊥ : Ideal R) - +-- This is in mathlib: IsArtinianRing.isNilpotent_jacobson_bot -- Stacks Lemma 10.53.5: If R has finitely many maximal ideals and -- locally nilpotent Jacobson radical, then R is the product of its localizations at @@ -187,21 +194,92 @@ lemma primes_of_Artinian_are_maximal -- Lemma: Krull dimension of a ring is the supremum of height of maximal ideals - -- Stacks Lemma 10.60.5: R is Artinian iff R is Noetherian of dimension 0 -lemma dim_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : - IsNoetherianRing R ∧ Ideal.krullDim R = 0 ↔ IsArtinianRing R := by +lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : + IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by constructor sorry intro RisArtinian constructor apply finite_length_is_Noetherian rwa [IsArtinian_iff_finite_length] at RisArtinian - sorry -- can use Grant's lemma dim_eq_zero_iff + rw [Ideal.dim_le_zero_iff] + intro I + apply primes_of_Artinian_are_maximal +-- Trash bin +-- lemma Artinian_has_finite_max_ideal +-- [IsArtinianRing R] : Finite (MaximalSpectrum R) := by +-- by_contra infinite +-- simp only [not_finite_iff_infinite] at infinite +-- let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) +-- have m'inj := m'.injective +-- let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal +-- let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal +-- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by +-- apply IsArtinian.monotone_stabilizes { +-- toFun := m'' +-- monotone' := sorry +-- } +-- cases' DCC with n DCCn +-- specialize DCCn (n+1) +-- specialize DCCn (Nat.le_succ n) +-- let F : Fin (n + 1) → MaximalSpectrum R := fun k ↦ m' k +-- have comaximal : ∀ (i j : Fin (n + 1)), (i ≠ j) → (F i).asIdeal ⊔ (F j).asIdeal = +-- (⊤ : Ideal R) := by +-- intro i j distinct +-- apply Ideal.IsMaximal.coprime_of_ne +-- exact (F i).IsMaximal +-- exact (F j).IsMaximal +-- have : (F i) ≠ (F j) := by +-- apply Function.Injective.ne m'inj +-- contrapose! distinct +-- exact Fin.ext distinct +-- intro h +-- apply this +-- exact MaximalSpectrum.ext _ _ h +-- let CRT1 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal)) +-- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) := +-- Ideal.quotientInfRingEquivPiQuotient +-- (fun i ↦ (F i).asIdeal) comaximal +-- let CRT2 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal)) +-- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) := +-- Ideal.quotientInfRingEquivPiQuotient +-- (fun i ↦ (F i).asIdeal) comaximal + + + + + -- have comaximal : ∀ (n : ℕ) (i j : Fin n), (i ≠ j) → ((F n) i).asIdeal ⊔ ((F n) j).asIdeal = + -- (⊤ : Ideal R) := by + -- intro n i j distinct + -- apply Ideal.IsMaximal.coprime_of_ne + -- exact (F n i).IsMaximal + -- exact (F n j).IsMaximal + -- have : (F n i) ≠ (F n j) := by + -- apply Function.Injective.ne m'inj + -- contrapose! distinct + -- exact Fin.ext distinct + -- intro h + -- apply this + -- exact MaximalSpectrum.ext _ _ h + -- let CRT : (n : ℕ) → (R ⧸ ⨅ (i : Fin n), ((F n) i).asIdeal) + -- ≃+* ((i : Fin n) → R ⧸ ((F n) i).asIdeal) := + -- fun n ↦ Ideal.quotientInfRingEquivPiQuotient + -- (fun i ↦ (F n i).asIdeal) (comaximal n) + -- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by + -- apply IsArtinian.monotone_stabilizes { + -- toFun := m'' + -- monotone' := sorry + -- } + -- cases' DCC with n DCCn + -- specialize DCCn (n+1) + -- specialize DCCn (Nat.le_succ n) + -- let CRT1 := CRT n + -- let CRT2 := CRT (n + 1) From 7cc1079f7d3f77b056049f89b5588e74bb28e0c9 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Fri, 16 Jun 2023 03:53:29 +0000 Subject: [PATCH 20/21] swapped inequalities in lt_height_iff --- CommAlg/krull.lean | 45 +++++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 22 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e068760..79e81c2 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -72,31 +72,32 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := /-- The height of a prime `𝔭` is greater than `n` if and only if there is a chain of primes less than `𝔭` with length `n + 1`. -/ lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : -height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by - rcases n with _ | n - . constructor <;> intro h <;> exfalso +n < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by + match n with + | ⊤ => + constructor <;> intro h <;> exfalso . exact (not_le.mpr h) le_top . tauto - have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by - symm - show (n + 1 ≤ m ↔ _ ) - apply ENat.add_one_le_iff - exact ENat.coe_ne_top _ - rw [this] - unfold Ideal.height - show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) - rw [{J | J < 𝔭}.le_chainHeight_iff] - show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ - constructor <;> rintro ⟨c, hc⟩ <;> use c - . tauto - . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc - norm_cast at hc - tauto + | (n : ℕ) => + have (m : ℕ∞) : n < m ↔ (n + 1 : ℕ∞) ≤ m := by + symm + show (n + 1 ≤ m ↔ _ ) + apply ENat.add_one_le_iff + exact ENat.coe_ne_top _ + rw [this] + unfold Ideal.height + show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ℕ) = (_:ℕ∞)) + rw [{J | J < 𝔭}.le_chainHeight_iff] + show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _ + constructor <;> rintro ⟨c, hc⟩ <;> use c + . tauto + . change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc + norm_cast at hc + tauto /-- Form of `lt_height_iff''` for rewriting with the height coerced to `WithBot ℕ∞`. -/ lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} : -height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by - show (_ < _) ↔ _ +(n : WithBot ℕ∞) < height 𝔭 ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by rw [WithBot.coe_lt_coe] exact lt_height_iff' @@ -158,7 +159,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal rw [hcontr] at h exact h h𝔪.1 use 𝔪p - show (_ : WithBot ℕ∞) > (0 : ℕ∞) + show (0 : ℕ∞) < (_ : WithBot ℕ∞) rw [lt_height_iff''] use [I] constructor @@ -169,7 +170,7 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal rwa [hI'] . simp . contrapose! h - change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h + change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h rw [lt_height_iff''] at h obtain ⟨c, _, hc2, hc3⟩ := h norm_cast at hc3 From 8eff058565edf99ccb03c3b0dc9b1c7be92f94be Mon Sep 17 00:00:00 2001 From: poincare-duality Date: Thu, 15 Jun 2023 21:34:38 -0700 Subject: [PATCH 21/21] more stuff --- CommAlg/jayden(krull-dim-zero).lean | 88 ++++------------------------- 1 file changed, 10 insertions(+), 78 deletions(-) diff --git a/CommAlg/jayden(krull-dim-zero).lean b/CommAlg/jayden(krull-dim-zero).lean index 78bd648..15dd150 100644 --- a/CommAlg/jayden(krull-dim-zero).lean +++ b/CommAlg/jayden(krull-dim-zero).lean @@ -43,7 +43,6 @@ class IsLocallyNilpotent {R : Type _} [CommRing R] (I : Ideal R) : Prop := #check Ideal.IsLocallyNilpotent end Ideal - -- Repeats the definition of the length of a module by Monalisa variable (R : Type _) [CommRing R] (I J : Ideal R) variable (M : Type _) [AddCommMonoid M] [Module R M] @@ -71,7 +70,7 @@ lemma ring_Noetherian_iff_spec_Noetherian : IsNoetherianRing R sorry -- how do I apply an instance to prove one direction? - +-- Stacks Lemma 5.9.2: -- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible : -- Every closed subset of a noetherian space is a finite union -- of irreducible closed subsets. @@ -169,7 +168,7 @@ abbrev Prod_of_localization := def foo : Prod_of_localization R →+* R where toFun := sorry - invFun := sorry + -- invFun := sorry left_inv := sorry right_inv := sorry map_mul' := sorry @@ -198,6 +197,13 @@ lemma primes_of_Artinian_are_maximal lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : IsNoetherianRing R ∧ Ideal.krullDim R ≤ 0 ↔ IsArtinianRing R := by constructor + rintro ⟨RisNoetherian, dimzero⟩ + rw [ring_Noetherian_iff_spec_Noetherian] at RisNoetherian + let Z := irreducibleComponents (PrimeSpectrum R) + have Zfinite : Set.Finite Z := by + -- apply TopologicalSpace.NoetherianSpace.finite_irreducibleComponents ?_ + sorry + sorry intro RisArtinian constructor @@ -207,81 +213,7 @@ lemma dim_le_zero_Noetherian_iff_Artinian (R : Type _) [CommRing R] : intro I apply primes_of_Artinian_are_maximal - - - --- Trash bin --- lemma Artinian_has_finite_max_ideal --- [IsArtinianRing R] : Finite (MaximalSpectrum R) := by --- by_contra infinite --- simp only [not_finite_iff_infinite] at infinite --- let m' : ℕ ↪ MaximalSpectrum R := Infinite.natEmbedding (MaximalSpectrum R) --- have m'inj := m'.injective --- let m'' : ℕ → Ideal R := fun n : ℕ ↦ ⨅ k ∈ range n, (m' k).asIdeal --- let f : ℕ → Ideal R := fun n : ℕ ↦ (m' n).asIdeal --- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by --- apply IsArtinian.monotone_stabilizes { --- toFun := m'' --- monotone' := sorry --- } --- cases' DCC with n DCCn --- specialize DCCn (n+1) --- specialize DCCn (Nat.le_succ n) --- let F : Fin (n + 1) → MaximalSpectrum R := fun k ↦ m' k --- have comaximal : ∀ (i j : Fin (n + 1)), (i ≠ j) → (F i).asIdeal ⊔ (F j).asIdeal = --- (⊤ : Ideal R) := by --- intro i j distinct --- apply Ideal.IsMaximal.coprime_of_ne --- exact (F i).IsMaximal --- exact (F j).IsMaximal --- have : (F i) ≠ (F j) := by --- apply Function.Injective.ne m'inj --- contrapose! distinct --- exact Fin.ext distinct --- intro h --- apply this --- exact MaximalSpectrum.ext _ _ h --- let CRT1 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal)) --- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) := --- Ideal.quotientInfRingEquivPiQuotient --- (fun i ↦ (F i).asIdeal) comaximal --- let CRT2 : (R ⧸ ⨅ (i : Fin (n + 1)), ((F i).asIdeal)) --- ≃+* ((i : Fin (n + 1)) → R ⧸ (F i).asIdeal) := --- Ideal.quotientInfRingEquivPiQuotient --- (fun i ↦ (F i).asIdeal) comaximal - - - - - -- have comaximal : ∀ (n : ℕ) (i j : Fin n), (i ≠ j) → ((F n) i).asIdeal ⊔ ((F n) j).asIdeal = - -- (⊤ : Ideal R) := by - -- intro n i j distinct - -- apply Ideal.IsMaximal.coprime_of_ne - -- exact (F n i).IsMaximal - -- exact (F n j).IsMaximal - -- have : (F n i) ≠ (F n j) := by - -- apply Function.Injective.ne m'inj - -- contrapose! distinct - -- exact Fin.ext distinct - -- intro h - -- apply this - -- exact MaximalSpectrum.ext _ _ h - -- let CRT : (n : ℕ) → (R ⧸ ⨅ (i : Fin n), ((F n) i).asIdeal) - -- ≃+* ((i : Fin n) → R ⧸ ((F n) i).asIdeal) := - -- fun n ↦ Ideal.quotientInfRingEquivPiQuotient - -- (fun i ↦ (F n i).asIdeal) (comaximal n) - -- have DCC : ∃ n : ℕ, ∀ k : ℕ, n ≤ k → m'' n = m'' k := by - -- apply IsArtinian.monotone_stabilizes { - -- toFun := m'' - -- monotone' := sorry - -- } - -- cases' DCC with n DCCn - -- specialize DCCn (n+1) - -- specialize DCCn (Nat.le_succ n) - -- let CRT1 := CRT n - -- let CRT2 := CRT (n + 1) - - +-- Use TopologicalSpace.NoetherianSpace.exists_finset_irreducible :