From e735a5254f16e44464b501e5b9979c1325b8c322 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Fri, 16 Jun 2023 10:42:02 -0700 Subject: [PATCH] Completed polynomial_over_field_dim_one --- CommAlg/sayantan(poly_over_field).lean | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/CommAlg/sayantan(poly_over_field).lean b/CommAlg/sayantan(poly_over_field).lean index 367e30f..fc5f967 100644 --- a/CommAlg/sayantan(poly_over_field).lean +++ b/CommAlg/sayantan(poly_over_field).lean @@ -7,6 +7,20 @@ import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic namespace Ideal +private lemma singleton_chainHeight_one {α : Type} [Preorder α] [Bot α] : Set.chainHeight {(⊥ : α)} ≤ 1 := by + unfold Set.chainHeight + simp only [iSup_le_iff, Nat.cast_le_one] + intro L h + unfold Set.subchain at h + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at h + rcases L with (_ | ⟨a,L⟩) + . simp only [List.length_nil, zero_le] + rcases L with (_ | ⟨b,L⟩) + . simp only [List.length_singleton, le_refl] + simp only [List.chain'_cons, List.find?, List.mem_cons, forall_eq_or_imp] at h + rcases h with ⟨⟨h1, _⟩, ⟨rfl, rfl, _⟩⟩ + exact absurd h1 (lt_irrefl _) + /-- 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 rw [le_antisymm_iff] @@ -27,7 +41,7 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD have : I = ⊥ := PrimeSpectrum.ext I ⊥ a contradiction have maxI := IsPrime.to_maximal_ideal this - have singleton : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by + have sngletn : ∀P, P ∈ {J | J < I} ↔ P = ⊥ := by intro P constructor · intro H @@ -49,9 +63,11 @@ lemma polynomial_over_field_dim_one {K : Type} [Nontrivial K] [Field K] : krullD · 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 + replace sngletn : {J | J < I} = {⊥} := Set.ext sngletn unfold height - sorry + rw [sngletn] + simp only [WithBot.coe_le_one, ge_iff_le] + exact singleton_chainHeight_one · suffices : ∃I : PrimeSpectrum (Polynomial K), 1 ≤ (height I : WithBot ℕ∞) · obtain ⟨I, h⟩ := this have : (height I : WithBot ℕ∞) ≤ ⨆ (I : PrimeSpectrum (Polynomial K)), ↑(height I) := by