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

Merge pull request #24 from GTBarkley/grant

Browse source 
stated some equivalences for bounding krull dim
This commit is contained in:
GTBarkley 2023-06-12 11:03:07 -07:00 committed by GitHub
commit 5854c496fe
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
CommAlg/grant.lean
View file

@ -2,6 +2,7 @@ import Mathlib.Order.KrullDimension
import Mathlib.Order.JordanHolder import Mathlib.Order.JordanHolder
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.Height import Mathlib.Order.Height
import CommAlg.krull
#check (p q : PrimeSpectrum _) → (p ≤ q) #check (p q : PrimeSpectrum _) → (p ≤ q)
@ -39,22 +40,14 @@ lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop
-- norm_cast -- norm_cast
sorry sorry
namespace Ideal
noncomputable def krullDim (R : Type _) [CommRing R] :=
Set.chainHeight (Set.univ : Set (PrimeSpectrum R))
def krullDimGE (R : Type _) [CommRing R] (n : ℕ) :=
∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1
def krullDimLE (R : Type _) [CommRing R] (n : ℕ) :=
∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1
end Ideal
open Ideal open Ideal
lemma krullDim_le (R : Type _) [CommRing R] : krullDimLE R n ↔ Ideal.krullDim R ≤ n := sorry lemma krullDim_le_iff' (R : Type _) [CommRing R] :
lemma krullDim_ge (R : Type _) [CommRing R] : krullDimGE R n ↔ Ideal.krullDim R ≥ n := sorry Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
sorry
lemma krullDim_ge_iff' (R : Type _) [CommRing R] :
Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
-- #check ((4 : ℕ∞) : WithBot (WithTop ℕ)) -- #check ((4 : ℕ∞) : WithBot (WithTop ℕ))