House of an algebraic number

This file defines the house of an algebraic number α, which is the largest of the modulus of its conjugates.

References

• [D. Marcus, Number Fields][marcus1977number]
• [Hua, L.-K., Introduction to number theory][hua1982house]

Tags

number field, algebraic number, house

noncomputable def NumberField.house {K : Type u_1} [Field K] [NumberField K] (α : K) : ℝ

The house of an algebraic number as the norm of its image by the canonical embedding.

Equations

• NumberField.house α = ‖(NumberField.canonicalEmbedding K) α‖

theorem NumberField.house_eq_sup' {K : Type u_1} [Field K] [NumberField K] (α : K) : house α = ↑(Finset.univ.sup' ⋯ fun (φ : K →+* ℂ) => ‖φ α‖₊)

The house is the largest of the modulus of the conjugates of an algebraic number.

theorem NumberField.house_sum_le_sum_house {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} (s : Finset ι) (α : ι → K) : house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, house (α i)

theorem NumberField.house_nonneg {K : Type u_1} [Field K] [NumberField K] (α : K) : 0 ≤ house α

theorem NumberField.house_mul_le {K : Type u_1} [Field K] [NumberField K] (α β : K) : house (α * β) ≤ house α * house β

theorem NumberField.house_prod_le {K : Type u_1} [Field K] [NumberField K] (s : Finset K) : house (∏ x ∈ s, x) ≤ ∏ x ∈ s, house x

theorem NumberField.house_add_le {K : Type u_1} [Field K] [NumberField K] (α β : K) : house (α + β) ≤ house α + house β

theorem NumberField.house_pow_le {K : Type u_1} [Field K] [NumberField K] (α : K) (i : ℕ) : house (α ^ i) ≤ house α ^ i

theorem NumberField.house_nat_mul {K : Type u_1} [Field K] [NumberField K] (α : K) (c : ℕ) : house (↑c * α) = ↑c * house α

@[simp]

theorem NumberField.house_intCast {K : Type u_1} [Field K] [NumberField K] (x : ℤ) : house ↑x = ↑|x|

theorem NumberField.exists_conjugate_one_le_norm {K : Type u_1} [Field K] [NumberField K] {α : RingOfIntegers K} (hα0 : α ≠ 0) : ∃ (σ : K →+* ℂ), 1 ≤ ‖σ ↑α‖

Let α be a non-zero algebraic integer. Then α has a conjugate σ α with ‖σ α‖ ≥ 1.

theorem NumberField.norm_embedding_le_house {K : Type u_1} [Field K] [NumberField K] (α : K) (σ : K →+* ℂ) : ‖σ α‖ ≤ house α

theorem NumberField.one_le_house_of_isIntegral {K : Type u_1} [Field K] [NumberField K] {α : K} (hα : IsIntegral ℤ α) (hα0 : α ≠ 0) : 1 ≤ house α

theorem NumberField.norm_norm_le_norm_mul_house_pow {K : Type u_1} [Field K] [NumberField K] (α : K) (σ : K →+* ℂ) : ‖(Algebra.norm ℚ) α‖ ≤ ‖σ α‖ * house α ^ (Module.finrank ℚ K - 1)

theorem NumberField.house.basis_repr_norm_le_const_mul_house (K : Type u_1) [Field K] [NumberField K] [DecidableEq (K →+* ℂ)] (α : RingOfIntegers K) (i : K →+* ℂ) : ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ NumberField.house.c✝ K * house ((algebraMap (RingOfIntegers K) K) α)

theorem NumberField.house.exists_ne_zero_int_vec_house_le (K : Type u_1) [Field K] [NumberField K] {α : Type u_2} {β : Type u_3} (a : Matrix α β (RingOfIntegers K)) (ha : a ≠ 0) {p q : ℕ} (h0p : 0 < p) (hpq : p < q) [Fintype β] (cardβ : Fintype.card β = q) {A : ℝ} (habs : ∀ (k : α) (l : β), house ((algebraMap (RingOfIntegers K) K) (a k l)) ≤ A) [DecidableEq (K →+* ℂ)] [Fintype α] (cardα : Fintype.card α = p) : ∃ (ξ : β → RingOfIntegers K), ξ ≠ 0 ∧ a.mulVec ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ NumberField.house.c₁✝ K * (NumberField.house.c₁✝¹ K * ↑q * A) ^ (↑p / (↑q - ↑p))

There exists a "small" non-zero algebraic integral solution of an non-trivial underdetermined system of linear equations with algebraic integer coefficients.