From 2d5a7d3deb013b9a9b1325ef6f3e505b72776bc8 Mon Sep 17 00:00:00 2001 From: GTBarkley Date: Thu, 15 Jun 2023 20:35:28 +0000 Subject: [PATCH] defined codimension of an ideal --- CommAlg/krull.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index a559b1d..e068760 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -28,6 +28,8 @@ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < noncomputable def krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I +noncomputable def codimension (J : Ideal R) : WithBot ℕ∞ := ⨅ I ∈ {I : PrimeSpectrum R | J ≤ I.asIdeal}, 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