English
For every a in the v-adic completion K v, there exists b with b a ∈ v.adicCompletionIntegers K v and b is a non-zero-divisor in R.
Русский
Для каждого a в v.adicCompletion K v существует b, такое что ba ∈ v.adicCompletionIntegers K v и b является не нулевым делителем в R.
LaTeX
$$∃ b ∈ R⁰, a ∗ b ∈ v.adicCompletionIntegers K$$
Lean4
theorem mul_nonZeroDivisor_mem_adicCompletionIntegers (v : HeightOneSpectrum R) (a : v.adicCompletion K) :
∃ b ∈ R⁰, a * b ∈ v.adicCompletionIntegers K :=
by
by_cases ha : a ∈ v.adicCompletionIntegers K
· use 1
simp [ha]
· rw [notMem_adicCompletionIntegers] at ha
obtain ⟨ϖ, hϖ⟩ := intValuation_exists_uniformizer v
have : Valued.v (algebraMap R (v.adicCompletion K) ϖ) = (exp (1 : ℤ))⁻¹ := by
simp [valuedAdicCompletion_eq_valuation, valuation_of_algebraMap, hϖ, exp]
have hϖ0 : ϖ ≠ 0 := by rintro rfl; simp at hϖ
refine
⟨ϖ ^ (log (Valued.v a)).natAbs, pow_mem (mem_nonZeroDivisors_of_ne_zero hϖ0) _, ?_⟩
-- now manually translate the goal (an inequality in ℤᵐ⁰) to an inequality of "log" of ℤ
simp only [map_pow, mem_adicCompletionIntegers, map_mul, this, inv_pow, ← exp_nsmul, nsmul_one, Int.natCast_natAbs]
exact mul_inv_le_one_of_le₀ (le_exp_log.trans (by simp [le_abs_self])) (zero_le _)
