feat(RingTheory/KrullDimension): dimension of polynomial ring (leanprover-community#27542)

We show that for a Noetherian ring `R`, `dim R[X] = dim R + 1`.

Co-authored by: Sihan Su <ssh@stu.pku.edu.cn>
Co-authored by: Yi Song <sif4delta0@mail.ustc.edu.cn>

Co-authored-by: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com>
Co-authored-by: Nailin Guan <150537269+Thmoas-Guan@users.noreply.github.com>

Author: 3 people

Mathlib/Order/KrullDimension.lean

@@ -460,6 +460,14 @@ lemma coheight_ne_zero {x : α} : coheight x ≠ 0 ↔ ¬ IsMax x := coheight_eq
 
 @[simp] lemma coheight_top (α : Type*) [Preorder α] [OrderTop α] : coheight (⊤ : α) = 0 := by simp
 
+lemma height_pos_of_bot_lt {x : α} [OrderBot α] (h : ⊥ < x) : 0 < height x := by
+  rw [height_pos]
+  grind [not_isMin_iff]
+
+lemma coheight_pos_of_lt_top {x : α} [OrderTop α] (h : x < ⊤) : 0 < coheight x := by
+  rw [coheight_pos]
+  grind [not_isMax_iff]
+
 lemma coe_lt_height_iff {x : α} {n : ℕ} (hfin : height x < ⊤) :
     n < height x ↔ ∃ y < x, height y = n where
   mp h := by

Mathlib/RingTheory/Ideal/Height.lean

@@ -340,6 +340,18 @@ theorem IsLocalization.AtPrime.ringKrullDim_eq_height (I : Ideal R) [I.IsPrime]
       ← IsLocalization.AtPrime.comap_maximalIdeal A I,
       Ideal.height_eq_primeHeight]
 
+lemma IsLocalization.height_map_of_disjoint {S : Type*} [CommRing S] [Algebra R S] (M : Submonoid R)
+    [IsLocalization M S] (p : Ideal R) [p.IsPrime] (h : Disjoint (M : Set R) (p : Set R)) :
+    (p.map <| algebraMap R S).height = p.height := by
+  let P := p.map (algebraMap R S)
+  have : P.IsPrime := isPrime_of_isPrime_disjoint M S p ‹_› h
+  have := isLocalization_isLocalization_atPrime_isLocalization (M := M) (Localization.AtPrime P) P
+  simp_rw [P, comap_map_of_isPrime_disjoint M S p _ h] at this
+  have := ringKrullDim_eq_of_ringEquiv (IsLocalization.algEquiv p.primeCompl
+    (Localization.AtPrime P) (Localization.AtPrime p)).toRingEquiv
+  rw [AtPrime.ringKrullDim_eq_height P, AtPrime.ringKrullDim_eq_height p] at this
+  exact WithBot.coe_eq_coe.mp this
+
 lemma mem_minimalPrimes_of_primeHeight_eq_height {I J : Ideal R} [J.IsPrime] (e : I ≤ J)
     (e' : J.primeHeight = I.height) [J.FiniteHeight] : J ∈ I.minimalPrimes := by
   rw [← J.height_eq_primeHeight] at e'

Mathlib/RingTheory/KrullDimension/Polynomial.lean

@@ -1,23 +1,29 @@
 /-
 Copyright (c) 2025 Jingting Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jingting Wang
+Authors: Jingting Wang, Sihan Su, Yi Song, Christian Merten
 -/
 module
 
 public import Mathlib.Algebra.Polynomial.FieldDivision
 public import Mathlib.RingTheory.KrullDimension.PID
 public import Mathlib.RingTheory.LocalRing.ResidueField.Fiber
+public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem
+public import Mathlib.RingTheory.KrullDimension.NonZeroDivisors
 
 /-!
 # Krull dimension of polynomial ring
 
-This file proves properties of the krull dimension of the polynomial ring over a commutative ring
+This file proves properties of the Krull dimension of the polynomial ring over a commutative ring
 
 ## Main results
 
-* `Polynomial.ringKrullDim_le`: the krull dimension of the polynomial ring over a commutative ring
+* `Polynomial.ringKrullDim_le`: the Krull dimension of the polynomial ring over a commutative ring
   `R` is less than `2 * (ringKrullDim R) + 1`.
+For noetherian rings:
+* `Polynomial.ringKrullDim_of_isNoetherianRing`: the Krull dimension of `R[X]` is `dim R + 1`.
+* `MvPolynomial.ringKrullDim_of_isNoetherianRing`: the Krull dimension of `R[X₁, ..., Xₙ]` is
+  `dim R + n`.
 -/
 
 public section
@@ -32,3 +38,92 @@ theorem Polynomial.ringKrullDim_le {R : Type*} [CommRing R] :
       ← ringKrullDim_eq_of_ringEquiv (polyEquivTensor R (p.asIdeal.ResidueField)).toRingEquiv,
       ← Ring.krullDimLE_iff]
     infer_instance
