Counting simple intermediate fields generated by roots of bounded integer polynomials

Mathlib's proof of Hermite's finiteness theorem NumberField.finite_of_discr_bdd reduces bounded-discriminant number fields in a fixed ambient extension to fields generated by elements of a finite root set, via NumberField.hermiteTheorem.finite_of_finite_generating_set. The effective Hermite--Minkowski count uses the corresponding cardinality step: if the admissible generators lie in a finite set T, then the image of T under x ↦ ℚ⟮x⟯ is finite and no larger than T (Set.Finite.image, Set.ncard_image_le).

This file specializes that image bound to the bounded-polynomial root set, which is itself counted in TauCeti.Algebra.Polynomial.Card.RootSetUnion.

Main results

• finite_image_adjoin_simple_biUnion_roots_natDegree_le_abs_intCoeff_le: the simple subfields generated by roots of integer polynomials of bounded degree and coefficient height form a finite set.
• ncard_image_adjoin_simple_biUnion_roots_natDegree_le_abs_intCoeff_le: their number is at most (2 * B + 1) ^ (d + 1) * d.

No formal code is vendored. The proof reuses Mathlib's IntermediateField.adjoin API and Tau Ceti's bounded-polynomial root finiteness and count.

theorem TauCeti.IntermediateField.finite_image_adjoin_simple_biUnion_roots_natDegree_le_abs_intCoeff_le (A : Type u_1) [Field A] [Algebra ℚ A] [DecidableEq A] (d B : ℕ) : ((fun (x : A) => ℚ⟮x⟯) '' ⋃ (f : Polynomial ℤ), ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B), ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset).Finite

The simple subfields of an ambient field A / ℚ generated by roots of integer polynomials of degree at most d and coefficient height at most B form a finite set.

This is the finiteness half of the root-to-field counting step used by the effective Hermite--Minkowski count.

theorem TauCeti.IntermediateField.ncard_image_adjoin_simple_biUnion_roots_natDegree_le_abs_intCoeff_le (A : Type u_1) [Field A] [Algebra ℚ A] [DecidableEq A] (d B : ℕ) : ((fun (x : A) => ℚ⟮x⟯) '' ⋃ (f : Polynomial ℤ), ⋃ (_ : f.natDegree ≤ d ∧ ∀ (i : ℕ), |f.coeff i| ≤ ↑B), ↑(Polynomial.map (algebraMap ℤ A) f).roots.toFinset).ncard ≤ (2 * B + 1) ^ (d + 1) * d

The simple subfields of an ambient field A / ℚ generated by roots of integer polynomials of degree at most d and coefficient height at most B number at most (2 * B + 1) ^ (d + 1) * d.

This is the root-to-field counting step used by the effective Hermite--Minkowski count, after TauCeti.Polynomial.ncard_biUnion_roots_natDegree_le_abs_intCoeff_le has counted the possible generators.