Evidence for quintic Galois-group certificates

A factorization of a monic integral polynomial at a prime not dividing its discriminant gives lower-bound evidence for its Galois group: the factor degrees are the full cycle type of an element of the Galois image. A root of a separable resolvent gives upper-bound evidence. This module packages those two kinds of evidence, together with the condition that a polynomial has a formal second-root representative modulo the polynomial. For a monic irreducible polynomial, this modular evidence represents a distinct second root in the field generated by one root.

The predicates contain only finite data. They do not search for a suitable prime, resolvent root, or second root. Their elimination lemmas expose the mathematical consequences used by quintic certificates, while keeping the proof of primality bundled with the factor-degree computation.

Main definitions

• TauCeti.IsGoodPrime: a prime candidate does not divide the polynomial discriminant.
• TauCeti.HasFactorDegrees: a good prime with specified factor degrees.
• TauCeti.HasSexticRoot: an integral root of a separable quintic resolvent sextic.
• TauCeti.HasSecondRootInRootField: formal modular evidence for a second root, whose root-field interpretation requires the polynomial to be monic and irreducible.

Main results

• TauCeti.HasFactorDegrees.exists_fullCycleType: factor-degree evidence produces an element of the Galois image with that full cycle type.
• TauCeti.HasFactorDegrees.irreducible_map_rat: singleton evidence proves irreducibility over ℚ.
• TauCeti.HasFactorDegrees.exists_orderOf_eq_two, TauCeti.HasFactorDegrees.exists_orderOf_eq_three, and TauCeti.HasFactorDegrees.exists_orderOf_eq_six: the factor types used by the dihedral, alternating, and symmetric certificate routes produce elements of the required orders.
• TauCeti.HasSexticRoot.isRoot_specialize_rat and TauCeti.HasSexticRoot.separable_specialize_rat: the two consequences of resolvent evidence in the rational specialization used by quintic labels.

def TauCeti.HasFactorDegrees (f : Polynomial ℤ) (p : ℕ) (t : Multiset ℕ) : Prop

A good-prime factorization item: p is prime, does not divide the discriminant of f, and the irreducible factors of f modulo p have degrees t, with multiplicity.

Equations

• TauCeti.HasFactorDegrees f p t = ∃ (hp : Nat.Prime p), TauCeti.IsGoodPrime f p ∧ f.factorDegrees p = t

@[simp]

theorem TauCeti.hasFactorDegrees_iff (f : Polynomial ℤ) (p : ℕ) (t : Multiset ℕ) : HasFactorDegrees f p t ↔ ∃ (hp : Nat.Prime p), IsGoodPrime f p ∧ f.factorDegrees p = t

The defining characterization of factor-degree evidence.

theorem TauCeti.HasFactorDegrees.mk {f : Polynomial ℤ} {p : ℕ} [hp : Fact (Nat.Prime p)] {t : Multiset ℕ} (hgood : IsGoodPrime f p) (hfac : f.factorDegrees p = t) : HasFactorDegrees f p t

Construct factor-degree evidence from a prime instance, goodness, and the factor degrees.

theorem TauCeti.HasFactorDegrees.exists_fact {f : Polynomial ℤ} {p : ℕ} {t : Multiset ℕ} (h : HasFactorDegrees f p t) : ∃ (hp : Fact (Nat.Prime p)), IsGoodPrime f p ∧ f.factorDegrees p = t

Eliminate factor-degree evidence while retaining a local primality instance.

theorem TauCeti.HasFactorDegrees.sum_eq_natDegree {f : Polynomial ℤ} {p : ℕ} {t : Multiset ℕ} (h : HasFactorDegrees f p t) (hf : f.Monic) : t.sum = f.natDegree

The factor degrees recorded by evidence for a monic polynomial sum to its degree.

theorem TauCeti.HasFactorDegrees.exists_fullCycleType {f : Polynomial ℤ} {p : ℕ} {t : Multiset ℕ} (h : HasFactorDegrees f p t) (hf : f.Monic) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, σ.fullCycleType = t

Factor-degree evidence produces an element of the Galois image whose full cycle type is the specified multiset.

