From 50515d9ed8e2aa115ef83b43df1e0f9c3bec3cb3 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:02:02 -0700 Subject: [PATCH 1/3] Completed most of the simple part --- .../sayantan(dim_eq_dim_polynomial_add_one).lean | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index ea6f7cd..485ee3b 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -22,11 +22,7 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c lemma dim_le_dim_polynomial_add_one [Nontrivial R] : krullDim R + 1 ≤ krullDim (Polynomial R) := sorry -- Others are working on it --- private lemma sum_succ_of_succ_sum {ι : Type} (a : ℕ∞) [inst : Nonempty ι] : --- (⨆ (x : ι), a + 1) = (⨆ (x : ι), a) + 1 := by --- have : a + 1 = (⨆ (x : ι), a) + 1 := by rw [ciSup_const] --- have : a + 1 = (⨆ (x : ι), a + 1) := Eq.symm ciSup_const --- simp +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 dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : krullDim R + 1 = krullDim (Polynomial R) := by @@ -37,6 +33,15 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : 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 + apply exists_le_maximal + apply IsPrime.ne_top + apply P.IsPrime + obtain ⟨M, maxM, PleM⟩ := this + let P' : PrimeSpectrum (Polynomial R) := PrimeSpectrum.mk M (IsMaximal.isPrime maxM) + have PleP' : P ≤ P' := PleM + have : height P ≤ height P' := height_le_of_le PleP' + simp only [WithBot.coe_le_coe] sorry obtain ⟨I, IP⟩ := this have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by From a2f481c7db196d982765165911022adaf6ea03e8 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:12:33 -0700 Subject: [PATCH 2/3] Turn some simp into simp only --- CommAlg/krull.lean | 2 +- CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean | 11 ++++++++--- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 06e6d0d..1e720c0 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -63,7 +63,7 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) := apply height_le_of_le apply le_maximalIdeal exact I.2.1 - . simp + . simp only [height_le_krullDim] #check height_le_krullDim --some propositions that would be nice to be able to eventually diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean index 485ee3b..089c4b5 100644 --- a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -42,16 +42,21 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] : have PleP' : P ≤ P' := PleM have : height P ≤ height P' := height_le_of_le PleP' simp only [WithBot.coe_le_coe] - sorry + have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by + + sorry + obtain ⟨I, h⟩ := this + use I + exact ge_trans h this obtain ⟨I, IP⟩ := this have : (↑(height I + 1) : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum R), ↑(height I + 1) := by apply @le_iSup (WithBot ℕ∞) _ _ _ I - apply ge_trans this IP + exact ge_trans this IP 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 apply this - simp + simp only [iSup_le_iff] intro P exact ge_trans oneOut (htPBdd P) From ae8bf07ee7b82901b157fb81d018120f8f52c804 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:23:29 -0700 Subject: [PATCH 3/3] Make the lemma names a little more descriptive --- CommAlg/krull.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1e720c0..ec94d36 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] -lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by +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 obtain ⟨P, ⟨h1, primeP⟩⟩ := x @@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) aesop contradiction -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by +lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor - · exact isField.dim_zero + · exact domain_dim_zero.isField · intro fieldD let h : Field D := IsField.toField fieldD exact dim_field_eq_zero