|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Nailin Guan. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Nailin Guan, Yongle Hu |
| 5 | +-/ |
| 6 | +import Mathlib.RingTheory.Flat.TorsionFree |
| 7 | +import Mathlib.RingTheory.KrullDimension.Module |
| 8 | +import Mathlib.RingTheory.Regular.RegularSequence |
| 9 | +import Mathlib.RingTheory.Spectrum.Prime.LTSeries |
| 10 | + |
| 11 | +/-! |
| 12 | +
|
| 13 | +# Krull Dimension of quotient regular sequence |
| 14 | +
|
| 15 | +## Main results |
| 16 | +
|
| 17 | +- `Module.supportDim_add_length_eq_supportDim_of_isRegular`: If `M` is a finite module over a |
| 18 | + Noetherian local ring `R`, `r₁, …, rₙ` is an `M`-sequence, then |
| 19 | + `dim M/(r₁, …, rₙ)M + n = dim M`. |
| 20 | +-/ |
| 21 | + |
| 22 | +namespace Module |
| 23 | + |
| 24 | +variable {R : Type*} [CommRing R] [IsNoetherianRing R] |
| 25 | + {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] |
| 26 | + |
| 27 | +open RingTheory Sequence IsLocalRing Ideal PrimeSpectrum Pointwise |
| 28 | + |
| 29 | +omit [IsNoetherianRing R] [Module.Finite R M] in |
| 30 | +lemma exists_ltSeries_support_isMaximal_last_of_ltSeries_support (q : LTSeries (support R M)) : |
| 31 | + ∃ p : LTSeries (support R M), q.length ≤ p.length ∧ p.last.1.1.IsMaximal := by |
| 32 | + obtain ⟨m, hmm, hm⟩ := exists_le_maximal _ q.last.1.2.1 |
| 33 | + obtain hlt | rfl := lt_or_eq_of_le hm |
| 34 | + · use q.snoc ⟨⟨m, inferInstance⟩, mem_support_mono hm q.last.2⟩ hlt |
| 35 | + simpa |
| 36 | + · use q |
| 37 | + |
| 38 | +theorem supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson {x : R} |
| 39 | + (h : x ∈ (annihilator R M).jacobson) : supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1 := by |
| 40 | + nontriviality M |
| 41 | + refine iSup_le_iff.mpr (fun p ↦ ?_) |
| 42 | + wlog hxp : x ∈ p.last.1.1 generalizing p |
| 43 | + · obtain ⟨p, hle, hm⟩ := exists_ltSeries_support_isMaximal_last_of_ltSeries_support p |
| 44 | + have hj : (annihilator R M).jacobson ≤ p.last.1.1 := |
| 45 | + sInf_le ⟨mem_support_iff_of_finite.mp p.last.2, inferInstance⟩ |
| 46 | + exact (Nat.cast_le.mpr hle).trans <| this _ (hj h) |
| 47 | + -- `q` is a chain of primes such that `x ∈ q 1`, `p.length = q.length` and `p.head = q.head`. |
| 48 | + obtain ⟨q, hxq, hq, h0, _⟩ : ∃ q : LTSeries (PrimeSpectrum R), _ ∧ _ ∧ p.head = q.head ∧ _ := |
| 49 | + exist_ltSeries_mem_one_of_mem_last (p.map Subtype.val (fun ⦃_ _⦄ lt ↦ lt)) hxp |
| 50 | + by_cases hp0 : p.length = 0 |
| 51 | + · have hb : supportDim R (QuotSMulTop x M) ≠ ⊥ := |
| 52 | + (supportDim_ne_bot_iff_nontrivial R (QuotSMulTop x M)).mpr <| |
| 53 | + Submodule.Quotient.nontrivial_of_ne_top _ <| |
| 54 | + (Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator h).symm |
| 55 | + rw [hp0, ← WithBot.coe_unbot (supportDim R (QuotSMulTop x M)) hb] |
| 56 | + exact WithBot.coe_le_coe.mpr (zero_le ((supportDim R (QuotSMulTop x M)).unbot hb + 1)) |
| 57 | + -- Let `q' i := q (i + 1)`, then `q'` is a chain of prime ideals in `Supp(M/xM)`. |
| 58 | + let q' : LTSeries (support R (QuotSMulTop x M)) := { |
| 59 | + length := p.length - 1 |
| 60 | + toFun := by |
| 61 | + intro ⟨i, hi⟩ |
| 62 | + have hi : i + 1 < q.length + 1 := |
| 63 | + Nat.succ_lt_succ (hi.trans_eq ((Nat.sub_add_cancel (Nat.pos_of_ne_zero hp0)).trans hq)) |
| 64 | + exact ⟨q ⟨i + 1, hi⟩, by simpa using |
| 65 | + ⟨mem_support_mono (by simpa [h0] using q.monotone (Fin.zero_le _)) p.head.2, q.monotone |
| 66 | + ((Fin.natCast_eq_mk (Nat.lt_of_add_left_lt hi)).trans_le (Nat.le_add_left 1 i)) hxq⟩⟩ |
| 67 | + step := by exact fun _ ↦ q.strictMono (by simp) |
| 68 | + } |
| 69 | + calc (p.length : WithBot ℕ∞) ≤ (p.length - 1 + 1 : ℕ) := Nat.cast_le.mpr le_tsub_add |
| 70 | + _ ≤ _ := by simpa using add_le_add_right (by exact le_iSup_iff.mpr fun _ h ↦ h q') 1 |
| 71 | + |
| 72 | +omit [IsNoetherianRing R] in |
| 73 | +/-- If `M` is a finite module over a commutative ring `R`, `x ∈ M` is not in any minimal prime of |
| 74 | + `M`, then `dim M/xM + 1 ≤ dim M`. -/ |
| 75 | +theorem supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes {x : R} |
| 76 | + (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) : |
| 77 | + supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M := by |
| 78 | + nontriviality M |
| 79 | + nontriviality (QuotSMulTop x M) |
| 80 | + have : Nonempty (Module.support R M) := nonempty_support_of_nontrivial.to_subtype |
| 81 | + have : Nonempty (Module.support R (QuotSMulTop x M)) := nonempty_support_of_nontrivial.to_subtype |
| 82 | + simp only [supportDim, Order.krullDim_eq_iSup_length] |
| 83 | + apply WithBot.coe_le_coe.mpr |
| 84 | + simp only [ENat.iSup_add, iSup_le_iff] |
| 85 | + intro p |
| 86 | + have hp := p.head.2 |
| 87 | + simp only [support_quotSMulTop, Set.mem_inter_iff, mem_zeroLocus, Set.singleton_subset_iff] at hp |
| 88 | + have le : support R (QuotSMulTop x M) ⊆ support R M := by simp |
| 89 | + -- Since `Supp(M/xM) ⊆ Supp M`, `p` can be viewed as a chain of prime ideals in `Supp M`, |
| 90 | + -- which we denote by `q`. |
| 91 | + let q : LTSeries (support R M) := |
| 92 | + p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) (fun _ _ h ↦ h) |
| 93 | + obtain ⟨r, hrm, hr⟩ := exists_minimalPrimes_le (mem_support_iff_of_finite.mp q.head.2) |
| 94 | + let r : support R M := ⟨⟨r, minimalPrimes_isPrime hrm⟩, mem_support_iff_of_finite.mpr hrm.1.2⟩ |
| 95 | + have hr : r < q.head := lt_of_le_of_ne hr (fun h ↦ hn q.head.1.1 (by rwa [← h]) hp.2) |
| 96 | + exact le_of_eq_of_le (by simp [q]) (le_iSup _ (q.cons r hr)) |
| 97 | + |
| 98 | +theorem supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson {x : R} |
| 99 | + (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) (hx : x ∈ (annihilator R M).jacobson) : |
| 100 | + supportDim R (QuotSMulTop x M) + 1 = supportDim R M := |
| 101 | + le_antisymm (supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes hn) |
| 102 | + (supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson hx) |
| 103 | + |
| 104 | +theorem supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson {x : R} (reg : IsSMulRegular M x) |
| 105 | + (hx : x ∈ (annihilator R M).jacobson) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M := |
| 106 | + supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson |
| 107 | + (fun _ ↦ reg.notMem_of_mem_minimalPrimes) hx |
| 108 | + |
| 109 | +lemma _root_.ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson {x : R} |
| 110 | + (reg : IsSMulRegular R x) (hx : x ∈ Ring.jacobson R) : |
| 111 | + ringKrullDim (R ⧸ span {x}) + 1 = ringKrullDim R := by |
| 112 | + have h := Submodule.ideal_span_singleton_smul x (⊤ : Ideal R) |
| 113 | + simp only [smul_eq_mul, mul_top] at h |
| 114 | + rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R h).toRingEquiv, |
| 115 | + ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim] |
| 116 | + exact supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg |
| 117 | + ((annihilator R R).ringJacobson_le_jacobson hx) |
| 118 | + |
| 119 | +variable [IsLocalRing R] |
| 120 | + |
| 121 | +/-- If `M` is a finite module over a Noetherian local ring `R`, then `dim M ≤ dim M/xM + 1` |
| 122 | + for every `x` in the maximal ideal of the local ring `R`. -/ |
| 123 | +@[stacks 0B52 "the second inequality"] |
| 124 | +theorem supportDim_le_supportDim_quotSMulTop_succ {x : R} (hx : x ∈ maximalIdeal R) : |
| 125 | + supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1 := |
| 126 | + supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson ((maximalIdeal_le_jacobson _) hx) |
| 127 | + |
| 128 | +@[stacks 0B52 "the equality case"] |
| 129 | +theorem supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal {x : R} |
| 130 | + (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) (hx : x ∈ maximalIdeal R) : |
| 131 | + supportDim R (QuotSMulTop x M) + 1 = supportDim R M := |
| 132 | + supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson hn <| |
| 133 | + (maximalIdeal_le_jacobson _) hx |
| 134 | + |
| 135 | +theorem supportDim_quotSMulTop_succ_eq_supportDim {x : R} (reg : IsSMulRegular M x) |
| 136 | + (hx : x ∈ maximalIdeal R) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M := |
| 137 | + supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson reg ((maximalIdeal_le_jacobson _) hx) |
| 138 | + |
| 139 | +lemma _root_.ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim {x : R} |
| 140 | + (reg : IsSMulRegular R x) (hx : x ∈ maximalIdeal R) : |
| 141 | + ringKrullDim (R ⧸ span {x}) + 1 = ringKrullDim R := |
| 142 | + ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson reg <| by |
| 143 | + rwa [ringJacobson_eq_maximalIdeal R] |
| 144 | + |
| 145 | +open nonZeroDivisors in |
| 146 | +@[stacks 00KW] |
| 147 | +lemma _root_.ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors |
| 148 | + {x : R} (reg : x ∈ R⁰) (hx : x ∈ maximalIdeal R) : |
| 149 | + ringKrullDim (R ⧸ span {x}) + 1 = ringKrullDim R := |
| 150 | + ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim |
| 151 | + (Module.Flat.isSMulRegular_of_nonZeroDivisors reg) hx |
| 152 | + |
| 153 | +/-- If `M` is a finite module over a Noetherian local ring `R`, `r₁, …, rₙ` is an |
| 154 | + `M`-sequence, then `dim M/(r₁, …, rₙ)M + n = dim M`. -/ |
| 155 | +theorem supportDim_add_length_eq_supportDim_of_isRegular (rs : List R) (reg : IsRegular M rs) : |
| 156 | + supportDim R (M ⧸ ofList rs • (⊤ : Submodule R M)) + rs.length = supportDim R M := by |
| 157 | + induction rs generalizing M with |
| 158 | + | nil => |
| 159 | + rw [ofList_nil, Submodule.bot_smul] |
| 160 | + simpa using supportDim_eq_of_equiv (Submodule.quotEquivOfEqBot ⊥ rfl) |
| 161 | + | cons x rs' ih => |
| 162 | + have mem : x ∈ maximalIdeal R := by |
| 163 | + simpa using fun isu ↦ reg.2 (by simp [span_singleton_eq_top.mpr isu]) |
| 164 | + simp [supportDim_eq_of_equiv (Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M x _), |
| 165 | + ← supportDim_quotSMulTop_succ_eq_supportDim ((isRegular_cons_iff M _ _).mp reg).1 mem, |
| 166 | + ← ih ((isRegular_cons_iff M _ _).mp reg).2, ← add_assoc] |
| 167 | + |
| 168 | +lemma _root_.ringKrullDim_add_length_eq_ringKrullDim_of_isRegular (rs : List R) |
| 169 | + (reg : IsRegular R rs) : ringKrullDim (R ⧸ ofList rs) + rs.length = ringKrullDim R := by |
| 170 | + have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp |
| 171 | + rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R eq).toRingEquiv, |
| 172 | + ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim] |
| 173 | + exact supportDim_add_length_eq_supportDim_of_isRegular rs reg |
| 174 | + |
| 175 | +end Module |
0 commit comments