English
In a Dedekind domain, any nonzero fractional ideal I in R⁰K decomposes as a finite product I = ∏_{v} v^{count(K,v,I)} over height-one spectrum v of R.
Русский
В дробном идеале в Дедекдиновском домене любой ненулевой дробный идеал I распадается на конечный произведение I = ∏_{v} v^{count(K,v,I)} по спектру высоты единицы v.
LaTeX
$$$I \;=\; \\prod_{v \\in \\mathrm{HeightOneSpectrum}(R)} v^{\\operatorname{count}(K,v,I)}.$$$
Lean4
/-- If `I` is a nonzero fractional ideal, then `I` is equal to the product `∏_v v^(count K v I)`. -/
theorem finprod_heightOneSpectrum_factorization' {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) :
∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^ (count K v I) = I :=
by
have h := (Classical.choose_spec (Classical.choose_spec (exists_eq_spanSingleton_mul I))).2
conv_rhs => rw [← finprod_heightOneSpectrum_factorization hI h]
apply finprod_congr
intro w
apply congr_arg
rw [count_ne_zero K w hI]
