Roots of a polynomial in an intermediate field

For an intermediate field L of E / K and a polynomial p over K, the roots of p in L, with multiplicities, are the roots of p in E that lie in L. This is Mathlib's Polynomial.filter_roots_map_range_eq_map_roots for the inclusion L → E, whose range is L. It lets root counts in different subfields of one ambient field be compared inside that field.

A monic polynomial of degree n over K is its coefficient vector a : Fin n → K, through TauCeti.Polynomial.monicOfCoeff. The root count L.rootCount a is the number of roots of that polynomial lying in L, counted with multiplicity. When that polynomial is irreducible of degree n and [L : K] = n, a root x in E lies in L exactly when K⟮x⟯ = L, so the roots in L are the roots generating L.

Main definitions

• IntermediateField.rootCount L a: the number of roots, with multiplicity, of the monic polynomial with coefficient vector a that lie in L.

Main results

• IntermediateField.filter_aroots_eq_map_aroots: the roots in E that lie in L are the roots in L, with multiplicities.
• IntermediateField.rootCount_eq_card_filter_adjoin_eq: for an irreducible monicOfCoeff a and [L : K] = n, the roots in L are the roots x in E with K⟮x⟯ = L.

theorem IntermediateField.filter_aroots_eq_map_aroots {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (L : IntermediateField K E) (p : Polynomial K) [DecidablePred fun (x : E) => x ∈ L] : Multiset.filter (fun (x : E) => x ∈ L) (p.aroots E) = Multiset.map Subtype.val (p.aroots ↥L)

The roots in E of a polynomial over K that lie in an intermediate field L are its roots in L, with the same multiplicities.

noncomputable def IntermediateField.rootCount {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (L : IntermediateField K E) {n : ℕ} (a : Fin n → K) : ℕ

The root count of a coefficient vector a : Fin n → K in a subextension L: the number of roots of the monic polynomial monicOfCoeff a lying in L, counted with multiplicity.

theorem IntermediateField.rootCount_def {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] (L : IntermediateField K E) {n : ℕ} (a : Fin n → K) : L.rootCount a = ((TauCeti.Polynomial.monicOfCoeff a).aroots ↥L).card

The defining equation of IntermediateField.rootCount.

theorem IntermediateField.rootCount_eq_card_filter_adjoin_eq {K : Type u_1} {E : Type u_2} [Field K] [Field E] [Algebra K E] {n : ℕ} {a : Fin n → K} (ha : Irreducible (TauCeti.Polynomial.monicOfCoeff a)) {L : IntermediateField K E} (hL : Module.finrank K ↥L = n) : L.rootCount a = (Multiset.filter (fun (x : E) => K⟮x⟯ = L) ((TauCeti.Polynomial.monicOfCoeff a).aroots E)).card

The roots in a degree-n subextension are its generators. If the monic polynomial monicOfCoeff a with coefficient vector a : Fin n → K is irreducible, then for an intermediate field L of E / K with [L : K] = n the roots of monicOfCoeff a in L correspond, with multiplicities, to the roots x in E with K⟮x⟯ = L.