English
Let S be a Dedekind domain and I an ideal. Then nat absNorm(under ℤ I) divides absNorm I.
Русский
Пусть S — Д Dedekind домен. Тогда nat(absNorm(under ℤ I)) делит absNorm I.
LaTeX
$$$\operatorname{absNorm}(\operatorname{under} \mathbb{Z} I) \mid \operatorname{absNorm} I$$$
Lean4
theorem absNorm_under_dvd_absNorm {S : Type*} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S] (I : Ideal S) :
absNorm (under ℤ I) ∣ absNorm I := by
cases finite_or_infinite (S ⧸ I)
· have : Fintype (S ⧸ I) := Fintype.ofFinite (S ⧸ I)
have h_main {d : ℕ} : (d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0 :=
by
simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]
exact ⟨fun h _ ↦ by simp [h], fun h ↦ by simpa using h 1⟩
rw [Ideal.absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_fintype_card]
simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]
exact AddGroup.exponent_dvd_card (G := S ⧸ I)
· rw [absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_zero_of_infinite]
exact Nat.dvd_zero _
