English
Let R be a Noetherian ring and p a prime ideal of R. Then there exists a finite subset S of R such that p is a minimal prime over the ideal generated by S, and the cardinality of S equals the Krull height of p.
Русский
Пусть R -- кольцо Ноether и p -- простый идеал в R. Существует конечный набор S элементов R, такой что p является минимальным над образом порождённого S идеала, и |S| = высота Крull(p).
LaTeX
$$$\\\\exists s : \\\\mathrm{Finset}(R), p \\\\in (\\\\mathrm{span}\, s).\\\\text{minimalPrimes} \\\\land \\\\; s.\\\\text{card} = p.\\\\text{height}$$$
Lean4
/-- If `p` is a prime in a Noetherian ring `R`, there exists a `p`-primary ideal `I`
spanned by `p.height` elements. -/
theorem exists_finset_card_eq_height_of_isNoetherianRing (p : Ideal R) [p.IsPrime] :
∃ s : Finset R, p ∈ (span s).minimalPrimes ∧ s.card = p.height :=
by
obtain ⟨I, hI, hr⟩ := (p.height_le_iff_exists_minimalPrimes <| p.height).mp le_rfl
have hs : I.generators.Finite := (IsNoetherian.noetherian I).finite_generators
refine ⟨hs.toFinset, by rwa [hs.coe_toFinset, span, I.span_generators], ?_⟩
rw [← Set.ncard_eq_toFinset_card (hs := hs), (IsNoetherian.noetherian I).generators_ncard]
refine le_antisymm ?_ ?_
· rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr
exact Cardinal.nat_le_ofENat.mp hr
· convert_to p.height ≤ I.spanRank.toENat
· symm
simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)
· exact I.height_le_spanRank_toENat_of_mem_minimal_primes _ hI
