English
Multiplicativity of the principal-equivalence: the image of a product equals the product of images.
Русский
Умножение сохраняется: образ произведения равен произведению образов.
LaTeX
$$$\big(associatesNonZeroDivisorsEquivIsPrincipal\ R (x)\big) \; * \; \big(associatesNonZeroDivisorsEquivIsPrincipal\ R (y)\big) = (associatesNonZeroDivisorsEquivIsPrincipal\ R (x * y))$$$
Lean4
/-- **Krull's principal ideal theorem** (also known as **Krullscher Hauptidealsatz**) :
In a commutative Noetherian ring `R`, any prime ideal that is minimal over a principal ideal
has height at most 1. -/
theorem height_le_one_of_isPrincipal_of_mem_minimalPrimes (I : Ideal R) [I.IsPrincipal] (p : Ideal R)
(hp : p ∈ I.minimalPrimes) : p.height ≤ 1 := by
have := hp.1.1
let f := algebraMap R (Localization.AtPrime p)
have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
· rwa [← IsLocalization.height_comap p.primeCompl, Localization.AtPrime.comap_maximalIdeal] at this
·
rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I, Set.mem_preimage,
Localization.AtPrime.comap_maximalIdeal]
