Automorphisms of extensions of prime degree

A finite extension of prime degree is Galois as soon as it has a nonidentity automorphism. Indeed, the automorphism group has order dividing the degree, by the fixed-field degree formula. This criterion is useful when a second root of a minimal polynomial already lies in the field generated by its first root. The general divisibility statement TauCeti.natCard_algEquiv_dvd_finrank lives in TauCeti.FieldTheory.Galois.FixedField, and the splitting-field facts for a normal simple extension in TauCeti.FieldTheory.Normal.Closure.

theorem TauCeti.isGalois_of_prime_finrank_of_exists_aut_ne_one (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] (hprime : Nat.Prime (Module.finrank F E)) (h : ∃ (σ : Gal(E/F)), σ ≠ 1) : IsGalois F E

A finite extension of prime degree with a nontrivial automorphism is Galois.

theorem TauCeti.isGalois_of_natDegree_prime_of_adjoin_simple_eq_top_of_exists_aut_ne_one (F : Type u_1) [Field F] (q : Polynomial F) (hprime : Nat.Prime q.natDegree) (E : Type u_2) [Field E] [Algebra F E] (x : E) (hminpoly : minpoly F x = q) (hgen : F⟮x⟯ = ⊤) (hAut : ∃ (σ : Gal(E/F)), σ ≠ 1) : IsGalois F E

A simple root field of a prime-degree polynomial is Galois as soon as it has a nonidentity automorphism.

theorem TauCeti.separable_of_natDegree_prime_of_exists_aut_ne_one (F : Type u_1) [Field F] (q : Polynomial F) (hprime : Nat.Prime q.natDegree) (E : Type u_2) [Field E] [Algebra F E] (x : E) (hminpoly : minpoly F x = q) (hgen : F⟮x⟯ = ⊤) (hAut : ∃ (σ : Gal(E/F)), σ ≠ 1) : q.Separable

A prime-degree polynomial whose simple root field has a nonidentity automorphism is separable.

theorem TauCeti.natCard_gal_eq_natDegree_of_prime_of_exists_aut_ne_one (F : Type u_1) [Field F] (q : Polynomial F) (hprime : Nat.Prime q.natDegree) (E : Type u_2) [Field E] [Algebra F E] (x : E) (hminpoly : minpoly F x = q) (hgen : F⟮x⟯ = ⊤) (hAut : ∃ (σ : Gal(E/F)), σ ≠ 1) : Nat.card q.Gal = q.natDegree

A prime-degree polynomial whose simple root field has a nonidentity automorphism has Galois group of order equal to its degree.