From 06a491b8437fa18bddee734ecbaaad74ad1636dd Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 19:58:28 -0700 Subject: [PATCH 1/2] del: Deleted temp working file --- CommAlg/sayantan(dim_eq_zero_iff_field).lean | 82 -------------------- 1 file changed, 82 deletions(-) delete mode 100644 CommAlg/sayantan(dim_eq_zero_iff_field).lean diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean deleted file mode 100644 index fd712f0..0000000 --- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean +++ /dev/null @@ -1,82 +0,0 @@ -import Mathlib.RingTheory.Ideal.Basic -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 - -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 - -@[simp] -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 - have : ¬P = ⊤ := IsPrime.ne_top primeP - tauto - · intro botP - rw [botP] - exact bot_prime - -lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by - unfold height - simp - by_contra spec - change _ ≠ _ at spec - rw [← Set.nonempty_iff_ne_empty] at spec - obtain ⟨J, JlP : J < P⟩ := spec - have P0 : IsPrime P.asIdeal := P.IsPrime - have J0 : IsPrime J.asIdeal := J.IsPrime - rw [field_prime_bot] at P0 J0 - have : J.asIdeal = P.asIdeal := Eq.trans J0 (Eq.symm P0) - have : J = P := PrimeSpectrum.ext J P this - have : J ≠ P := ne_of_lt JlP - contradiction - -lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by - unfold krullDim - simp [field_prime_height_zero] - -noncomputable -instance : CompleteLattice (WithBot ℕ∞) := - inferInstanceAs <| CompleteLattice (WithBot (WithTop ℕ)) - -lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by - unfold krullDim at h - simp [height] at h - by_contra x - rw [Ring.not_isField_iff_exists_prime] at x - obtain ⟨P, ⟨h1, primeP⟩⟩ := x - let P' : PrimeSpectrum D := PrimeSpectrum.mk P primeP - have h2 : P' ≠ ⊥ := by - by_contra a - have : P = ⊥ := by rwa [PrimeSpectrum.ext_iff] at a - contradiction - have PgtBot : P' > ⊥ := Ne.bot_lt h2 - have pos_height : ¬ ↑(Set.chainHeight {J | J < P'}) ≤ 0 := by - have : ⊥ ∈ {J | J < P'} := PgtBot - have : {J | J < P'}.Nonempty := Set.nonempty_of_mem this - rw [←Set.one_le_chainHeight_iff] at this - exact not_le_of_gt (Iff.mp ENat.one_le_iff_pos this) - have nonpos_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by - have : (⨆ (I : PrimeSpectrum D), (Set.chainHeight {J | J < I} : WithBot ℕ∞)) ≤ 0 := h.le - rw [iSup_le_iff] at this - exact Iff.mp WithBot.coe_le_zero (this P') - contradiction - -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by - constructor - · exact isField.dim_zero - · intro fieldD - let h : Field D := IsField.toField fieldD - exact dim_field_eq_zero From 56cefd9b53ab50541dbd3c088febe0ffd6894d6d Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 22:54:57 -0700 Subject: [PATCH 2/2] Made some progress on dim_eq_dim_polynomial_add_one --- ...yantan(dim_eq_dim_polynomial_add_one).lean | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean diff --git a/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean new file mode 100644 index 0000000..a9269a2 --- /dev/null +++ b/CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean @@ -0,0 +1,46 @@ +import Mathlib.RingTheory.Ideal.Basic +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 + +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 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 + +-- 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 dim_eq_dim_polynomial_add_one [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 + intro P + unfold height + sorry + have : (⨆ (I : PrimeSpectrum R), ↑(height I) + 1) ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := by + have : ∀ P : PrimeSpectrum R, ↑(height P) + 1 ≤ (⨆ (I : PrimeSpectrum R), ↑(height I)) + 1 := + fun _ ↦ add_le_add_right (le_iSup height _) 1 + apply iSup_le + exact this + sorry \ No newline at end of file