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]

Tagshouse

number field, algebraic number, house

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 β

@[simp]

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

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) α)

@[deprecated NumberField.house.basis_repr_norm_le_const_mul_house (since := "2025-02-17")]

theorem NumberField.house.basis_repr_abs_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) α)

Alias of NumberField.house.basis_repr_norm_le_const_mul_house.

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.