English
Let R be a Dedekind domain with fraction field K and let I be a nonzero fractional ideal of R. If a is an element of R and J is an ideal of R with I = a^{-1} J, then I equals the product over all height-one primes v of R of v raised to the integer exponent val_v(J) − val_v(a).
Русский
Пусть R — область Дедекадина, K — её поле дробей, I — ненулевой дробный идеал R. Если a ∈ R и J — идеал R так, что I = a^{-1}J, тогда I равен произведению по всем простым идеалам v высоты 1: v^(val_v(J) − val_v(a)).
LaTeX
$$$$I \;=\; \\prod_{v \\in \\mathrm{HeightOneSpectrum}(R)} v^{\\mathrm{val}_v(J) - \\mathrm{val}_v(a)}.$$$$
Lean4
/-- If `I` is a nonzero fractional ideal, `a ∈ R`, and `J` is an ideal of `R` such that
`I = a⁻¹J`, then `I` is equal to the product `∏_v v^(val_v(J) - val_v(a))`. -/
theorem finprod_heightOneSpectrum_factorization {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
(haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
∏ᶠ v : HeightOneSpectrum R,
(v.asIdeal : FractionalIdeal R⁰ K) ^
((Associates.mk v.asIdeal).count (Associates.mk J).factors -
(Associates.mk v.asIdeal).count (Associates.mk (Ideal.span { a })).factors :
ℤ) =
I :=
by
have hJ_ne_zero : J ≠ 0 := ideal_factor_ne_zero hI haJ
have hJ := Ideal.finprod_heightOneSpectrum_factorization_coe K hJ_ne_zero
have ha_ne_zero : Ideal.span { a } ≠ 0 := constant_factor_ne_zero hI haJ
have ha := Ideal.finprod_heightOneSpectrum_factorization_coe K ha_ne_zero
rw [haJ, ← div_spanSingleton, div_eq_mul_inv, ← coeIdeal_span_singleton, ← hJ, ← ha, ← finprod_inv_distrib]
simp_rw [← zpow_neg]
rw [← finprod_mul_distrib (Ideal.finite_mulSupport_coe hJ_ne_zero) (Ideal.finite_mulSupport_inv ha_ne_zero)]
apply finprod_congr
intro v
rw [← zpow_add₀ ((@coeIdeal_ne_zero R _ K _ _ _ _).mpr v.ne_bot), sub_eq_add_neg]
