Galois groups of polynomials
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremTauCeti.exists_monic_int_polynomial_hasFullSymmetricGaloisGroup#
Every positive degree occurs for a monic integral polynomial irreducible over ℚ
with full symmetric Galois group.
TauCeti.exists_monic_int_polynomial_hasFullSymmetricGaloisGroup (n : ℕ) (hn : 1 ≤ n) :
∃ f,
f.Monic ∧
f.natDegree = n ∧
Irreducible (Polynomial.map (Int.castRingHom ℚ) f) ∧
(Polynomial.map (Int.castRingHom ℚ) f).HasFullSymmetricGaloisGroup
Lean
Formalized in Tau Ceti as TauCeti.exists_monic_int_polynomial_hasFullSymmetricGaloisGroup.
Sources
Uses 1
TheoremTauCeti.existsUnique_transitiveGroupLabel_five#
A transitive subgroup of the symmetric group on five points carries exactly one label, one of
5T1, …, 5T5.
TauCeti.existsUnique_transitiveGroupLabel_five (G : Subgroup (Equiv.Perm (Fin 5)))
[MulAction.IsPretransitive (↥G) (Fin 5)] : ∃! j, TauCeti.TransitiveGroupLabel j G
DefinitionThe factorization theorem for a separable resolvent#
Let f be monic of
degree n, let E be a normal splitting extension, number the roots of f in E by e, and
let the resolvent of f for the specification be separable. The orbits of the Galois image, read
through e, on the cosets of H are then in bijection with the monic irreducible factors of the
resolvent over F: the orbit of the coset of τ goes to the minimal polynomial of the value at
the roots of the invariant renamed along τ.
The degree of each factor is the size of the matching orbit,
TauCeti.ResolventSpec.natCard_orbit_eq_natDegree_factor.
TauCeti.ResolventSpec.orbitQuotientEquivFactors.{u, v} {F : Type u} [Field F] {E : Type v} [Field E]
[Algebra F E] {f : Polynomial F} {n : ℕ} (spec : TauCeti.ResolventSpec n)
[Fact (Polynomial.map (algebraMap F E) f).Splits] [Normal F E] (hf : f.Monic)
(hdeg : f.natDegree = n) (e : ↑(f.rootSet E) ≃ Fin n)
(hres : TauCeti.ResolventSeparationEvidence spec f) :
MulAction.orbitRel.Quotient
(↥(Subgroup.map (↑e.permCongrHom) (Polynomial.Gal.galActionHom f E).range))
(Equiv.Perm (Fin n) ⧸ spec.H) ≃
(spec.specialize F f).Factors
Lean
Formalized in Tau Ceti as TauCeti.ResolventSpec.orbitQuotientEquivFactors.
Sources
Uses 3
TheoremThe quintic resolvent solvability criterion#
Let f be a monic irreducible separable
quintic over a field. If the specialization of Dummit's F₂₀ resolvent is separable, then
the polynomial Galois group is solvable if and only if that resolvent has a root in the base
field.
TauCeti.isSolvable_gal_iff_exists_isRoot_specialize_quinticF20Spec.{u} {F : Type u} [Field F]
{f : Polynomial F} (hf : f.Monic) (hsep : f.Separable) (hirr : Irreducible f)
(hdeg : f.natDegree = 5) (hres : TauCeti.ResolventSeparationEvidence TauCeti.quinticF20Spec f) :
Group.IsSolvable f.Gal ↔ ∃ a, (TauCeti.quinticF20Spec.specialize F f).IsRoot a
Lean
Formalized in Tau Ceti as TauCeti.isSolvable_gal_iff_exists_isRoot_specialize_quinticF20Spec.
Sources
Uses 3
StructureTauCeti.ResolventSpec#
A resolvent specification in degree n: a subgroup H of Equiv.Perm (Fin n), an
integral invariant Φ in n formal roots whose stabilizer under renaming is exactly H, and the
integral expression of the orbit product of Φ in the elementary symmetric polynomials. No
polynomial and no coefficient ring appears; specialization is ResolventSpec.specialize.
TauCeti.ResolventSpec (n : ℕ) : Type
StructureSeparation evidence for a specialized resolvent#
This records that the specialized
resolvent is separable. Under the usual monic degree-n splitting description, it says that
distinct elements of the symbolic orbit take distinct values at the roots of f. This is the
hypothesis that lets a root or a factorization of the resolvent constrain the Galois image;
specialization never loses degree, but its values can collide.
TauCeti.ResolventSeparationEvidence.{u_1} {F : Type u_1} [Field F] {n : ℕ}
(spec : TauCeti.ResolventSpec n) (f : Polynomial F) : Prop
Uses 1 · Used by 2
DefinitionTauCeti.HasGaloisLabel#
The Galois group of f carries the transitive-group label j of degree n: f is
separable of degree n, and some numbering of its roots in the splitting field by Fin n carries
the image of the Galois action on the roots to a conjugate of the reference subgroup
referenceSubgroup n j. By TauCeti.hasGaloisLabel_iff_forall, every numbering then does.
TauCeti.HasGaloisLabel.{u} {F : Type u} [Field F] (f : Polynomial F) {n : ℕ}
(j : TauCeti.TransitiveGroupIndex n) : Prop
DefinitionPolynomial.Gal.sign#
The parity character of the action of p.Gal on the distinct roots of p in its splitting
field. It takes values in ℤˣ, independently of the characteristic of the base field.
Polynomial.Gal.sign.{u} {F : Type u} [Field F] (p : Polynomial F) : p.Gal →* ℤˣ
Used by 1
TheoremVieta's formulas, in the form the symmetric descent uses#
if f is the product of the
linear factors attached to x, then substituting the signed coefficients of f is the same as
substituting the elementary symmetric polynomials and evaluating at x.
TauCeti.vietaHom_eq_comp_esymmSubst.{u_1} {R : Type u_1} [CommRing R] {n : ℕ} {f : Polynomial R}
{x : Fin n → R} (hf : f = ∏ i, (Polynomial.X - Polynomial.C (x i))) :
TauCeti.vietaHom n f = (MvPolynomial.eval₂Hom (Int.castRingHom R) x).comp (TauCeti.esymmSubst n)
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.