From 89d7be5bc9a03189dd345fd63db0a8d4f7bac552 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Thu, 15 Jun 2023 00:40:57 +0000 Subject: [PATCH] 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