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

moved krullDim_nonneg_of_nontrivial to krull.lean

Browse source
This commit is contained in:
leopoldmayer 2023-06-13 20:58:32 -07:00
parent a941cce12f
commit 50aa1b07a8
1 changed files with 13 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
CommAlg/krull.lean
View file

@ -94,6 +94,17 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
. rw [h.forall_iff]
trivial
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
lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
constructor <;> intro h
. intro I
sorry
. sorry
lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
#check Ring.DimensionLEOne
@ -104,10 +115,10 @@ lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1
exact Ring.DimensionLEOne.principal_ideal_ring R
lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
krullDim R + 1 ≤ krullDim (Polynomial R) := sorry
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krullDim R = krullDim (Polynomial R) + 1 := sorry
krullDim R + 1 = krullDim (Polynomial R) := sorry
lemma height_eq_dim_localization :
height I = krullDim (Localization.AtPrime I.asIdeal) := sorry