comm_alg/CommAlg/grant.lean
2023-06-14 04:51:49 +00:00

228 lines
No EOL
7.6 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Order.KrullDimension
import Mathlib.Order.JordanHolder
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.Height
import CommAlg.krull
#check (p q : PrimeSpectrum _) → (p ≤ q)
#check Preorder (PrimeSpectrum _)
-- Dimension of a ring
#check krullDim (PrimeSpectrum _)
-- Length of a module
#check krullDim (Submodule _ _)
#check JordanHolderLattice
section Chains
variable {α : Type _} [Preorder α] (s : Set α)
def finFun_to_list {n : } : (Fin n → α) → List α := by sorry
def series_to_chain : StrictSeries s → s.subchain
| ⟨length, toFun, strictMono⟩ =>
⟨ finFun_to_list (fun x => toFun x),
sorry⟩
-- there should be a coercion from WithTop to WithBot (WithTop ) but it doesn't seem to work
-- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
-- actually it looks like we can coerce to WithBot (ℕ∞) fine
lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop )) = krullDim s := by
intro hs
unfold Set.chainHeight
unfold krullDim
have hKrullSome : ∃n, krullDim s = some n := by
sorry
-- norm_cast
sorry
end Chains
section Krull
variable (R : Type _) [CommRing R] (M : Type _) [AddCommGroup M] [Module R M]
open Ideal
-- chain of primes
#check height
lemma lt_height_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := 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
. -- change ∃c, _ ∧ _ ∧ ((List.length c : ℕ∞) = + 1) at h
-- rw [WithTop.top_add] at h
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 → 𝔮 < 𝔭) ∧ _) ↔ _
-- have h := fun (c : List (PrimeSpectrum R)) => (@WithTop.coe_eq_coe _ (List.length c) n)
constructor <;> rintro ⟨c, hc⟩ <;> use c --<;> tauto--<;> exact ⟨hc.1, by tauto⟩
. --rw [and_assoc]
-- show _ ∧ _ ∧ _
--exact ⟨hc.1, _⟩
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' _
lemma height_le_iff {𝔭 : PrimeSpectrum R} {n : ℕ∞} :
height 𝔭 ≤ n ↔ ∀ c : List (PrimeSpectrum R), c ∈ {I : PrimeSpectrum R | I < 𝔭}.subchain ∧ c.length = n + 1 := by
sorry
lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
have h := dim_eq_bot_iff.not.mpr (not_subsingleton R)
lift (Ideal.krullDim R) to ℕ∞ using h with k
use k
-- lemma krullDim_le_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
-- Ideal.krullDim R ≤ n ↔ (∀ c : List (PrimeSpectrum R), c.Chain' (· < ·) → c.length ≤ n + 1) := by
-- sorry
-- lemma krullDim_ge_iff' (R : Type _) [CommRing R] {n : WithBot ℕ∞} :
-- Ideal.krullDim R ≥ n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ c.length = n + 1 := sorry
lemma primeSpectrum_empty_of_subsingleton (x : PrimeSpectrum R) [Subsingleton R] : False :=
x.1.ne_top_iff_one.1 x.2.1 <| Eq.substr (Subsingleton.elim 1 (0 : R)) x.1.zero_mem
lemma primeSpectrum_empty_iff : IsEmpty (PrimeSpectrum R) ↔ Subsingleton R := by
constructor
. contrapose
rw [not_isEmpty_iff, ←not_nontrivial_iff_subsingleton, not_not]
apply PrimeSpectrum.instNonemptyPrimeSpectrum
. intro h
by_contra hneg
rw [not_isEmpty_iff] at hneg
rcases hneg with ⟨a, ha⟩
exact primeSpectrum_empty_of_subsingleton R ⟨a, ha⟩
/-- A ring has Krull dimension -∞ if and only if it is the zero ring -/
lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
unfold Ideal.krullDim
rw [←primeSpectrum_empty_iff, iSup_eq_bot]
constructor <;> intro h
. rw [←not_nonempty_iff]
rintro ⟨a, ha⟩
specialize h ⟨a, ha⟩
tauto
. rw [h.forall_iff]
trivial
#check (sorry : False)
#check (sorryAx)
#check (4 : WithBot ℕ∞)
#check List.sum
#check (_ ∈ (_ : List _))
variable (α : Type )
#synth Membership α (List α)
#check bot_lt_iff_ne_bot
-- #check ((4 : ℕ∞) : WithBot (WithTop ))
-- #check ( (Set.chainHeight s) : WithBot (ℕ∞))
/-- 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. -/
lemma dim_le_one_of_dimLEOne : Ring.DimensionLEOne R → krullDim R ≤ (1 : ) := by
rw [krullDim_le_iff R 1]
-- unfold Ring.DimensionLEOne
intro H p
-- have Hp := H p.asIdeal
-- have Hp := fun h => (Hp h) p.IsPrime
apply le_of_not_gt
intro h
rcases ((lt_height_iff'' R).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)
-- generalize hq0 : List.get _ _ = q0 at hc1
set q0 : PrimeSpectrum R := List.get c { val := 0, isLt := _ }
set q1 : PrimeSpectrum R := List.get c { val := 1, isLt := _ }
-- have hq0 : q0 ∈ c := List.get_mem _ _ _
-- have hq1 : q1 ∈ c := List.get_mem _ _ _
specialize hc2 q1 (List.get_mem _ _ _)
-- have aa := (bot_le : (⊥ : Ideal R) ≤ q0.asIdeal)
change q0.asIdeal < q1.asIdeal at hc1
have q1nbot := Trans.trans (bot_le : ⊥ ≤ q0.asIdeal) hc1
specialize H q1.asIdeal (bot_lt_iff_ne_bot.mp q1nbot) q1.IsPrime
-- change q1.asIdeal < p.asIdeal at hc2
apply IsPrime.ne_top p.IsPrime
apply (IsCoatom.lt_iff H.out).mp
exact hc2
--refine Iff.mp radical_eq_top (?_ (id (Eq.symm hc3)))
end Krull
section iSupWithBot
variable {α : Type _} [CompleteSemilatticeSup α] {I : Type _} (f : I → α)
#synth SupSet (WithBot ℕ∞)
protected lemma WithBot.iSup_ge_coe_iff {a : α} :
(a ≤ ⨆ i : I, (f i : WithBot α) ) ↔ ∃ i : I, f i ≥ a := by
rw [WithBot.coe_le_iff]
sorry
end iSupWithBot
section myGreatElab
open Lean Meta Elab
syntax (name := lhsStx) "lhs% " term:max : term
syntax (name := rhsStx) "rhs% " term:max : term
@[term_elab lhsStx, term_elab rhsStx]
def elabLhsStx : Term.TermElab := fun stx expectedType? =>
match stx with
| `(lhs% $t) => do
let (lhs, _, eq) ← mkExpected expectedType?
discard <| Term.elabTermEnsuringType t eq
return lhs
| `(rhs% $t) => do
let (_, rhs, eq) ← mkExpected expectedType?
discard <| Term.elabTermEnsuringType t eq
return rhs
| _ => throwUnsupportedSyntax
where
mkExpected expectedType? := do
let α
if let some expectedType := expectedType? then
pure expectedType
else
mkFreshTypeMVar
let lhs ← mkFreshExprMVar α
let rhs ← mkFreshExprMVar α
let u ← getLevel α
let eq := mkAppN (.const ``Eq [u]) #[α, lhs, rhs]
return (lhs, rhs, eq)
#check lhs% (add_comm 1 2)
#check rhs% (add_comm 1 2)
#check lhs% (add_comm _ _ : _ = 1 + 2)
example (x y : α) (h : x = y) : lhs% h = rhs% h := h
def lhsOf {α : Sort _} {x y : α} (h : x = y) : α := x
#check lhsOf (add_comm 1 2)