Merge pull request #72 from GTBarkley/grant

added docstrings

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
@@ -176,9 +186,10 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum
   rw [←WithBot.coe_le_coe,←hn] at this
   change (0 : WithBot ℕ∞) ≤ _ at this
   constructor <;> intro h'
-  rw [h']
-  exact le_antisymm h' this
+  . 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
@@ -259,10 +274,9 @@ lemma dim_le_one_of_dimLEOne :  Ring.DimensionLEOne R → krullDim R ≤ 1 := by
   change q0.asIdeal < q1.asIdeal at hc1
   have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
   specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
-  apply IsPrime.ne_top p.IsPrime
-  apply (IsCoatom.lt_iff H.out).mp
-  exact hc2
+  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