English
If I is a nonzero fractional ideal and k ∈ K with hk, there exist representations expressing I as (k) and the product formula holds: ∏_v v^{val_v(r) − val_v(s)} = (k).
Русский
Если I — ненулевой дробный идеал и k ∈ K, существуют представления, при которых I = (k) и выполняется формула разложения: ∏_v v^{val_v(r) − val_v(s)} = (k).
LaTeX
$$$$ I = (k) \\quad\\Rightarrow\\quad \\prod_{v \\in \\mathrm{HeightOneSpectrum}(R)} v^{\\mathrm{val}_v(r) - \\mathrm{val}_v(s)} = (k). $$$$
Lean4
/-- For a nonzero `k = r/s ∈ K`, the fractional ideal `(k)` is equal to the product
`∏_v v^(val_v(r) - val_v(s))`. -/
theorem finprod_heightOneSpectrum_factorization_principal {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) (k : K)
(hk : I = spanSingleton R⁰ k) :
∏ᶠ v : HeightOneSpectrum R,
(v.asIdeal : FractionalIdeal R⁰ K) ^
((Associates.mk v.asIdeal).count
(Associates.mk (Ideal.span {choose (mk'_surjective R⁰ k)} : Ideal R)).factors -
(Associates.mk v.asIdeal).count
(Associates.mk
((Ideal.span {(↑(choose (choose_spec (mk'_surjective R⁰ k)) : ↥R⁰) : R)}) : Ideal R)).factors :
ℤ) =
I :=
by
set n : R := choose (mk'_surjective R⁰ k)
set d : ↥R⁰ := choose (choose_spec (mk'_surjective R⁰ k))
have hnd : mk' K n d = k := choose_spec (choose_spec (mk'_surjective R⁰ k))
have hn0 : n ≠ 0 := by
by_contra h
rw [← hnd, h, IsFractionRing.mk'_eq_div, map_zero, zero_div, spanSingleton_zero] at hk
exact hI hk
rw [finprod_heightOneSpectrum_factorization_principal_fraction hn0 d, hk, hnd]
