Add Galois-group certification library (Dedekind + discriminant certificates, degree-6 A₄×C₂ example)

[CBirkbeck]

What this adds

A self-contained Lean 4 / Mathlib library (IdealArithmetic/Galois/) for certifying the Galois group of a number field ℚ[x]/(f) from elementary factorisation data, together with a fully worked degree-6 example:

Gal(f/ℚ) ≅ A₄ × C₂ for f = X⁶ − 5X⁴ − 50X² + 125 — the transitive group 6T6, order 24.

Everything is sorry-free, and the headline results are verified axiom-clean (#print axioms → only the three standard axioms). lake build is green.

The general machinery is reusable for other fields/polynomials; only Examples/DegSixA4C2.lean is specific to the showcase polynomial.

---

General theorems

1. Dedekind's theorem — Frobenius cycle type from factorisation mod p

For monic f ∈ ℤ[X] and a prime p ∤ disc f, the cycle type of an arithmetic Frobenius acting on the roots of f equals the multiset of degrees of the irreducible factors of f mod p (Dedekind.lean):

theorem galActionHom_arithFrob_partition_eq_factor_degrees :
    (Polynomial.Gal.galActionHom (f.map (Int.castRingHom ℚ)) … (arithFrobAt ℤ … 𝔔)).partition.parts
      = (normalizedFactors (f.map (Int.castRingHom (ZMod p)))).map Polynomial.natDegree

Packaged as a user-facing certificate (Certificate.lean): supply a prime and a claimed factorisation, get a Galois element of the matching cycle type — no need to exhibit a prime of the splitting field.

structure FrobeniusCycleTypeCertificate (f : ℤ[X]) where
  p : ℕ ; hp : p.Prime
  hdisc : (Int.castRingHom (ZMod p)) f.discr ≠ 0     -- p ∤ disc f
  factors : Multiset (ZMod p)[X]
  hirr : ∀ q ∈ factors, Irreducible q
  hprod : factors.prod = f.map (Int.castRingHom (ZMod p))

theorem exists_partition_eq_of_certificate (f : ℤ[X]) (hf : f.Monic) (hdeg : f.natDegree ≠ 0)
    … (cert : FrobeniusCycleTypeCertificate f) :
    ∃ σ : (f.map (Int.castRingHom ℚ)).Gal,
      (Polynomial.Gal.galActionHom … σ).partition.parts = cert.factors.map Polynomial.natDegree

2. The discriminant square test — Aₙ vs Sₙ

Over a characteristic-zero field, the Galois action lands in the alternating group iff the discriminant is a square (Parity.lean, following K. Conrad, Galois groups as permutation groups, Thm 4.7):

theorem range_galActionHom_le_alternatingGroup_iff [CharZero F] (p : F[X])
    (hmonic : p.Monic) (hp : p.Separable) :
    MonoidHom.range (galActionHom p p.SplittingField) ≤ alternatingGroup _ ↔ IsSquare p.discr

3. Cubic Galois groups, end to end

Combining (1) and (2): the Galois group of any monic irreducible cubic over ℚ is A₃ (order 3) or S₃ (order 6) according to whether disc is a square (Determine.lean):

theorem galoisGroup_cubic (p : ℚ[X]) (hp : Irreducible p) (hmonic : p.Monic) (h3 : p.natDegree = 3) :
    (IsSquare p.discr → Nat.card p.Gal = 3) ∧ (¬ IsSquare p.discr → Nat.card p.Gal = 6)

4. Even polynomials f = h(X²) — block-sign analysis

For f = h.comp (X²), the ±-pairing of roots is a Gal f-invariant block system. The order factors through the composition, and the kernel K = ker(restrict to Gal h) is identified with C₂^{#roots of h} (EvenSextic.lean):

theorem card_gal_comp_eq {F : Type*} [Field F] (p q : F[X]) (hq : q.natDegree ≠ 0) :
    Nat.card (p.comp q).Gal = Nat.card p.Gal * Nat.card (MonoidHom.ker (Gal.restrictComp p q hq))

noncomputable def blockSignEquiv … :        -- K ≃* C₂^{roots of h}
    ↥(MonoidHom.ker (Gal.restrictComp h (X ^ 2) hq)) ≃*
      Multiplicative (h.rootSet (h.comp (X ^ 2)).SplittingField → ZMod 2)
-- card_ker_eq : |K| = 2 ^ (#roots of h),  given the blocks are nondegenerate and every flip is realised

5. The abstract endpoint C₂³ ⋊ C₃ ≅ A₄ × C₂

Pure finite-group theory (SemidirectA4.lean): for a 3-element block set with an order-3 cyclic block permutation, the semidirect product is A₄ × C₂ (6T6):

theorem threeBlockIso {S : Type*} [Fintype S] [DecidableEq S] (hcard : Fintype.card S = 3)
    (τ : Equiv.Perm S) (hτ : orderOf τ = 3) (hτ3 : τ ^ 3 = 1) :
    Nonempty ((Multiplicative (S → ZMod 2)) ⋊[blockAction τ hτ3] (Multiplicative (ZMod 3)) ≃* A4timesC2)

Supporting reusable pieces: separable_map_of_discr_ne_zero (p ∤ disc f ⇒ f mod p separable, SeparableReduction.lean), the sign character signHom and splitting-field Fact instance (Defs.lean).

---

How the example is certified

f = X⁶ − 5X⁴ − 50X² + 125 is even: f = g(X²) with g = Y³ − 5Y² − 50Y + 125 (Examples/DegSixA4C2.lean). The certificate assembles the general theorems as follows.

1. The cubic g is cyclic. g is irreducible with square discriminant, so by galoisGroup_cubic, Gal g ≅ C₃ — card_gal_g : Nat.card (g.map …).Gal = 3.

2. Order factors through the square. Since f = g(X²), card_gal_comp_eq gives |Gal f| = |Gal g| · |K| where K = ker(Gal f ↠ Gal g) is the block-flip kernel.

3. One Frobenius transposition, from p = 13. The certificate cert13 : FrobeniusCycleTypeCertificate f records
   f mod 13 = (X+2)(X+5)(X−5)(X−2)(X²−2), cycle type {1,1,1,1,2}.
   Via Dedekind's theorem this yields an arithmetic Frobenius that flips exactly one ±-block — a single generator of K.

4. The C₃ symmetry spreads it to all three blocks. Conjugating that one flip by the cyclic C₃-action realises every coordinate flip, so K ≅ C₂³ with |K| = 8 (card_ker : … = 8). Hence |Gal f| = 3 · 8 = 24:

   theorem card_gal_f : Nat.card (f.map (Int.castRingHom ℚ)).Gal = 24

5. Identify the group. The C₃-action on K = C₂³ is the cyclic coordinate permutation, so threeBlockIso applies and gives the isomorphism type:

   theorem gal_f_mulEquiv :
       Nonempty ((f.map (Int.castRingHom ℚ)).Gal ≃*
         alternatingGroup (Fin 4) × Multiplicative (ZMod 2))

So Gal(f/ℚ) ≅ A₄ × C₂ (6T6, order 24), certified from the single input f mod 13 plus the cyclic-cubic structure.

---

Notes

• New files: Defs, Parity, SeparableReduction, Dedekind, Certificate, Determine, EvenSextic, SemidirectA4, Examples/DegSixA4C2 (all under IdealArithmetic/Galois/), plus a .gitignore for /.lake/.
• No native_decide; regular decide only where a finite group computation is closed.
• sorry-free; card_gal_f, gal_f_mulEquiv, galoisGroup_cubic, threeBlockIso, and the Dedekind theorem are all axiom-clean.

🤖 Generated with Claude Code

[CBirkbeck]

Closing this PR — the Galois-group certification work is moving to CBirkbeck/LeanBridge (a project linking LMFDB and Lean), where it has been ported to Lean v4.31 / mathlib fabf563a and integrated as a dependency: CBirkbeck/LeanBridge#80 . Thanks!