Candidate minimal polynomials for units in rank one

Let K be a number field of unit rank one and degree n. A unit v generating K over ℚ whose value at a real infinite place lies between 1 and B has all its other conjugates of absolute value at most 1, so its minimal polynomial over ℤ is a monic polynomial of degree n with constant coefficient ±1 whose coefficient of X ^ (n - k) is at most C(n-1, k-1) B + C(n-1, k) in absolute value. unitCandidates K B is the finite set of all such polynomials; the minimal polynomial of every generating unit in the interval belongs to it, and at prime degree every unit in the interval generates K.

In degree 2 the candidates are X² + mX ± 1 with |m| ≤ B + 1; in degree 3 they are X³ + aX² + bX ± 1 with |a| ≤ B + 2 and |b| ≤ 2B + 1. The enumeration is intentionally an overapproximation: a later root test and field test eliminate candidates that cannot be units in the given field.

Main results

• TauCeti.NumberField.Units.unitCandidates: the finite set of candidate minimal polynomials, characterised by TauCeti.NumberField.Units.mem_unitCandidates_iff.
• TauCeti.NumberField.Units.minpoly_mem_unitCandidates: completeness of the candidate set at unit rank one and prime degree.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §5.7.

noncomputable def TauCeti.NumberField.Units.unitCandidates (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : Finset (Polynomial ℤ)

The finite list of monic integer polynomials of degree n = [K : ℚ] with constant coefficient ±1 whose coefficient of X ^ (n - k), for 0 < k < n, is at most C(n-1, k-1) B + C(n-1, k) in absolute value.

@[simp]

theorem TauCeti.NumberField.Units.mem_unitCandidates_iff {K : Type u_1} [Field K] [NumberField K] (f : Polynomial ℤ) (B : ℝ) : f ∈ unitCandidates K B ↔ f.Monic ∧ f.natDegree = Module.finrank ℚ K ∧ (f.coeff 0 = 1 ∨ f.coeff 0 = -1) ∧ ∀ (k : ℕ), 0 < k → k < Module.finrank ℚ K → |↑(f.coeff (Module.finrank ℚ K - k))| ≤ ↑((Module.finrank ℚ K - 1).choose (k - 1)) * B + ↑((Module.finrank ℚ K - 1).choose k)

Membership in the candidate list is exactly monicity, field degree, constant coefficient ±1, and the binomial coefficient bounds.

theorem TauCeti.NumberField.Units.minpoly_mem_unitCandidates_of_adjoin_eq_top {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) {w : NumberField.InfinitePlace K} (hw : w.IsReal) (v : (NumberField.RingOfIntegers K)ˣ) (hgen : ℚ[↑↑v] = ⊤) {B : ℝ} (hlo : 1 < (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v)) (hhi : (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) ≤ B) : minpoly ℤ ↑v ∈ unitCandidates K B

Every unit generating K over ℚ whose value at a real infinite place lies in (1, B] has its minimal polynomial in unitCandidates K B when the unit rank is one.

theorem TauCeti.NumberField.Units.minpoly_mem_unitCandidates {K : Type u_1} [Field K] [NumberField K] (hr : NumberField.Units.rank K = 1) (hp : Nat.Prime (Module.finrank ℚ K)) {w : NumberField.InfinitePlace K} (hw : w.IsReal) (v : (NumberField.RingOfIntegers K)ˣ) {B : ℝ} (hlo : 1 < (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v)) (hhi : (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) ≤ B) : minpoly ℤ ↑v ∈ unitCandidates K B

Every unit whose value at a real infinite place lies in (1, B] has its minimal polynomial in unitCandidates K B when the unit rank is one and the field degree is prime.