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]
• [Keng, H. L, Introduction to number theory][keng1982house]

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) : NumberField.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) : NumberField.house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, NumberField.house (α i)

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

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

@[simp]

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

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

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