SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Added some comments

Browse source
This commit is contained in:
Sayantan Santra 2023-06-15 20:06:08 -07:00
parent 1cf31c2590
commit 54c76464bc
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 6 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
CommAlg/krull.lean
View file

@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic
developed. developed.
-/ -/
/-- If something is smaller that Bot of a PartialOrder after attaching another Bot, it must be Bot. -/
lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by
cases a cases a
. rfl . rfl
@ -29,18 +30,19 @@ open LocalRing
variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
/-- Definitions -/
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
noncomputable def codimension (J : Ideal R) : WithBot ℕ∞ := ⨅ I ∈ {I : PrimeSpectrum R | J ≤ I.asIdeal}, height I noncomputable def codimension (J : Ideal R) : WithBot ℕ∞ := ⨅ I ∈ {I : PrimeSpectrum R | J ≤ I.asIdeal}, height I
lemma height_def : height I = Set.chainHeight {J : PrimeSpectrum R | J < I} := rfl 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 = (⨆ (I : PrimeSpectrum R), height I : WithBot ℕ∞) := rfl
lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl lemma krullDim_def' (R : Type _) [CommRing R] : krullDim R = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
/-- A lattice structure on WithBot ℕ∞. -/
noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
/-- Height of ideals is monotonic. -/
lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by
apply Set.chainHeight_mono apply Set.chainHeight_mono
intro J' hJ' intro J' hJ'
@ -57,6 +59,8 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R :=
le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I
/-- The Krull dimension of a ring being ≥ n is equivalent to there being an
ideal of height ≥ n. -/
lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by
constructor constructor