Documentation

TauCeti.FieldTheory.GaloisGroups.Certificate.Check

Quintic Galois-group certificates and their soundness #

A TauCeti.QuinticCertificate is a finite package of evidence about a monic integral quintic f, with one constructor for each sound route to a transitive-group label of degree five. Every constructor starts with a prime p modulo which f is irreducible; the further evidence is:

constructorfurther evidencelabel
cyclic p ba second root b of f in ℚ[X]/(f)5T1
dihedral p q s adisc f = s², sextic root a, factor degrees (1,2,2) modulo q5T2
frobeniusF20 p adisc f not a square, sextic root a5T3
alternating p q sdisc f = s², factor degrees (1,1,3) modulo q5T4
symmetric p qfactor degrees (2,3) modulo q5T5

Every factorization is taken modulo a prime not dividing disc f, as packaged by TauCeti.HasFactorDegrees. A sextic root is an integral root of the resolvent sextic TauCeti.resolventSextic f with nonzero discriminant, as packaged by TauCeti.HasSexticRoot. The irreducible reduction modulo p makes the Galois action transitive, and it also forces f to have degree five.

TauCeti.QuinticCertificate.Verifies lists the conditions the evidence must satisfy, and TauCeti.QuinticCertificate.check is the Boolean verdict on them. Every condition is finite: an equation or a non-square condition on integers, a congruence in ℚ[X], or a factorization over ZMod p.

The certificates are sound, and only sound: a certificate that verifies proves its label. Nothing here says that a certificate exists for a given quintic, or looks for one. Producing the primes a certificate needs is a question about the density of Frobenius elements. The discriminant and the sextic alone cannot separate 5T1 from 5T2, which is why the cyclic and dihedral routes carry further evidence.

Main definitions #

Main results #

References #

source
inductive TauCeti.QuinticCertificate :
Type

A certificate for the Galois group of a monic integral quintic. Each constructor is one sound route to a transitive-group label of degree five, and its arguments are the evidence that route reads: primes at which to factor, a square root of the discriminant, a root of the resolvent sextic, or a second root in the field generated by one root. The conditions this evidence must satisfy are TauCeti.QuinticCertificate.Verifies.

  • cyclic (p : ℕ) (b : Polynomial ℚ) : QuinticCertificate

    5T1: irreducible modulo p, and b represents a second root of f in ℚ[X]/(f).

  • dihedral (p q : ℕ) (s a : ℤ) : QuinticCertificate

    5T2: irreducible modulo p, discriminant s², a root a of the separable resolvent sextic, and factor degrees (1,2,2) modulo q, exhibiting an element of order two.

  • frobeniusF20 (p : ℕ) (a : ℤ) : QuinticCertificate

    5T3: irreducible modulo p, non-square discriminant, and a root a of the separable resolvent sextic.

  • alternating (p q : ℕ) (s : ℤ) : QuinticCertificate

    5T4: irreducible modulo p, discriminant s², and factor degrees (1,1,3) modulo q, exhibiting an element of order three.

  • symmetric (p q : ℕ) : QuinticCertificate

    5T5: irreducible modulo p, and factor degrees (2,3) modulo q, exhibiting an element of order six.

Instances For
    source
    def TauCeti.QuinticCertificate.label :
    QuinticCertificate → TransitiveGroupIndex 5

    The transitive-group label a certificate claims; index j is the label 5T(j+1).

    Equations
    Instances For
      source
      def TauCeti.QuinticCertificate.Verifies :
      QuinticCertificate → Polynomial ℤ → Prop

      The conditions that the evidence of a certificate must satisfy for the monic integral quintic f. Each route asks for an irreducible reduction of f modulo a prime not dividing its discriminant, together with the further evidence that separates its label from the others.

      Equations
      Instances For
        source
        noncomputable def TauCeti.QuinticCertificate.check (cert : QuinticCertificate) (f : Polynomial ℤ) :
        Bool

        The Boolean verdict on the verification conditions of a certificate.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.QuinticCertificate.label_cyclic (p : ℕ) (b : Polynomial ℚ) :
          (cyclic p b).label = ⟨0, label_cyclic._proof_1⟩

          A cyclic-route certificate claims the label 5T1.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.label_dihedral (p q : ℕ) (s a : ℤ) :
          (dihedral p q s a).label = ⟨1, label_dihedral._proof_1⟩

          A dihedral-route certificate claims the label 5T2.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.label_frobeniusF20 (p : ℕ) (a : ℤ) :
          (frobeniusF20 p a).label = ⟨2, label_frobeniusF20._proof_1⟩

          A Frobenius-route certificate claims the label 5T3.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.label_alternating (p q : ℕ) (s : ℤ) :
          (alternating p q s).label = ⟨3, label_alternating._proof_1⟩

          An alternating-route certificate claims the label 5T4.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.label_symmetric (p q : ℕ) :
          (symmetric p q).label = ⟨4, label_symmetric._proof_1⟩

          A symmetric-route certificate claims the label 5T5.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.verifies_cyclic_iff {f : Polynomial ℤ} {p : ℕ} {b : Polynomial ℚ} :
          (cyclic p b).Verifies f ↔ HasFactorDegrees f p {5} ∧ HasSecondRootInRootField f b

          The verification conditions of the cyclic route.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.verifies_dihedral_iff {f : Polynomial ℤ} {p q : ℕ} {s a : ℤ} :
          (dihedral p q s a).Verifies f ↔ HasFactorDegrees f p {5} ∧ f.discr = s ^ 2 ∧ HasSexticRoot f a ∧ HasFactorDegrees f q {1, 2, 2}

          The verification conditions of the dihedral route.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.verifies_frobeniusF20_iff {f : Polynomial ℤ} {p : ℕ} {a : ℤ} :
          (frobeniusF20 p a).Verifies f ↔ HasFactorDegrees f p {5} ∧ ¬IsSquare f.discr ∧ HasSexticRoot f a

          The verification conditions of the Frobenius route.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.verifies_alternating_iff {f : Polynomial ℤ} {p q : ℕ} {s : ℤ} :
          (alternating p q s).Verifies f ↔ HasFactorDegrees f p {5} ∧ f.discr = s ^ 2 ∧ HasFactorDegrees f q {1, 1, 3}

          The verification conditions of the alternating route.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.verifies_symmetric_iff {f : Polynomial ℤ} {p q : ℕ} :
          (symmetric p q).Verifies f ↔ HasFactorDegrees f p {5} ∧ HasFactorDegrees f q {2, 3}

          The verification conditions of the symmetric route.

          source
          @[simp]
          theorem TauCeti.QuinticCertificate.check_eq_true_iff {cert : QuinticCertificate} {f : Polynomial ℤ} :
          cert.check f = true ↔ cert.Verifies f

          A certificate checks exactly when its evidence verifies.

          source
          theorem TauCeti.QuinticCertificate.Verifies.hasGaloisLabel {cert : QuinticCertificate} {f : Polynomial ℤ} (hf : f.Monic) (h : cert.Verifies f) :
          HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) cert.label

          Soundness of quintic certificates. A certificate whose evidence verifies for a monic integral polynomial proves the label it claims for the Galois group of that polynomial over ℚ.

          source
          theorem TauCeti.QuinticCertificate.check_sound {cert : QuinticCertificate} {f : Polynomial ℤ} (hf : f.Monic) (h : cert.check f = true) :
          HasGaloisLabel (Polynomial.map (Int.castRingHom ℚ) f) cert.label

          Soundness of the quintic checker. A certificate that checks for a monic integral polynomial proves the label it claims for the Galois group of that polynomial over ℚ.