diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index e35a4c5..e24aa0f 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -19,6 +19,7 @@ import Mathlib.Order.ConditionallyCompleteLattice.Basic developed. -/ +/-- If something is smaller that Bot of a PartialOrder after attaching another Bot, it must be Bot. -/ lemma lt_bot_eq_WithBot_bot [PartialOrder α] [OrderBot α] {a : WithBot α} (h : a < (⊥ : α)) : a = ⊥ := by cases a . rfl @@ -29,18 +30,19 @@ open LocalRing variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) +/-- Definitions -/ noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I} - 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 +/-- A lattice structure on WithBot ℕ∞. -/ noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice +/-- Height of ideals is monotonic. -/ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := by apply Set.chainHeight_mono intro J' hJ' @@ -57,6 +59,34 @@ lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) : lemma height_le_krullDim (I : PrimeSpectrum R) : height I ≤ krullDim R := le_iSup (λ I : PrimeSpectrum R => (height I : WithBot ℕ∞)) I +/-- In a domain, the height of a prime ideal is Bot (0 in this case) iff it's the Bot ideal. -/ +@[simp] +lemma height_bot_iff_bot {D: Type} [CommRing D] [IsDomain D] {P : PrimeSpectrum D} : height P = ⊥ ↔ P = ⊥ := by + constructor + · intro h + unfold height at h + rw [bot_eq_zero] at h + simp only [Set.chainHeight_eq_zero_iff] at h + apply eq_bot_of_minimal + intro I + by_contra x + have : I ∈ {J | J < P} := x + rw [h] at this + contradiction + · intro h + unfold height + simp only [bot_eq_zero', Set.chainHeight_eq_zero_iff] + by_contra spec + change _ ≠ _ at spec + rw [← Set.nonempty_iff_ne_empty] at spec + obtain ⟨J, JlP : J < P⟩ := spec + have JneP : J ≠ P := ne_of_lt JlP + rw [h, ←bot_lt_iff_ne_bot, ←h] at JneP + have := not_lt_of_lt JneP + contradiction + +/-- The Krull dimension of a ring being ≥ n is equivalent to there being an + ideal of height ≥ n. -/ lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) : n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by constructor @@ -230,9 +260,9 @@ lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal . exact List.chain'_singleton _ . constructor . intro I' hI' - simp at hI' + simp only [List.mem_singleton] at hI' rwa [hI'] - . simp + . simp only [List.length_singleton, Nat.cast_one, zero_add] . contrapose! h change (0 : ℕ∞) < (_ : WithBot ℕ∞) at h rw [lt_height_iff''] at h @@ -259,7 +289,7 @@ lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum /-- In a field, the unique prime ideal is the zero ideal. -/ @[simp] -lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by +lemma field_prime_bot {K: Type _} [Field K] {P : Ideal K} : IsPrime P ↔ P = ⊥ := by constructor · intro primeP obtain T := eq_bot_or_top P @@ -270,9 +300,16 @@ lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = exact bot_prime /-- In a field, all primes have height 0. -/ -lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : height P = 0 := by +lemma field_prime_height_bot {K: Type _} [Nontrivial K] [Field K] {P : PrimeSpectrum K} : height P = ⊥ := by + -- This should be doable by + -- have : IsPrime P.asIdeal := P.IsPrime + -- rw [field_prime_bot] at this + -- have : P = ⊥ := PrimeSpectrum.ext P ⊥ this + -- rw [height_bot_iff_bot] + -- Need to check what's happening + rw [bot_eq_zero] unfold height - simp + simp only [Set.chainHeight_eq_zero_iff] by_contra spec change _ ≠ _ at spec rw [← Set.nonempty_iff_ne_empty] at spec @@ -288,7 +325,7 @@ lemma field_prime_height_zero {K: Type _} [Field K] (P : PrimeSpectrum K) : heig /-- The Krull dimension of a field is 0. -/ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim - simp [field_prime_height_zero] + simp only [field_prime_height_bot, ciSup_unique] /-- A domain with Krull dimension 0 is a field. -/ lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by @@ -335,7 +372,7 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by rcases (lt_height_iff''.mp h) with ⟨c, ⟨hc1, hc2, hc3⟩⟩ norm_cast at hc3 rw [List.chain'_iff_get] at hc1 - specialize hc1 0 (by rw [hc3]; simp) + specialize hc1 0 (by rw [hc3]; simp only) set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ } set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ } specialize hc2 q1 (List.get_mem _ _ _) diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 987fe93..367e30f 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -1,39 +1,71 @@ import CommAlg.krull 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.Ideal.MinimalPrime -import Mathlib.RingTheory.Localization.AtPrime import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic -import Mathlib.Order.ConditionallyCompleteLattice.Basic namespace Ideal +/-- The ring of polynomials over a field has dimension one. -/ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullDim (Polynomial K) = 1 := by - -- unfold krullDim rw [le_antisymm_iff] + let X := @Polynomial.X K _ constructor - · - sorry + · unfold krullDim + apply @iSup_le (WithBot ℕ∞) _ _ _ _ + intro I + have PIR : IsPrincipalIdealRing (Polynomial K) := by infer_instance + by_cases I = ⊥ + · rw [← height_bot_iff_bot] at h + simp only [WithBot.coe_le_one, ge_iff_le] + rw [h] + exact bot_le + · push_neg at h + have : I.asIdeal ≠ ⊥ := by + by_contra a + have : I = ⊥ := PrimeSpectrum.ext I ⊥ a + contradiction + have maxI := IsPrime.to_maximal_ideal this + have singleton : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by + intro P + constructor + · intro H + simp only [Set.mem_setOf_eq] at H + by_contra x + push_neg at x + have : P.asIdeal ≠ ⊥ := by + by_contra a + have : P = ⊥ := PrimeSpectrum.ext P ⊥ a + contradiction + have maxP := IsPrime.to_maximal_ideal this + have IneTop := IsMaximal.ne_top maxI + have : P ≤ I := le_of_lt H + rw [←PrimeSpectrum.asIdeal_le_asIdeal] at this + have : P.asIdeal = I.asIdeal := Ideal.IsMaximal.eq_of_le maxP IneTop this + have : P = I := PrimeSpectrum.ext P I this + replace H : P ≠ I := ne_of_lt H + contradiction + · intro pBot + simp only [Set.mem_setOf_eq, pBot] + exact lt_of_le_of_ne bot_le h.symm + replace singleton : {J | J < I} = {⊥} := Set.ext singleton + unfold height + sorry · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) · obtain ⟨I, h⟩ := this have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by apply @le_iSup (WithBot ℕ∞) _ _ _ I exact le_trans h this have primeX : Prime Polynomial.X := @Polynomial.prime_X K _ _ - let X := @Polynomial.X K _ have : IsPrime (span {X}) := by - refine Iff.mpr (span_singleton_prime ?hp) primeX + refine (span_singleton_prime ?hp).mpr primeX exact Polynomial.X_ne_zero let P := PrimeSpectrum.mk (span {X}) this unfold height use P have : ⊥ ∈ {J | J < P} := by - simp only [Set.mem_setOf_eq] - rw [bot_lt_iff_ne_bot] + simp only [Set.mem_setOf_eq, bot_lt_iff_ne_bot] suffices : P.asIdeal ≠ ⊥ · by_contra x rw [PrimeSpectrum.ext_iff] at x