English
For a Noetherian ring R and ideal I ≠ ⊤, there exists J ≤ I with J.spanRank = I.height and J.height = I.height.
Русский
Для кольца Ноetherian R и идеала I ≠ ⊤ существует J ≤ I такое, что J.spanRank = I.height и J.height = I.height.
LaTeX
$$$\exists J \leq I,\; J.spanRank = I.height \wedge J.height = I.height$$$
Lean4
/-- **Krull's height theorem** (also known as **Krullscher Höhensatz**) :
In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated
by `n` elements has height at most `n`. -/
nonrec theorem height_le_spanRank_toENat_of_mem_minimal_primes (I : Ideal R) (p : Ideal R) (hp : p ∈ I.minimalPrimes) :
p.height ≤ I.spanRank.toENat := by
classical
rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
rintro ⟨s, (rfl : span s = I)⟩
induction hn : s.card using Nat.strong_induction_on generalizing R with
| h n H =>
replace hn : s.card ≤ n := hn.le
have := hp.1.1
cases n with
|
zero =>
rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_primeHeight p, primeHeight_eq_zero_iff, minimalPrimes]
simp_all
| succ n =>
wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
· rw [← Localization.AtPrime.comap_maximalIdeal (I := p)] at hp ⊢
rw [IsLocalization.height_comap p.primeCompl]
rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
exact
this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp) inferInstance _ H
(Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
obtain ⟨_, rfl⟩ := hR
simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
intro q hq hpq hq'
obtain ⟨x, s', hxs', rfl, hxq⟩ : ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q :=
by
have : ¬(s : Set R) ⊆ q := by
rw [← span_le]
exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩
have : maximalIdeal R ≤ (q ⊔ span { x }).radical :=
by
rw [radical_eq_sInf, le_sInf_iff]
exact fun J ⟨hJ, hJ'⟩ ↦
by_contra fun h ↦
hq' J hJ'
((SetLike.lt_iff_le_and_exists.mpr
⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le
hJ)
((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
have h : (s' : Set R) ⊆ (q ⊔ span { x }).radical :=
by
have := hp.1.2.trans this
rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this
exact this.2
obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
let t := Finset.univ.image t
suffices hq : q ∈ (span t).minimalPrimes from
have tcard : t.card ≤ n :=
Nat.le_of_lt_succ
((Finset.card_image_le.trans_lt <| by simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')).trans_le
hn)
(H _ (tcard.trans_lt n.lt_succ_self) q t hq rfl).trans (by norm_cast)
rw [Finset.coe_insert] at hp
convert mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
· simp [t]
refine hspan.trans <| radical_mono ?_
rw [← Set.union_singleton, span_union]