theorem TauCeti.HasFactorDegrees.exists_orderOf_eq_lcm {f : Polynomial ℤ} {p : ℕ} {t : Multiset ℕ} (h : HasFactorDegrees f p t) (hf : f.Monic) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, orderOf σ = t.lcm

Factor-degree evidence exhibits an element of the Galois image whose order is the least common multiple of the specified factor degrees.

theorem TauCeti.HasFactorDegrees.exists_orderOf_eq_two {f : Polynomial ℤ} {p : ℕ} (h : HasFactorDegrees f p {1, 2, 2}) (hf : f.Monic) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, orderOf σ = 2

Factor degrees (1,2,2) exhibit an element of order two in the Galois image. This is the lower-bound evidence that distinguishes the dihedral quintic label from the cyclic one.

theorem TauCeti.HasFactorDegrees.exists_orderOf_eq_six {f : Polynomial ℤ} {p : ℕ} (h : HasFactorDegrees f p {2, 3}) (hf : f.Monic) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, orderOf σ = 6

Factor degrees (2,3) exhibit an element of order six in the Galois image. In degree five, this is the lower-bound evidence for the full symmetric label.

theorem TauCeti.HasFactorDegrees.exists_orderOf_eq_three {f : Polynomial ℤ} {p : ℕ} (h : HasFactorDegrees f p {1, 1, 3}) (hf : f.Monic) : ∃ σ ∈ (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom ℚ) f) ℂ).range, orderOf σ = 3

Factor degrees (1,1,3) exhibit an element of order three in the Galois image. In degree five, this is the lower-bound evidence for the alternating label.

theorem TauCeti.HasFactorDegrees.irreducible_map {f : Polynomial ℤ} {p n : ℕ} (h : HasFactorDegrees f p {n}) : ∃ (_hp : Fact (Nat.Prime p)), Irreducible (Polynomial.map (Int.castRingHom (ZMod p)) f) ∧ (Polynomial.map (Int.castRingHom (ZMod p)) f).natDegree = n

Singleton factor-degree evidence proves that the reduction is irreducible and records its degree.

theorem TauCeti.HasFactorDegrees.irreducible_map_rat {f : Polynomial ℤ} {p n : ℕ} (h : HasFactorDegrees f p {n}) (hf : f.Monic) : Irreducible (Polynomial.map (Int.castRingHom ℚ) f)

Any singleton factor-degree evidence for a monic polynomial proves that its image over ℚ is irreducible.

def TauCeti.HasSexticRoot (f : Polynomial ℤ) (a : ℤ) : Prop

A resolvent item: a is an integral root of the quintic resolvent sextic and the sextic has nonzero discriminant. The latter condition is precisely the separation evidence needed to read the root as an upper bound on the Galois image.

Equations

• TauCeti.HasSexticRoot f a = (Polynomial.eval a (TauCeti.resolventSextic f) = 0 ∧ (TauCeti.resolventSextic f).discr ≠ 0)

@[simp]

theorem TauCeti.hasSexticRoot_iff (f : Polynomial ℤ) (a : ℤ) : HasSexticRoot f a ↔ Polynomial.eval a (resolventSextic f) = 0 ∧ (resolventSextic f).discr ≠ 0

The defining characterization of resolvent-root evidence.

theorem TauCeti.HasSexticRoot.mk {f : Polynomial ℤ} {a : ℤ} (hroot : Polynomial.eval a (resolventSextic f) = 0) (hdisc : (resolventSextic f).discr ≠ 0) : HasSexticRoot f a

Construct resolvent-root evidence from its two defining conditions.

theorem TauCeti.HasSexticRoot.isRoot {f : Polynomial ℤ} {a : ℤ} (h : HasSexticRoot f a) : (resolventSextic f).IsRoot a

The integer carried by resolvent evidence is a root of the resolvent sextic.

theorem TauCeti.HasSexticRoot.separable_map_rat {f : Polynomial ℤ} {a : ℤ} (h : HasSexticRoot f a) : (Polynomial.map (Int.castRingHom ℚ) (resolventSextic f)).Separable

