English
A variant for the ring of integers: under a Minkowski-type bound, there exists a primitive element a ∈ 𝓞(K) with a prime-like generation property, bounded at infinite places by max(B,1).
Русский
Вариант для кольца целых: при условии Минковского существует примитивный элемент a ∈ 𝓞(K) с свойством порождения, ограниченным на бесконечных местах максимальным между B и 1.
LaTeX
$$$\exists a \in \mathcal{O}_K,\ \mathbb{Q}(a) = K,\forall w:\ InfinitePlace\ K,\ w(a) < \max\{B,1\}$$$
Lean4
theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀ : IsComplex w₀) {B : ℝ≥0}
(hB : minkowskiBound K ↑1 < convexBodyLT'Factor K * B) :
∃ a : 𝓞 K, ℚ⟮(a : K)⟯ = ⊤ ∧ ∀ w : InfinitePlace K, w a < Real.sqrt (1 + B ^ 2) := by
classical
have : minkowskiBound K ↑1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩) :=
by
rw [convexBodyLT'_volume, ← Finset.prod_erase_mul _ _ (Finset.mem_univ w₀)]
simp_rw [ite_pow, one_pow]
rw [Finset.prod_ite_eq']
simp_rw [Finset.notMem_erase, ite_false, mult, not_isReal_iff_isComplex.mpr hw₀, ite_true, ite_false, one_mul,
NNReal.sq_sqrt]
exact hB
obtain ⟨a, h_nz, h_le, h_le₀⟩ := exists_ne_zero_mem_ringOfIntegers_lt' K ⟨w₀, hw₀⟩ this
refine ⟨a, ?_, fun w ↦ ?_⟩
·
exact
is_primitive_element_of_infinitePlace_lt h_nz (fun w h_ne ↦ by convert if_neg h_ne ▸ h_le w h_ne) (Or.inr h_le₀.1)
· by_cases h_eq : w = w₀
· rw [if_pos rfl] at h_le₀
dsimp only at h_le₀
rw [h_eq, ← norm_embedding_eq, Real.lt_sqrt (norm_nonneg _), ← Complex.re_add_im (embedding w₀ _),
Complex.norm_add_mul_I, Real.sq_sqrt (by positivity)]
refine add_lt_add ?_ ?_
· rw [← sq_abs, sq_lt_one_iff₀ (abs_nonneg _)]
exact h_le₀.1
· rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
exact h_le₀.2
· refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_
rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
norm_num
