Monic irreducible polynomials of a fixed degree

The monic irreducible polynomials of a given degree over a semiring R form a set depending only on R and the degree. When R is finite that set is finite, because a monic polynomial of degree d is determined by its lower coefficients: Polynomial.monicEquivDegreeLT matches such polynomials with Polynomial.degreeLT, which Polynomial.degreeLTEquiv identifies with the finite function space Fin d → R.

Main definitions

• Polynomial.monicIrreduciblesOfDegree: the monic irreducible polynomials of degree d.

Main results

• Polynomial.mem_monicIrreduciblesOfDegree_iff: the defining membership condition.
• Polynomial.finite_monicIrreduciblesOfDegree: over a finite coefficient ring there are finitely many.
• Polynomial.ncard_monicIrreduciblesOfDegree_one: over a domain the monic irreducibles of degree one are the X - C a, as many as the elements of the coefficient ring.
• TauCeti.irreducible_map_intCast_of_natDegree_eq_three: a monic integral cubic with no integral root is irreducible over ℚ.
• TauCeti.irreducible_map_intCast_of_natDegree_eq_four: a monic integral quartic with no integral root and no monic integral quadratic factor is irreducible over ℚ.

def Polynomial.monicIrreduciblesOfDegree (R : Type u_1) [Semiring R] (d : ℕ) : Set (Polynomial R)

The monic irreducible polynomials of degree d over R.

The set depends only on R and d, which is what lets a counting argument compare it with an unrelated family without assuming a bound on either.

Equations

• Polynomial.monicIrreduciblesOfDegree R d = {g : Polynomial R | g.Monic ∧ Irreducible g ∧ g.natDegree = d}

@[simp]

theorem Polynomial.mem_monicIrreduciblesOfDegree_iff (R : Type u_1) [Semiring R] {d : ℕ} {g : Polynomial R} : g ∈ monicIrreduciblesOfDegree R d ↔ g.Monic ∧ Irreducible g ∧ g.natDegree = d

Membership in monicIrreduciblesOfDegree is the conjunction defining it.

theorem Polynomial.finite_monicIrreduciblesOfDegree (R : Type u_1) [Semiring R] [Nontrivial R] [Finite R] (d : ℕ) : (monicIrreduciblesOfDegree R d).Finite

Over a finite coefficient ring there are finitely many monic irreducibles of each degree. They sit inside the monic polynomials of that degree, which are parametrised by their lower coefficients.

theorem Polynomial.monicIrreduciblesOfDegree_one {R : Type u_1} [CommRing R] [IsDomain R] : monicIrreduciblesOfDegree R 1 = Set.range fun (a : R) => X - C a

Over a domain, the monic irreducible polynomials of degree one are exactly the X - C a.

@[simp]

theorem Polynomial.ncard_monicIrreduciblesOfDegree_one (R : Type u_1) [CommRing R] [IsDomain R] : (monicIrreduciblesOfDegree R 1).ncard = Nat.card R

Over a domain there are as many monic irreducible polynomials of degree one as elements of the coefficient ring.

theorem TauCeti.irreducible_map_intCast_of_natDegree_eq_three {g : Polynomial ℤ} (hg : g.Monic) (hdeg : g.natDegree = 3) (h : ∀ (m : ℤ), Polynomial.eval m g ≠ 0) : Irreducible (Polynomial.map (Int.castRingHom ℚ) g)

A monic integral cubic without an integral root is irreducible over ℚ: a rational root of a monic integral polynomial is integral.

theorem TauCeti.irreducible_map_intCast_of_natDegree_eq_four {g : Polynomial ℤ} (hg : g.Monic) (hdeg : g.natDegree = 4) (hroot : ∀ (m : ℤ), Polynomial.eval m g ≠ 0) (hquad : ∀ (a b : ℤ), ¬Polynomial.X ^ 2 + Polynomial.C a * Polynomial.X + Polynomial.C b ∣ g) : Irreducible (Polynomial.map (Int.castRingHom ℚ) g)

A monic integral quartic with no integral root and no monic integral quadratic factor is irreducible over ℚ. By Gauss's lemma it suffices to rule out monic factors of degree one and two over ℤ, and a monic linear factor X + C c divides g exactly when -c is a root of g.