SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 19:43:55 -05:00
Code Issues Projects Releases Packages Wiki Activity

golf, added dim_eq_bot_iff

Browse source
This commit is contained in:
leopoldmayer 2023-06-12 13:03:35 -07:00
parent 7a189c7b1d
commit fd5bd05f01
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
CommAlg/krull.lean
View file

@ -1,4 +1,5 @@
import Mathlib.RingTheory.Ideal.Basic import Mathlib.RingTheory.Ideal.Operations
import Mathlib.RingTheory.FiniteType
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.RingTheory.PrincipalIdealDomain import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.RingTheory.DedekindDomain.Basic import Mathlib.RingTheory.DedekindDomain.Basic
@ -33,11 +34,12 @@ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.c
lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) : lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔ iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔
∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n)
--some propositions that would be nice to be able to eventually --some propositions that would be nice to be able to eventually
lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := sorry
lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
#check Ring.DimensionLEOne #check Ring.DimensionLEOne