Merge branch 'main' of github.com:GTBarkley/comm_alg into main

This commit is contained in:
leopoldmayer 2023-06-14 14:36:24 -07:00
commit 5035e6ba73
4 changed files with 128 additions and 61 deletions

View file

@ -171,6 +171,48 @@ lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 :
apply (IsCoatom.lt_iff H.out).mp apply (IsCoatom.lt_iff H.out).mp
exact hc2 exact hc2
--refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3))) --refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3)))
lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
intro hp
apply IsPrime.ne_top hq
apply (IsCoatom.lt_iff hp.out).mp
exact h
lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
show ((_ : WithBot ℕ∞) ≤ (0 : )) ↔ _
rw [krullDim_le_iff R 0]
constructor <;> intro h I
. contrapose! h
have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
have hstrct : I < 𝔪p := by
apply lt_of_le_of_ne h𝔪.2
intro hcontr
rw [hcontr] at h
exact h h𝔪.1
use 𝔪p
show (_ : WithBot ℕ∞) > (0 : ℕ∞)
rw [_root_.lt_height_iff'']
use [I]
constructor
. exact List.chain'_singleton _
. constructor
. intro I' hI'
simp at hI'
rwa [hI']
. simp
. contrapose! h
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
rw [_root_.lt_height_iff''] at h
obtain ⟨c, _, hc2, hc3⟩ := h
norm_cast at hc3
rw [List.length_eq_one] at hc3
obtain ⟨𝔮, h𝔮⟩ := hc3
use 𝔮
specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
apply not_maximal_of_lt_prime _ I.IsPrime
exact hc2
end Krull end Krull
section iSupWithBot section iSupWithBot

View file

@ -65,6 +65,34 @@ lemma krullDim_eq_height [LocalRing R] : krullDim R = height (closedPoint R) :=
exact I.2.1 exact I.2.1
. simp only [height_le_krullDim] . simp only [height_le_krullDim]
lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
rcases n with _ | n
. constructor <;> intro h <;> exfalso
. exact (not_le.mpr h) le_top
. tauto
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
symm
show (n + 1 ≤ m ↔ _ )
apply ENat.add_one_le_iff
exact ENat.coe_ne_top _
rw [this]
unfold Ideal.height
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ) = (_:ℕ∞))
rw [{J | J < 𝔭}.le_chainHeight_iff]
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
constructor <;> rintro ⟨c, hc⟩ <;> use c
. tauto
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
norm_cast at hc
tauto
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
show (_ < _) ↔ _
rw [WithBot.coe_lt_coe]
exact lt_height_iff'
#check height_le_krullDim #check height_le_krullDim
--some propositions that would be nice to be able to eventually --some propositions that would be nice to be able to eventually
@ -99,11 +127,57 @@ lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [Nontrivial R] :
lift (Ideal.krullDim R) to ℕ∞ using h with k lift (Ideal.krullDim R) to ℕ∞ using h with k
use k use k
lemma not_maximal_of_lt_prime {p : Ideal R} {q : Ideal R} (hq : IsPrime q) (h : p < q) : ¬IsMaximal p := by
intro hp
apply IsPrime.ne_top hq
apply (IsCoatom.lt_iff hp.out).mp
exact h
lemma dim_le_zero_iff : krullDim R ≤ 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
show ((_ : WithBot ℕ∞) ≤ (0 : )) ↔ _
rw [krullDim_le_iff R 0]
constructor <;> intro h I
. contrapose! h
have ⟨𝔪, h𝔪⟩ := I.asIdeal.exists_le_maximal (IsPrime.ne_top I.IsPrime)
let 𝔪p := (⟨𝔪, IsMaximal.isPrime h𝔪.1⟩ : PrimeSpectrum R)
have hstrct : I < 𝔪p := by
apply lt_of_le_of_ne h𝔪.2
intro hcontr
rw [hcontr] at h
exact h h𝔪.1
use 𝔪p
show (_ : WithBot ℕ∞) > (0 : ℕ∞)
rw [lt_height_iff'']
use [I]
constructor
. exact List.chain'_singleton _
. constructor
. intro I' hI'
simp at hI'
rwa [hI']
. simp
. contrapose! h
change (_ : WithBot ℕ∞) > (0 : ℕ∞) at h
rw [lt_height_iff''] at h
obtain ⟨c, _, hc2, hc3⟩ := h
norm_cast at hc3
rw [List.length_eq_one] at hc3
obtain ⟨𝔮, h𝔮⟩ := hc3
use 𝔮
specialize hc2 𝔮 (h𝔮 ▸ (List.mem_singleton.mpr rfl))
apply not_maximal_of_lt_prime I.IsPrime
exact hc2
lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by lemma dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
constructor <;> intro h rw [←dim_le_zero_iff]
. intro I obtain ⟨n, hn⟩ := krullDim_nonneg_of_nontrivial R
sorry have : n ≥ 0 := zero_le n
. sorry change _ ≤ _ at this
rw [←WithBot.coe_le_coe,←hn] at this
change (0 : WithBot ℕ∞) ≤ _ at this
constructor <;> intro h'
rw [h']
exact le_antisymm h' this
@[simp] @[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
@ -167,37 +241,10 @@ lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krull
-- This lemma is false! -- This lemma is false!
lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry
lemma lt_height_iff' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
rcases n with _ | n
. constructor <;> intro h <;> exfalso
. exact (not_le.mpr h) le_top
. tauto
have (m : ℕ∞) : m > some n ↔ m ≥ some (n + 1) := by
symm
show (n + 1 ≤ m ↔ _ )
apply ENat.add_one_le_iff
exact ENat.coe_ne_top _
rw [this]
unfold Ideal.height
show ((↑(n + 1):ℕ∞) ≤ _) ↔ ∃c, _ ∧ _ ∧ ((_ : WithTop ) = (_:ℕ∞))
rw [{J | J < 𝔭}.le_chainHeight_iff]
show (∃ c, (List.Chain' _ c ∧ ∀𝔮, 𝔮 ∈ c → 𝔮 < 𝔭) ∧ _) ↔ _
constructor <;> rintro ⟨c, hc⟩ <;> use c
. tauto
. change _ ∧ _ ∧ (List.length c : ℕ∞) = n + 1 at hc
norm_cast at hc
tauto
lemma lt_height_iff'' {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > (n : WithBot ℕ∞) ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀ 𝔮 ∈ c, 𝔮 < 𝔭) ∧ c.length = n + 1 := by
show (_ < _) ↔ _
rw [WithBot.coe_lt_coe]
exact lt_height_iff'
/-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib /-- The converse of this is false, because the definition of "dimension ≤ 1" in mathlib
applies only to dimension zero rings and domains of dimension 1. -/ applies only to dimension zero rings and domains of dimension 1. -/
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ) := by lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ 1 := by
show _ → ((_ : WithBot ℕ∞) ≤ (1 : ))
rw [krullDim_le_iff R 1] rw [krullDim_le_iff R 1]
intro H p intro H p
apply le_of_not_gt apply le_of_not_gt

View file

@ -87,19 +87,15 @@ theorem hilbert_polynomial_0 (𝒜 : → Type _) (𝓜 : → Type _) [
: true := by : true := by
sorry sorry
lemma ass_graded (𝒜 : → Type _) (𝓜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) : (HomogeneousMax 𝒜 p) := by
sorry
lemma Associated_prime_of_graded_is_graded lemma Associated_prime_of_graded_is_graded
(𝒜 : → Type _) (𝓜 : → Type _) (𝒜 : → Type _) (𝓜 : → Type _)
[∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)] [∀ i, AddCommGroup (𝒜 i)] [∀ i, AddCommGroup (𝓜 i)]
[DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜] [DirectSum.GCommRing 𝒜] [DirectSum.Gmodule 𝒜 𝓜]
(p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i)) (p : associatedPrimes (⨁ i, 𝒜 i) (⨁ i, 𝓜 i))
: (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of x i}).annihilator)) := by : (Ideal.IsHomogeneous' 𝒜 p) ∧ ((∃ (i : ), ∃ (x : 𝒜 i), p = (Submodule.span (⨁ i, 𝒜 i) {DirectSum.of _ i x}).annihilator)) := by
sorry sorry
def standard_graded (𝒜 : → Type _) [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (I : Ideal (⨁ i, 𝒜 i)) := (⨁ i, 𝒜 i) -- def standard_graded {𝒜 : → Type _} [∀ i, AddCommGroup (𝒜 i)] [DirectSum.GCommRing 𝒜] (n : ) :
-- Prop :=
-- ∃ J, Ideal.IsHomogeneous' 𝒜 J (J :Nonempty ((⨁ i, 𝒜 i) ≃+* (MvPolynomial (Fin n) (𝒜 0)) J)

View file

@ -1,24 +1,6 @@
import Mathlib
import Mathlib.Algebra.MonoidAlgebra.Basic
import Mathlib.Data.Finset.Sort
import Mathlib.Order.Height import Mathlib.Order.Height
import Mathlib.Order.KrullDimension
import Mathlib.Order.JordanHolder
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.Height
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Ideal.Operations
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.RingTheory.GradedAlgebra.Basic
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal
import Mathlib.Algebra.Module.GradedModule
import Mathlib.RingTheory.Ideal.AssociatedPrime
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Artinian
import Mathlib.Algebra.Module.GradedModule
import Mathlib.RingTheory.Noetherian
import Mathlib.RingTheory.Finiteness
import Mathlib.RingTheory.Ideal.Operations
-- Setting for "library_search" -- Setting for "library_search"
set_option maxHeartbeats 0 set_option maxHeartbeats 0