+
+variable {R : Type*} [CommRing R] [IsNoetherianRing R]
+
+namespace Polynomial
+
+open Ideal IsLocalization
+
+/--
+Let `p` be a maximal ideal of `A`. If `P` is a maximal ideal of `A[X]` lying above `p`,
+then `ht(P) = ht(p) + 1`.
+See `Polynomial.height_eq_height_add_one` for the more general version that does not assume `p` is
+maximal.
+-/
+private lemma height_eq_height_add_one_of_isMaximal (p : Ideal R) [p.IsMaximal] (P : Ideal R[X])
+    [P.IsMaximal] [P.LiesOver p] : P.height = p.height + 1 := by
+  let _ : Field (R ⧸ p) := Quotient.field p
+  suffices h : (P.map (Ideal.Quotient.mk (Ideal.map (algebraMap R R[X]) p))).height = 1 by
+    rw [height_eq_height_add_of_liesOver_of_hasGoingDown p, h]
+  let e : (R[X] ⧸ (p.map C)) ≃+* (R ⧸ p)[X] := (polynomialQuotientEquivQuotientPolynomial p).symm
+  let P' : Ideal (R ⧸ p)[X] := Ideal.map e <| P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))
+  have : (P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))).IsMaximal := by
+    refine .map_of_surjective_of_ker_le Quotient.mk_surjective ?_
+    rw [mk_ker, LiesOver.over (P := P) (p := p)]
+    exact map_comap_le
+  have : P'.IsMaximal := map_isMaximal_of_equiv e
+  have : P'.height = 1 := IsPrincipalIdealRing.height_eq_one_of_isMaximal P' polynomial_not_isField
+  rwa [← e.height_map <| P.map (Ideal.Quotient.mk <| p.map (algebraMap R R[X]))]
+
+/-- Let `p` be a maximal ideal of `R`. Then the height of `p[X]` equals the height of `p`. -/
+lemma height_map_C (p : Ideal R) [p.IsMaximal] : (p.map C).height = p.height := by
+  have : (p.map C).LiesOver p := ⟨IsMaximal.eq_of_le inferInstance IsPrime.ne_top' le_comap_map⟩
+  simp [height_eq_height_add_of_liesOver_of_hasGoingDown p]
+
+attribute [local instance] Polynomial.algebra Polynomial.isLocalization in
+/-- Let `p` be a prime ideal of `R`. If `P` is a maximal ideal of `R[X]` lying over `p`,
+`ht(P) = ht(p) + 1`. -/
+lemma height_eq_height_add_one (p : Ideal R)
+    (P : Ideal R[X]) [P.IsMaximal] [P.LiesOver p] :
+    P.height = p.height + 1 := by
+  have : p.IsPrime := by rw [P.over_def p]; infer_instance
+  let Rₚ := Localization.AtPrime p
+  set p' : Ideal Rₚ := p.map (algebraMap R Rₚ) with p'_def
+  have : p'.IsMaximal := by
+    rw [p'_def, Localization.AtPrime.map_eq_maximalIdeal]
+    exact IsLocalRing.maximalIdeal.isMaximal Rₚ
+  let P' : Ideal Rₚ[X] := P.map (algebraMap R[X] Rₚ[X])
+  have disj : Disjoint (p.primeCompl.map C : Set R[X]) P := by
+    refine Set.disjoint_left.mpr fun a ⟨b, hb⟩ ha ↦ hb.1 ?_
+    rwa [SetLike.mem_coe, LiesOver.over (P := P) (p := p), mem_comap, algebraMap_eq, hb.2]
+  have eq := comap_map_of_isPrime_disjoint _ Rₚ[X] P ‹P.IsMaximal›.isPrime disj
+  have : (comap (algebraMap R[X] Rₚ[X]) P').IsMaximal := eq.symm ▸ ‹P.IsMaximal›
+  have : P'.IsMaximal := .of_isLocalization_of_disjoint (p.primeCompl.map C)
+  have : P'.LiesOver p' := liesOver_of_isPrime_of_disjoint p.primeCompl _ _ disj
+  have eq1 : p.height = p'.height := by
+    rw [height_map_of_disjoint p.primeCompl]
+    exact Disjoint.symm <| Set.disjoint_left.mpr fun _ a b ↦ b a
+  have eq2 : P.height = P'.height := by
+    rw [height_map_of_disjoint (Submonoid.map C <| p.primeCompl) _ disj]
+  rw [eq1, eq2]
+  apply height_eq_height_add_one_of_isMaximal p' P'
+
+/-- If `R` is Noetherian, `dim R[X] = dim R + 1`. -/
+@[simp]
+lemma ringKrullDim_of_isNoetherianRing : ringKrullDim R[X] = ringKrullDim R + 1 := by
+  refine le_antisymm ?_ ?_
+  · nontriviality R[X]
+    refine (ringKrullDim_le_iff_isMaximal_height_le (ringKrullDim R + 1)).mpr fun M hM ↦ ?_
+    rw [height_eq_height_add_one (M.under R) M, WithBot.coe_add, WithBot.coe_one]
+    gcongr
+    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'
+  · exact ringKrullDim_succ_le_ringKrullDim_polynomial
+
+end Polynomial
+
+/-- If `R` is Noetherian, `dim R[X₁, ..., Xₙ] = dim R + n`. -/
+@[simp]
+lemma MvPolynomial.ringKrullDim_of_isNoetherianRing {ι : Type*} [Finite ι] :
+    ringKrullDim (MvPolynomial ι R) = ringKrullDim R + Nat.card ι := by
+  induction ι using Finite.induction_empty_option with
+  | of_equiv e H =>
+    convert ← H using 1
+    · exact ringKrullDim_eq_of_ringEquiv (renameEquiv _ e).toRingEquiv
+    · rw [Nat.card_congr e]
+  | h_empty => simp
+  | h_option IH =>
+    simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
+      ← add_assoc] at IH ⊢
+    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
+      Polynomial.ringKrullDim_of_isNoetherianRing, IH]