The resolvent sextic in a resolvent item becomes separable over ℚ.

theorem TauCeti.HasSexticRoot.isRoot_map {F : Type u_1} [CommRing F] {f : Polynomial ℤ} {a : ℤ} (h : HasSexticRoot f a) : (Polynomial.map (Int.castRingHom F) (resolventSextic f)).IsRoot ↑a

Resolvent evidence remains a root after mapping the sextic and its root to any commutative ring.

theorem TauCeti.HasSexticRoot.isRoot_specialize_rat {f : Polynomial ℤ} {a : ℤ} (h : HasSexticRoot f a) : (quinticF20Spec.specialize ℚ (Polynomial.map (Int.castRingHom ℚ) f)).IsRoot ↑a

Resolvent evidence gives a root of the rational specialization of the quintic F₂₀-resolvent.

theorem TauCeti.HasSexticRoot.separable_specialize_rat {f : Polynomial ℤ} {a : ℤ} (h : HasSexticRoot f a) : (quinticF20Spec.specialize ℚ (Polynomial.map (Int.castRingHom ℚ) f)).Separable

The rational specialization of the quintic F₂₀-resolvent in a resolvent item is separable.

def TauCeti.HasSecondRootInRootField (f : Polynomial ℤ) (b : Polynomial ℚ) : Prop

Formal modular evidence that b is a root representative distinct from the class of X. When f is monic and irreducible, the quotient is the field generated by one root and this evidence represents a distinct second root there.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.hasSecondRootInRootField_iff (f : Polynomial ℤ) (b : Polynomial ℚ) : HasSecondRootInRootField f b ↔ (Polynomial.map (Int.castRingHom ℚ) f).comp b %ₘ Polynomial.map (Int.castRingHom ℚ) f = 0 ∧ b %ₘ Polynomial.map (Int.castRingHom ℚ) f ≠ Polynomial.X %ₘ Polynomial.map (Int.castRingHom ℚ) f

The defining characterization of formal second-root evidence.

theorem TauCeti.HasSecondRootInRootField.mk {f : Polynomial ℤ} {b : Polynomial ℚ} (hroot : (Polynomial.map (Int.castRingHom ℚ) f).comp b %ₘ Polynomial.map (Int.castRingHom ℚ) f = 0) (hne : b %ₘ Polynomial.map (Int.castRingHom ℚ) f ≠ Polynomial.X %ₘ Polynomial.map (Int.castRingHom ℚ) f) : HasSecondRootInRootField f b

Construct formal second-root evidence from its two defining congruences.

theorem TauCeti.HasSecondRootInRootField.comp_modByMonic_eq_zero {f : Polynomial ℤ} {b : Polynomial ℚ} (h : HasSecondRootInRootField f b) : (Polynomial.map (Int.castRingHom ℚ) f).comp b %ₘ Polynomial.map (Int.castRingHom ℚ) f = 0

The polynomial represented by a second-root item vanishes after substitution, modulo f.

theorem TauCeti.HasSecondRootInRootField.modByMonic_ne_X_modByMonic {f : Polynomial ℤ} {b : Polynomial ℚ} (h : HasSecondRootInRootField f b) : b %ₘ Polynomial.map (Int.castRingHom ℚ) f ≠ Polynomial.X %ₘ Polynomial.map (Int.castRingHom ℚ) f

The polynomial represented by a second-root item is not the distinguished root X modulo f.

theorem TauCeti.HasSecondRootInRootField.isRoot_mk_and_ne_root {f : Polynomial ℤ} {b : Polynomial ℚ} (h : HasSecondRootInRootField f b) (hf : f.Monic) : have fℚ := Polynomial.map (Int.castRingHom ℚ) f; (Polynomial.map (algebraMap ℚ (AdjoinRoot fℚ)) fℚ).IsRoot ((AdjoinRoot.mk fℚ) b) ∧ (AdjoinRoot.mk fℚ) b ≠ AdjoinRoot.root fℚ

For a monic polynomial, formal second-root evidence gives the represented root in AdjoinRoot and proves that it differs from the distinguished root.