From 5f241e80f164fb255953686d33c21d4a12cd1df1 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:16:53 -0700 Subject: [PATCH 1/3] Added a comment --- CommAlg/krull.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index c021d74..e8941a3 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -88,7 +88,7 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial -lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry +lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file #check Ring.DimensionLEOne lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry From 3730100c86de0fed1adf2df212d98d84af084ef7 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:10 -0700 Subject: [PATCH 2/3] Moved dim_eq_zero_iff_field to the main file --- CommAlg/krull.lean | 60 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e8941a3..4e069a2 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -88,7 +88,65 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by . rw [h.forall_iff] trivial -lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file +@[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] + +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 #check Ring.DimensionLEOne lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry From 7b8c0ba127128bfb3bd11221291139e087978e03 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:35:46 -0700 Subject: [PATCH 3/3] Made very small changes --- CommAlg/sayantan(dim_eq_zero_iff_field).lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CommAlg/sayantan(dim_eq_zero_iff_field).lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean index 35f197f..fd712f0 100644 --- a/CommAlg/sayantan(dim_eq_zero_iff_field).lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -68,7 +68,7 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) 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 zero_height : (Set.chainHeight {J | J < P'}) ≤ 0 := by + 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')