Mathlib/RingTheory/Localization/AtPrime/Basic.lean

@@ -346,6 +346,32 @@ lemma IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes
     (minimalPrimes_eq_minimals (R := R) ▸ hp).eq_of_le i.1.2 i.2⟩
   (IsLocalization.AtPrime.primeSpectrumOrderIso S p).subsingleton
 
+open Ideal in
+/-- If `R'` (resp. `S'`) is the localization of `R` (resp. `S`) and
+`P` lies over `p` then the image of `P` in `S'` lies over the image of `p` in `R'`. -/
+lemma IsLocalization.liesOver_of_isPrime_of_disjoint {R' S' : Type*}
+    (M : Submonoid R) (T : Submonoid S)
+    [CommSemiring R'] [CommSemiring S'] [Algebra R R'] [Algebra S S'] [Algebra R' S']
+    [Algebra R S'] [IsScalarTower R S S'] [IsScalarTower R R' S']
+    [IsLocalization M R'] [IsLocalization T S']
+    (p : Ideal R) {P : Ideal S} [P.IsPrime] [P.LiesOver p]
+    (disj : Disjoint (T : Set S) (P : Set S)) :
+    (P.map (algebraMap S S')).LiesOver (p.map (algebraMap R R')) := by
+  suffices h : Ideal.map (algebraMap R R') (under R (under R' (P.map (algebraMap S S')))) =
+      Ideal.map (algebraMap R R') p by exact ⟨by rw [← h, IsLocalization.map_comap (M := M)]⟩
+  rw [under_under, ← under_under (B := S), under_def, under_def,
+    IsLocalization.comap_map_of_isPrime_disjoint (M := T) _ _ ‹_› disj,
+    LiesOver.over (P := P) (p := p)]
+
+lemma Ideal.IsMaximal.of_isLocalization_of_disjoint [IsLocalization M S] {J : Ideal S}
+    [(Ideal.comap (algebraMap R S) J).IsMaximal] : J.IsMaximal := by
+  obtain ⟨m, maxm, hm⟩ := exists_le_maximal J <| by
+    rintro rfl
+    exact Ideal.IsMaximal.ne_top ‹_› (by simp)
+  apply comap_mono (f := algebraMap R S) at hm
+  rwa [← IsLocalization.map_comap M S J, IsMaximal.eq_of_le ‹_› (IsPrime.under R m).ne_top hm,
+    Ideal.under_def, IsLocalization.map_comap M S m]
+
 end
 
 namespace IsLocalization.AtPrime