English
There is a canonical IsScalarTower between R, K, and the finite adele ring, i.e., R → K → FiniteAdeleRing is compatible with scalars.
Русский
Существует корректная проблема-иерархия IsScalarTower между R, K и FiniteAdeleRing, обеспечивающая совместимость умножения скаляров.
LaTeX
$$instance : IsScalarTower R K (IsDedekindDomain.FiniteAdeleRing R K)$$
Lean4
/-- The support of an element of the field of fractions of a Dedekind domain
is finite.
-/
theorem finite (k : K) : (Support R k).Finite := by
-- We write k=n/d.
obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k
have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
suffices {v : HeightOneSpectrum R | v.valuation K (algebraMap R K d) < 1}.Finite
by
apply Set.Finite.subset this
intro v hv
apply_fun v.valuation K at hk
simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
rw [Set.mem_setOf_eq, valuation_of_algebraMap]
have := intValuation_le_one v n
contrapose! this
rw [← hk, mul_comm]
exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <| mul_le_mul_of_nonneg_right this (by simp)
simp_rw [valuation_lt_one_iff_dvd]
apply Ideal.finite_factors
simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]
