Merge branch 'GTBarkley:main' into main

CommAlg/grant.lean

@@ -83,6 +83,16 @@ height 𝔭 > n ↔ ∃ c : List (PrimeSpectrum R), c.Chain' (· < ·) ∧ (∀
     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
@@ -116,19 +126,103 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   constructor <;> intro h
   . rw [←not_nonempty_iff]
     rintro ⟨a, ha⟩
-    -- specialize h ⟨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 (ℕ∞))
 
-variable (P : PrimeSpectrum R)
+/-- 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
 
-#check {J | J < P}.le_chainHeight_iff (n := 4)
+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)

CommAlg/jayden(krull-dim-zero).lean

@@ -77,12 +77,25 @@ lemma containment_radical_power_containment :
     rintro ⟨RisNoetherian, containment⟩ 
     rw [isNoetherianRing_iff_ideal_fg] at RisNoetherian
     specialize RisNoetherian (Ideal.radical I)
-    rcases RisNoetherian with ⟨S, Sgenerates⟩
+    -- rcases RisNoetherian with ⟨S, Sgenerates⟩
+    have containment2 : ∃ n : ℕ,  (Ideal.radical I) ^ n ≤ I := by
+      apply Ideal.exists_radical_pow_le_of_fg I RisNoetherian
+    cases' containment2 with n containment2'
+    have containment3 : J ^ n ≤ (Ideal.radical I) ^ n := by 
+      apply Ideal.pow_mono containment
+    use n
+    apply le_trans containment3 containment2'
+-- The above can be proven using the following quicker theorem that is in the wrong place.
+-- Ideal.exists_pow_le_of_le_radical_of_fG
 
-    -- how to I get a generating set?
 
 -- Stacks Lemma 10.52.6: I is a maximal ideal and IM = 0. Then length of M is
--- 
+-- the same as the dimension as a vector space over R/I,
+lemma length_eq_dim_if_maximal_annihilates {I : Ideal R} [Ideal.IsMaximal I] 
+    : I • (⊤ : Submodule R M) = 0
+     → Module.length R M = Module.rank R⧸I M⧸(I • (⊤ : Submodule R M)) := by sorry
+
+-- Does lean know that M/IM is a R/I module?
 
 -- Stacks Lemma 10.52.8: I is a finitely generated maximal ideal of R.
 -- M is a finite R-mod and I^nM=0. Then length of M is finite.

CommAlg/krull.lean

@@ -25,11 +25,11 @@ variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
 
 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 krullDim (R : Type _) [CommRing R] : WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), 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
+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
 
 noncomputable instance : CompleteLattice (WithBot (ℕ∞)) := WithBot.WithTop.completeLattice
 
@@ -42,13 +42,13 @@ lemma height_le_of_le {I J : PrimeSpectrum R} (I_le_J : I ≤ J) : height I ≤
 lemma krullDim_le_iff (R : Type _) [CommRing R] (n : ℕ) :
   krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
-lemma krullDim_le_iff' (R : Type) [CommRing R] (n : ℕ∞) :
+lemma krullDim_le_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
   krullDim R ≤ n ↔ ∀ I : PrimeSpectrum R, (height I : WithBot ℕ∞) ≤ ↑n := iSup_le_iff (α := WithBot ℕ∞)
 
-lemma le_krullDim_iff (R : Type) [CommRing R] (n : ℕ) :
+lemma le_krullDim_iff (R : Type _) [CommRing R] (n : ℕ) :
   n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
 
-lemma le_krullDim_iff' (R : Type) [CommRing R] (n : ℕ∞) :
+lemma le_krullDim_iff' (R : Type _) [CommRing R] (n : ℕ∞) :
   n ≤ krullDim R ↔ ∃ I : PrimeSpectrum R, n ≤ (height I : WithBot ℕ∞) := by sorry
 
 @[simp]
@@ -94,11 +94,17 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
   . rw [h.forall_iff]
     trivial
 
-lemma krullDim_nonneg_of_nontrivial [Nontrivial R] : ∃ n : ℕ∞, Ideal.krullDim R = n := by
+lemma krullDim_nonneg_of_nontrivial (R : Type _) [CommRing R] [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 dim_eq_zero_iff [Nontrivial R] : krullDim R = 0 ↔ ∀ I : PrimeSpectrum R, IsMaximal I.asIdeal := by
+  constructor <;> intro h
+  . intro I
+    sorry
+  . sorry
+  
 @[simp]
 lemma field_prime_bot {K: Type _} [Field K] (P : Ideal K) : IsPrime P ↔ P = ⊥ := by
       constructor
@@ -158,8 +164,58 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D =
     exact dim_field_eq_zero
 
 #check Ring.DimensionLEOne
+-- This lemma is false!
 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
+  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]
+  intro H p
+  apply le_of_not_gt
+  intro h
+  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)
+  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 _ _ _)
+  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
+  apply IsPrime.ne_top p.IsPrime
+  apply (IsCoatom.lt_iff H.out).mp
+  exact hc2
+
 lemma dim_le_one_of_pid [IsDomain R] [IsPrincipalIdealRing R] : krullDim R ≤ 1 := by
   rw [dim_le_one_iff]
   exact Ring.DimensionLEOne.principal_ideal_ring R