English
For any nonzero x in the ring of integers 𝓞K of a number field K, the finite-place product of w x equals the inverse of the absolute norm |N_{ℤ} x|.
Русский
Для любого ненулевого x в кольце целых чисел 𝓞K конечного числа полей, произведение по всем конечноположительным местам w x равно обратному модулю целой нормы |N_{ℤ}(x)|.
LaTeX
$$$x \neq 0 \Rightarrow \prod_{w \text{ finite place}} w x = |\operatorname{norm}_{\mathbb{Z}}(x)|^{-1}$$$
Lean4
/-- For any non-zero `x` in `𝓞 K`, the product of `w x`, where `w` runs over `FinitePlace K`, is
equal to the inverse of the absolute value of `Algebra.norm ℤ x`. -/
theorem prod_eq_inv_abs_norm_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) : ∏ᶠ w : FinitePlace K, w x = (|norm ℤ x| : ℝ)⁻¹ :=
by
simp only [← finprod_comp_equiv equivHeightOneSpectrum.symm, equivHeightOneSpectrum_symm_apply]
refine (inv_eq_of_mul_eq_one_left ?_).symm
norm_cast
have h_span_nezero : span { x } ≠ 0 := by simp [h_x_nezero]
rw [Int.abs_eq_natAbs, ← absNorm_span_singleton, ← finprod_heightOneSpectrum_factorization h_span_nezero,
Int.cast_natCast]
let t₀ := {v : HeightOneSpectrum (𝓞 K) | x ∈ v.asIdeal}
have h_fin₀ : t₀.Finite := by simp only [← dvd_span_singleton, finite_factors h_span_nezero, t₀]
let t₁ := (fun v : HeightOneSpectrum (𝓞 K) ↦ ‖embedding v (x : K)‖).mulSupport
let t₂ := (fun v : HeightOneSpectrum (𝓞 K) ↦ (absNorm (v.maxPowDividing (span { x })) : ℝ)).mulSupport
have h_fin₁ : t₁.Finite := h_fin₀.subset <| by simp [norm_eq_one_iff_notMem, t₁, t₀]
have h_fin₂ : t₂.Finite := by
refine h_fin₀.subset ?_
simp only [mulSupport_subset_iff, Set.mem_setOf_eq, t₂, t₀, maxPowDividing, ← dvd_span_singleton]
intro v hv
simp only [map_pow, Nat.cast_pow, ← pow_zero (absNorm v.asIdeal : ℝ)] at hv
classical
refine (Associates.count_ne_zero_iff_dvd h_span_nezero (irreducible v)).1 <| fun h ↦ hv ?_
congr
have h_prod :
(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span { x })) : ℝ) =
∏ᶠ (v : HeightOneSpectrum (𝓞 K)), (absNorm (v.maxPowDividing (span { x })) : ℝ) :=
((Nat.castRingHom ℝ).toMonoidHom.comp absNorm.toMonoidHom).map_finprod_of_preimage_one (by simp) _
rw [h_prod, ← finprod_mul_distrib h_fin₁ h_fin₂]
exact finprod_eq_one_of_forall_eq_one fun v ↦ v.embedding_mul_absNorm h_x_nezero
