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

Merge pull request #68 from SinTan1729/main

Browse source 
Trying to break it down to smaller parts
This commit is contained in:
Sayantan Santra 2023-06-14 19:02:19 -05:00 committed by GitHub
commit e103d3d1ac
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
CommAlg/sayantan(dim_eq_dim_polynomial_add_one).lean
View file

@ -3,9 +3,11 @@ 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
import Mathlib.Data.Set.Ncard
namespace Ideal
@ -24,6 +26,13 @@ lemma dim_le_dim_polynomial_add_one [Nontrivial R] :
lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤ height J := sorry -- Already done in main file
lemma primeIdeal_finite_height_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) : height P ≠ ⊤ := by
sorry
lemma exist_elts_MinimalOver_of_primeIdeal_of_noetherianRing [Nontrivial R] [IsNoetherianRing R] (P: PrimeSpectrum R) :
∃S : Set R, Set.ncard s = height P ∧ P.asIdeal ∈ Ideal.minimalPrimes (Ideal.span S) := by
sorry
lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
krullDim R + 1 = krullDim (Polynomial R) := by
rw [le_antisymm_iff]
@ -43,6 +52,7 @@ lemma dim_eq_dim_polynomial_add_one [Nontrivial R] [IsNoetherianRing R] :
have : height P ≤ height P' := height_le_of_le PleP'
simp only [WithBot.coe_le_coe]
have : ∃ (I : PrimeSpectrum R), height P' ≤ height I + 1 := by
-- Prime avoidance is called subset_union_prime
sorry
obtain ⟨I, h⟩ := this