mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2024-12-26 23:48:36 -06:00
61 lines
No EOL
2.6 KiB
Text
61 lines
No EOL
2.6 KiB
Text
import Mathlib.RingTheory.Ideal.Operations
|
||
import Mathlib.RingTheory.FiniteType
|
||
import Mathlib.Order.Height
|
||
import Mathlib.RingTheory.PrincipalIdealDomain
|
||
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.
|
||
There are also sorried statements of many of the theorems that would be
|
||
really nice to prove.
|
||
I'm imagining for this file to ultimately contain basic API for height and
|
||
krull dimension, and the theorems will probably end up other files,
|
||
depending on how long the proofs are, and what extra API needs to be
|
||
developed.
|
||
-/
|
||
|
||
namespace Ideal
|
||
|
||
variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
|
||
|
||
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < 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 := iSup_le_iff (α := WithBot ℕ∞)
|
||
|
||
--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
|
||
|
||
#check Ring.DimensionLEOne
|
||
lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
|
||
|
||
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] :
|
||
krullDim R ≤ krullDim (Polynomial R) + 1 := sorry
|
||
|
||
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
|
||
krullDim R = krullDim (Polynomial R) + 1 := sorry
|
||
|
||
lemma height_eq_dim_localization :
|
||
height I = krullDim (Localization.AtPrime I.asIdeal) := sorry
|
||
|
||
lemma height_add_dim_quotient_le_dim : height I + krullDim (R ⧸ I.asIdeal) ≤ krullDim R := sorry |