English
There exists a unit associated to the place w1 whose log-embedding configuration yields negativity at others; equivalently there exists u with log-embedding properties as in exists_unit.
Русский
Существует единица, связанная с местом w1, чья конфигурация лог-отображений даёт отрицательность на остальных местах.
LaTeX
$$$\exists u \in (\mathcal{O}_K)^×,\; \forall w \neq w_1:\; \log w(u) < 0$$$
Lean4
/-- Construct a unit associated to the place `w₁`. The family, for `w₁ ≠ w₀`, formed by the
image by the `logEmbedding` of these units is `ℝ`-linearly independent, see
`unitLattice_span_eq_top`. -/
theorem exists_unit (w₁ : InfinitePlace K) : ∃ u : (𝓞 K)ˣ, ∀ w : InfinitePlace K, w ≠ w₁ → Real.log (w u) < 0 :=
by
obtain ⟨B, hB⟩ : ∃ B : ℕ, minkowskiBound K 1 < (convexBodyLTFactor K) * B :=
by
conv => congr; ext; rw [mul_comm]
exact
ENNReal.exists_nat_mul_gt (ENNReal.coe_ne_zero.mpr (convexBodyLTFactor_ne_zero K))
(ne_of_lt (minkowskiBound_lt_top K 1))
rsuffices ⟨n, m, hnm, h⟩ :
∃ n m, n < m ∧ (Ideal.span ({(seq K w₁ hB n : 𝓞 K)}) = Ideal.span ({(seq K w₁ hB m : 𝓞 K)}))
· have hu := Ideal.span_singleton_eq_span_singleton.mp h
refine ⟨hu.choose, fun w hw ↦ Real.log_neg (pos_at_place hu.choose w) ?_⟩
calc
_ = w (algebraMap (𝓞 K) K (seq K w₁ hB m) * (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹) := by
rw [← congr_arg (algebraMap (𝓞 K) K) hu.choose_spec, mul_comm, map_mul (algebraMap _ _), ← mul_assoc,
inv_mul_cancel₀ (seq_ne_zero K w₁ hB n), one_mul]
_ = w (algebraMap (𝓞 K) K (seq K w₁ hB m)) * w (algebraMap (𝓞 K) K (seq K w₁ hB n))⁻¹ := (map_mul _ _ _)
_ < 1 := by
rw [map_inv₀, mul_inv_lt_iff₀' (pos_iff.mpr (seq_ne_zero K w₁ hB n)), mul_one]
exact seq_decreasing K w₁ hB hnm w hw
refine
Set.Finite.exists_lt_map_eq_of_forall_mem (t := {I : Ideal (𝓞 K) | Ideal.absNorm I ≤ B}) (fun n ↦ ?_)
(Ideal.finite_setOf_absNorm_le B)
rw [Set.mem_setOf_eq, Ideal.absNorm_span_singleton]
exact seq_norm_le K w₁ hB n
