English
For a nonzero element k = r/s in the fraction field K of a Dedekind domain R, the principal fractional ideal (k) factors as the product over height-one primes v of v^{val_v(r) − val_v(s)}.
Русский
Для ненулевого элемента k = r/s из поля K, где R — область Дедекадина, главный дробный идеал (k) факторизуется как произведение по всем простым идеалам высоты 1: v^{val_v(r) − val_v(s)}.
LaTeX
$$$$ (k) \;=\; \\prod_{v \\in \\mathrm{HeightOneSpectrum}(R)} v^{\\mathrm{val}_v(r) - \\mathrm{val}_v(s)}. $$$$
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_fraction {n : R} (hn : n ≠ 0) (d : ↥R⁰) :
∏ᶠ v : HeightOneSpectrum R,
(v.asIdeal : FractionalIdeal R⁰ K) ^
((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { n } : Ideal R)).factors -
(Associates.mk v.asIdeal).count (Associates.mk ((Ideal.span {(↑d : R)}) : Ideal R)).factors :
ℤ) =
spanSingleton R⁰ (mk' K n d) :=
by
have hd_ne_zero : (algebraMap R K) (d : R) ≠ 0 :=
map_ne_zero_of_mem_nonZeroDivisors _ (IsFractionRing.injective R K) d.property
have h0 : spanSingleton R⁰ (mk' K n d) ≠ 0 :=
by
rw [spanSingleton_ne_zero_iff, IsFractionRing.mk'_eq_div, ne_eq, div_eq_zero_iff, not_or]
exact ⟨(map_ne_zero_iff (algebraMap R K) (IsFractionRing.injective R K)).mpr hn, hd_ne_zero⟩
have hI : spanSingleton R⁰ (mk' K n d) = spanSingleton R⁰ ((algebraMap R K) d)⁻¹ * ↑(Ideal.span { n } : Ideal R) :=
by
rw [coeIdeal_span_singleton, spanSingleton_mul_spanSingleton]
apply congr_arg
rw [IsFractionRing.mk'_eq_div, div_eq_mul_inv, mul_comm]
exact finprod_heightOneSpectrum_factorization h0 hI
