English
For an algebraic integer α ∈ 𝓞K and a fixed embedding i, the ℂ-norm of the coordinate of α in a basis-representation is bounded by a constant c(K) times house(α).
Русский
Для целого алгебраического числа α ∈ 𝓞K и фиксированного вложения i норм-a координаты α в базисном представлении не превышает константы c(K) умноженной на house(α).
LaTeX
$$$\\|\\big( ((\\text{integralBasis } K).reindex (\\text{equivReindex } K).symm).repr α i : \\mathbb{C} \\big)\\| \\le (c(K)) \\cdot \\operatorname{house}(\\alpha).$$$
Lean4
theorem basis_repr_norm_le_const_mul_house (α : 𝓞 K) (i : K →+* ℂ) :
‖(((integralBasis K).reindex (equivReindex K).symm).repr α i : ℂ)‖ ≤ (c K) * house (algebraMap (𝓞 K) K α) :=
by
let σ := canonicalEmbedding K
calc
_ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ :=
by
rw [← inverse_basisMatrix_mulVec_eq_repr]
exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
_ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ :=
by
gcongr
exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
_ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖ * house (algebraMap (𝓞 K) K α) :=
by
gcongr with j
exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
_ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
simp [Embeddings.card, mul_assoc]
