From 54c76464bc171509ebf117949389ba538d2237fe Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 20:06:08 -0700 Subject: [PATCH 1/3] Added some comments --- CommAlg/krull.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 642c2c7..05727a0 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic developed. -/ +/-- If something is smaller that Bot of a PartialOrder after attaching another Bot, it must be Bot. -/ lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by cases a . rfl @@ -29,18 +30,19 @@ open LocalRing variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) +/-- Definitions -/ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} - 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 +/-- A lattice structure on WithBot ℕ∞. -/ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice +/-- Height of ideals is monotonic. -/ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by apply Set.chainHeight_mono intro J' hJ' @@ -57,6 +59,8 @@ lemma krullDim_le_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 ring being ≥ n is equivalent to there being an + ideal of height ≥ n. -/ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by constructor From d4a2a416f5036b291b8e3fcabe609747a95708c8 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Thu, 15 Jun 2023 22:45:43 -0700 Subject: [PATCH 2/3] Some cleanup and added height_bot_iff_bot --- CommAlg/krull.lean | 40 ++++++++++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 05727a0..bf3e998 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -59,6 +59,31 @@ lemma krullDim_le_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 +/-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/ +lemma height_bot_iff_bot {D: Type} [CommRing D] [IsDomain D] (P : PrimeSpectrum D) : height P = ⊥ ↔ P = ⊥ := by + constructor + · intro h + unfold height at h + rw [bot_eq_zero] at h + simp only [Set.chainHeight_eq_zero_iff] at h + apply eq_bot_of_minimal + intro I + by_contra x + have : I ∈ {J | J < P} := x + rw [h] at this + contradiction + · intro h + unfold height + simp only [bot_eq_zero', Set.chainHeight_eq_zero_iff] + by_contra spec + change _ ≠ _ at spec + rw [← Set.nonempty_iff_ne_empty] at spec + obtain ⟨J, JlP : J < P⟩ := spec + have JneP : J ≠ P := ne_of_lt JlP + rw [h, ←bot_lt_iff_ne_bot, ←h] at JneP + have := not_lt_of_lt JneP + contradiction + /-- The Krull dimension of a ring being ≥ n is equivalent to there being an ideal of height ≥ n. -/ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : @@ -209,9 +234,9 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal . exact List.chain'_singleton _ . constructor . intro I' hI' - simp at hI' + simp only [List.mem_singleton] at hI' rwa [hI'] - . simp + . simp only [List.length_singleton, Nat.cast_one, zero_add] . contrapose! h change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h rw [lt_height_iff''] at h @@ -249,9 +274,12 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = 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 +lemma field_prime_height_bot {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = ⊥ := by + -- This should be doable by using field_prime_height_bot + -- and height_bot_iff_bot + rw [bot_eq_zero] unfold height - simp + simp only [Set.chainHeight_eq_zero_iff] by_contra spec change _ ≠ _ at spec rw [← Set.nonempty_iff_ne_empty] at spec @@ -267,7 +295,7 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig /-- 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] + simp only [field_prime_height_bot, ciSup_unique] /-- 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 @@ -314,7 +342,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩ norm_cast at hc3 rw [List.chain'_iff_get] at hc1 - specialize hc1 0 (by rw [hc3]; simp) + specialize hc1 0 (by rw [hc3]; simp only) set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ } set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } specialize hc2 q1 (List.get_mem _ _ _) From d2836ad8f85135d32282e86111734e543146c70c Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 00:22:40 -0700 Subject: [PATCH 3/3] Almost completed polynomial_over_field_dim_one --- CommAlg/krull.lean | 15 ++++--- CommAlg/sayantan(poly_over_field).lean | 56 ++++++++++++++++++++------ 2 files changed, 54 insertions(+), 17 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index bf3e998..b346d4d 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -60,7 +60,8 @@ lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I /-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/ -lemma height_bot_iff_bot {D: Type} [CommRing D] [IsDomain D] (P : PrimeSpectrum D) : height P = ⊥ ↔ P = ⊥ := by +@[simp] +lemma height_bot_iff_bot {D: Type} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = ⊥ ↔ P = ⊥ := by constructor · intro h unfold height at h @@ -263,7 +264,7 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum /-- 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 +lemma field_prime_bot {K: Type _} [Field K] {P : Ideal K} : IsPrime P ↔ P = ⊥ := by constructor · intro primeP obtain T := eq_bot_or_top P @@ -274,9 +275,13 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = exact bot_prime /-- In a field, all primes have height 0. -/ -lemma field_prime_height_bot {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = ⊥ := by - -- This should be doable by using field_prime_height_bot - -- and height_bot_iff_bot +lemma field_prime_height_bot {K: Type _} [Nontrivial K] [Field K] {P : PrimeSpectrum K} : height P = ⊥ := by + -- This should be doable by + -- have : IsPrime P.asIdeal := P.IsPrime + -- rw [field_prime_bot] at this + -- have : P = ⊥ := PrimeSpectrum.ext P ⊥ this + -- rw [height_bot_iff_bot] + -- Need to check what's happening rw [bot_eq_zero] unfold height simp only [Set.chainHeight_eq_zero_iff] diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 987fe93..367e30f 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -1,39 +1,71 @@ 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 +/-- The ring of polynomials over a field has dimension one. -/ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by - -- unfold krullDim rw [le_antisymm_iff] + let X := @Polynomial.X K _ constructor - · - sorry + · unfold krullDim + apply @iSup_le (WithBot ℕ∞) _ _ _ _ + intro I + have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance + by_cases I = ⊥ + · rw [← height_bot_iff_bot] at h + simp only [WithBot.coe_le_one, ge_iff_le] + rw [h] + exact bot_le + · push_neg at h + have : I.asIdeal ≠ ⊥ := by + by_contra a + have : I = ⊥ := PrimeSpectrum.ext I ⊥ a + contradiction + have maxI := IsPrime.to_maximal_ideal this + have singleton : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by + intro P + constructor + · intro H + simp only [Set.mem_setOf_eq] at H + by_contra x + push_neg at x + have : P.asIdeal ≠ ⊥ := by + by_contra a + have : P = ⊥ := PrimeSpectrum.ext P ⊥ a + contradiction + have maxP := IsPrime.to_maximal_ideal this + have IneTop := IsMaximal.ne_top maxI + have : P ≤ I := le_of_lt H + rw [←PrimeSpectrum.asIdeal_le_asIdeal] at this + have : P.asIdeal = I.asIdeal := Ideal.IsMaximal.eq_of_le maxP IneTop this + have : P = I := PrimeSpectrum.ext P I this + replace H : P ≠ I := ne_of_lt H + contradiction + · intro pBot + simp only [Set.mem_setOf_eq, pBot] + exact lt_of_le_of_ne bot_le h.symm + replace singleton : {J | J < I} = {⊥} := Set.ext singleton + unfold height + 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 + refine (span_singleton_prime ?hp).mpr 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] + simp only [Set.mem_setOf_eq, bot_lt_iff_ne_bot] suffices : P.asIdeal ≠ ⊥ · by_contra x rw [PrimeSpectrum.ext_iff] at x