English
In a local ring that is Dedekind and finite over R, primes lying over a maximal ideal p are exactly the maximal ideal of A.
Русский
В локальном кольце, являющемся Дедекиндовым и конечно над R, лежащие над максимальным идеалом p — это ровно максимальный идеал A.
LaTeX
$$Ideal.primesOver p A = {IsLocalRing.maximalIdeal A}$$
Lean4
theorem primesOver_eq [IsLocalRing A] [IsDedekindDomain A] [Algebra R A] [FaithfulSMul R A] [Module.Finite R A]
{p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) : Ideal.primesOver p A = {IsLocalRing.maximalIdeal A} :=
by
refine Set.eq_singleton_iff_nonempty_unique_mem.mpr ⟨?_, fun P hP ↦ ?_⟩
· obtain ⟨w', hmax, hover⟩ := Ideal.exists_ideal_liesOver_maximal_of_isIntegral p A
exact ⟨w', hmax.isPrime, hover⟩
· exact IsLocalRing.eq_maximalIdeal <| hP.1.isMaximal (Ideal.ne_bot_of_mem_primesOver hp0 hP)
