English
Let S be a Dedekind domain which is a finitely generated free abelian group, and let I be an ideal of S. If the absolute norm absNorm(I) is a prime number, then the principal Z-ideal generated by absNorm(I) equals the contraction of I along the map Z → S; i.e., span{absNorm(I)} = I comap (algebraMap Z S).
Русский
Пусть S — Дедекендов домен, являющийся свободной Z-модулей размерности конечного типа, и пусть I — ideal S. Если absNorm(I) — простое число p, то канонический Z-образ (каноническая ℤ-идеал) абсNorm(I) равен компакционной норме I по отображению Z → S; другими словами, pℤ = I comap (algebraMap ℤ S).
LaTeX
$$$ \operatorname{span}_{\mathbb{Z}}\{ \operatorname{absNorm}(I) \} = I \comap \bigl( \operatorname{algebraMap} \mathbb{Z} S \bigr). $$$
Lean4
theorem span_singleton_absNorm {I : Ideal S} (hI : (Ideal.absNorm I).Prime) :
Ideal.span (singleton (Ideal.absNorm I : ℤ)) = I.comap (algebraMap ℤ S) :=
by
have : Ideal.IsPrime (Ideal.span (singleton (Ideal.absNorm I : ℤ))) := by
rwa [Ideal.span_singleton_prime (Int.ofNat_ne_zero.mpr hI.ne_zero), ← Nat.prime_iff_prime_int]
apply (this.isMaximal _).eq_of_le
· exact ((isPrime_of_irreducible_absNorm ((Nat.irreducible_iff_nat_prime _).mpr hI)).comap (algebraMap ℤ S)).ne_top
· rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]
exact absNorm_mem I
· rw [Ne, span_singleton_eq_bot]
exact Int.ofNat_ne_zero.mpr hI.ne_zero
