Good primes for resolvents

Specializing an integral resolvent and reducing modulo a prime commute without hypotheses. Interpreting that reduction as a subgroup test requires two separability conditions: the original polynomial must retain distinct roots, and the resolvent must retain distinct orbit values. These are the nondivisibility of their respective discriminants.

TauCeti.ResolventSpec.IsGoodPrime records both conditions. For a monic polynomial it is equivalent to separability of the reduction and of its specialized resolvent. The reduced resolvent then has a root in the prime field exactly when the Galois image of the reduced polynomial lies in a conjugate of the specification's subgroup. This is a statement about the Galois group over the prime field, with no assertion about the characteristic-zero Galois group.

Renaming the invariant preserves the condition, just as it preserves the resolvent itself. The degree of the resolvent is already preserved at every prime by ResolventSpec.natDegree_specialize; goodness concerns separability alone.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, Springer 1993, §6.3.

def TauCeti.ResolventSpec.IsGoodPrime {n : ℕ} (spec : ResolventSpec n) (f : Polynomial ℤ) (p : ℕ) : Prop

A prime candidate is good for a polynomial and a resolvent specification when it divides neither the polynomial discriminant nor the discriminant of the specialized resolvent. Primality is supplied separately when interpreting reduction over a field.

Equations

• spec.IsGoodPrime f p = (TauCeti.IsGoodPrime f p ∧ TauCeti.IsGoodPrime (spec.specialize ℤ f) p)

@[simp]

theorem TauCeti.ResolventSpec.isGoodPrime_iff {n : ℕ} (spec : ResolventSpec n) (f : Polynomial ℤ) (p : ℕ) : spec.IsGoodPrime f p ↔ ¬↑p ∣ f.discr ∧ ¬↑p ∣ (spec.specialize ℤ f).discr

The two discriminant conditions defining a good prime for a resolvent.

theorem TauCeti.ResolventSpec.IsGoodPrime.mk {n : ℕ} (spec : ResolventSpec n) {f : Polynomial ℤ} {p : ℕ} (hf : TauCeti.IsGoodPrime f p) (hres : TauCeti.IsGoodPrime (spec.specialize ℤ f) p) : spec.IsGoodPrime f p

Construct joint goodness from goodness for the polynomial and for its resolvent.

theorem TauCeti.ResolventSpec.IsGoodPrime.polynomial {n : ℕ} {f : Polynomial ℤ} {p : ℕ} {spec : ResolventSpec n} (h : spec.IsGoodPrime f p) : TauCeti.IsGoodPrime f p

Joint goodness implies goodness for the original polynomial.

theorem TauCeti.ResolventSpec.IsGoodPrime.resolvent {n : ℕ} {f : Polynomial ℤ} {p : ℕ} {spec : ResolventSpec n} (h : spec.IsGoodPrime f p) : TauCeti.IsGoodPrime (spec.specialize ℤ f) p

Joint goodness implies goodness for the integral specialized resolvent.

theorem TauCeti.ResolventSpec.IsGoodPrime.separable_map {n : ℕ} {f : Polynomial ℤ} {p : ℕ} {spec : ResolventSpec n} (h : spec.IsGoodPrime f p) (hf : f.Monic) [Fact (Nat.Prime p)] : (Polynomial.map (Int.castRingHom (ZMod p)) f).Separable

A good prime for a resolvent preserves separability of the original monic polynomial.

theorem TauCeti.ResolventSpec.IsGoodPrime.separable_specialize {n : ℕ} {f : Polynomial ℤ} {p : ℕ} {spec : ResolventSpec n} (h : spec.IsGoodPrime f p) [Fact (Nat.Prime p)] : (spec.specialize (ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) f)).Separable

A good prime for a resolvent preserves separability of the specialized resolvent. No monicity or degree hypothesis on the original polynomial is needed for this implication.

theorem TauCeti.ResolventSpec.isGoodPrime_iff_separable {n : ℕ} (spec : ResolventSpec n) {f : Polynomial ℤ} (hf : f.Monic) (p : ℕ) [Fact (Nat.Prime p)] : spec.IsGoodPrime f p ↔ (Polynomial.map (Int.castRingHom (ZMod p)) f).Separable ∧ (spec.specialize (ZMod p) (Polynomial.map (Int.castRingHom (ZMod p)) f)).Separable

For a monic polynomial, joint goodness is exactly separability of the reduction and of the resolvent specialized at that reduction.

theorem TauCeti.ResolventSpec.IsGoodPrime.exists_isRoot_map_specialize_iff {n : ℕ} {f : Polynomial ℤ} {p : ℕ} {E : Type u_1} [Field E] [Algebra (ZMod p) E] [Fact (Nat.Prime p)] [IsGalois (ZMod p) E] [Fact (Polynomial.map (algebraMap (ZMod p) E) (Polynomial.map (Int.castRingHom (ZMod p)) f)).Splits] {spec : ResolventSpec n} (h : spec.IsGoodPrime f p) (hf : f.Monic) (hdeg : f.natDegree = n) (e : ↑((Polynomial.map (Int.castRingHom (ZMod p)) f).rootSet E) ≃ Fin n) : (∃ (a : ZMod p), (Polynomial.map (Int.castRingHom (ZMod p)) (spec.specialize ℤ f)).IsRoot a) ↔ ∃ (τ : Equiv.Perm (Fin n)), Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom (Polynomial.map (Int.castRingHom (ZMod p)) f) E).range ≤ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj τ)) spec.H

At a jointly good prime, a root of the reduced integral resolvent detects containment of the Galois image of the reduced polynomial in a conjugate of the specification's subgroup. The root numbering is explicit, and E may be any Galois splitting extension.