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

updated krull_dim name, addd krullDim_le_iff

Browse source
This commit is contained in:
leopoldmayer 2023-06-12 09:49:40 -07:00
parent a157174c65
commit 6d4b9b0f60
1 changed files with 20 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
comm_alg/krull.lean
View file

@ -5,6 +5,7 @@ import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic
/- This file contains the definitions of height of an ideal, and the krull
dimension of a commutative ring.
@ -22,26 +23,37 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
noncomputable def krullDim (R : Type) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I
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 = iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) := rfl
noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
lemma krullDim_le_iff (R : Type) [CommRing R] (n : ℕ) :
iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) ≤ n ↔
∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := by
convert @iSup_le_iff (WithBot ℕ∞) (PrimeSpectrum R) inferInstance _ (↑n)
--some propositions that would be nice to be able to eventually
lemma dim_eq_zero_iff_field : krull_dim R = 0 ↔ IsField R := by sorry
lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry
#check Ring.DimensionLEOne
lemma dim_le_one_iff : krull_dim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krull_dim R ≤ 1 := by
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
lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
krull_dim R ≤ krull_dim (Polynomial R) + 1 := sorry
krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krull_dim R = krull_dim (Polynomial R) + 1 := sorry
krullDim R = krullDim (Polynomial R) + 1 := sorry
lemma height_eq_dim_localization :
height I = krull_dim (Localization.AtPrime I.asIdeal) := sorry
height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
lemma height_add_dim_quotient_le_dim : height I + krull_dim (R ⧸ I.asIdeal) ≤ krull_dim R := sorry
lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry