Counting monic divisors and intermediate fields; Hilbert 90 for an involution

Monic divisors of a nonzero polynomial are determined by their multisets of roots in an algebraic closure, so there are at most 2 ^ natDegree of them. Through a primitive element, the intermediate fields of a finite separable extension inject into the monic divisors of a minimal polynomial.

Main results

• Polynomial.card_monic_dvd_le_two_pow_natDegree: a nonzero polynomial f over a field has at most 2 ^ f.natDegree monic divisors.
• IntermediateField.card_le_two_pow_finrank: a finite separable extension E / F has at most 2 ^ finrank F E intermediate fields.
• RingEquiv.hilbert90_of_involutive: Hilbert 90 for a nontrivial involution σ of a field, with an explicit construction that also works in characteristic two: if a σ(a) = 1, then a σ(b) = b for some b ≠ 0. RingEquiv.hilbert90_units_of_involutive is the unit-group form.
• RingEquiv.exists_invariant_of_involutive: for a compatible homomorphism P from the units, an element I with τ I = P a * I and a σ(a) = 1 has a τ-invariant multiple P b * I.

theorem Polynomial.card_monic_dvd_le_two_pow_natDegree {K : Type u_1} [Field K] (f : Polynomial K) (hf : f ≠ 0) : Nat.card { g : Polynomial K // g.Monic ∧ g ∣ f } ≤ 2 ^ f.natDegree

A nonzero polynomial over a field has at most 2 ^ natDegree monic divisors.

theorem IntermediateField.card_le_two_pow_finrank (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : Nat.card (IntermediateField F E) ≤ 2 ^ Module.finrank F E

The number of intermediate fields depends only on the extension degree, without a chosen normal closure or Galois-group estimate.

theorem RingEquiv.hilbert90_of_involutive {K : Type u_1} [Field K] (σ : K ≃+* K) (hσ : Function.Involutive ⇑σ) (hσne : σ ≠ refl K) {a : K} (ha : a * σ a = 1) : ∃ (b : K), b ≠ 0 ∧ a * σ b = b

A norm-one scalar for a nontrivial involution is a multiplicative coboundary. The explicit construction also works in characteristic two.

theorem RingEquiv.hilbert90_units_of_involutive {K : Type u_1} [Field K] (σ : K ≃+* K) (hσ : Function.Involutive ⇑σ) (hσne : σ ≠ refl K) (a : Kˣ) (ha : ↑a * σ ↑a = 1) : ∃ (b : Kˣ), a * (Units.map σ.toMonoidHom) b = b

Hilbert 90 for a nontrivial involution, in the unit group: a unit a with a σ(a) = 1 has the form b / σ(b) for some unit b.

theorem RingEquiv.exists_invariant_of_involutive {K : Type u_1} [Field K] {A : Type u_2} [CommGroup A] (σ : K ≃+* K) (hσ : Function.Involutive ⇑σ) (hσne : σ ≠ refl K) (τ : A →* A) (P : Kˣ →* A) (hcompat : ∀ (b : Kˣ), τ (P b) = P ((Units.map σ.toMonoidHom) b)) (I : A) (a : Kˣ) (hI : τ I = P a * I) (ha : ↑a * σ ↑a = 1) : ∃ (b : Kˣ), τ (P b * I) = P b * I

If the scalar comparison of an element with its conjugate has norm one, multiplication by a principal element produces an invariant representative. Here the principal map is a homomorphism.