English
For a nonzero integer x in the ring of integers, the set of finite places w for which w x ≠ 0 is finite.
Русский
Для не нулевого целого числа x в кольце целых множество конечных мест w, для которых w x ≠ 0, конечно.
LaTeX
$$$\\{w : FinitePlace(K) \\mid w x \\ne 0\\}$ is finite for x \\ne 0$$$
Lean4
theorem mulSupport_finite_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) :
(Function.mulSupport fun w : FinitePlace K ↦ w x).Finite :=
by
have (w : FinitePlace K) : w x ≠ 1 ↔ w x < 1 :=
ne_iff_lt_iff_le.mpr <| norm_embedding_eq w x ▸ norm_le_one w.maximalIdeal x
simp_rw [Function.mulSupport, this, ← norm_embedding_eq, norm_lt_one_iff_mem, ← Ideal.dvd_span_singleton]
have h : {v : HeightOneSpectrum (𝓞 K) | v.asIdeal ∣ span { x }}.Finite :=
by
apply Ideal.finite_factors
simp only [Submodule.zero_eq_bot, ne_eq, span_singleton_eq_bot, h_x_nezero, not_false_eq_true]
have h_inj : Set.InjOn FinitePlace.maximalIdeal {w | w.maximalIdeal.asIdeal ∣ span { x }} :=
Function.Injective.injOn maximalIdeal_injective
refine (h.subset ?_).of_finite_image h_inj
simp only [dvd_span_singleton, Set.image_subset_iff, Set.preimage_setOf_eq, subset_refl]
