Alphabeta Math
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 24 results · all verified · 22 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Galois Correspondence

1 · Prerequisites

2 · Summary

Finite extensions, splitting fields, embeddings into algebraic closures, normality, and separability provide the field-theoretic background. Separable degree bounds the number of relative automorphisms, while the sign homomorphism and symmetric-polynomial theorem control the Vandermonde product, discriminant, and quartic resolvent. The tower law and quotient-group isomorphism theorem supply the degree and restriction calculations.

Relative automorphism groups and fixed fields lead through Dedekind independence to Artin's fixed-field theorem. The equivalent Galois conditions then support the inclusion-reversing subgroup-field correspondence, its normality and quotient clause, translation, and compositum formulas. Finally the action on roots relates irreducibility to transitivity; discriminants classify monic separable irreducible cubics in characteristic not two, and the resolvent gives the possible transitive quartic Galois groups under the same characteristic hypothesis.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Relative field automorphisms and Aut⁡(K/F)

Definition

Let K/F be a field extension. An F-automorphism of K is an F-isomorphism K→K. This is the relative-automorphism case of F-homomorphisms and F-embeddings of field extensions.

The set of all F-automorphisms of K is denoted

Aut⁡(K/F):={σ:K→K:σ is an F-automorphism}.

Composition is the proposed operation. That it makes this set a group, and the basic finite-extension bound on its order, are proved in Aut⁡(K/F) is a group and ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F] ↗.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Aut⁡(K/F) is a group and ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F]

Statement

For every field extension K/F, composition makes Aut⁡(K/F) a group. If K/F is finite, then

∣Aut⁡(K/F)∣≤[K:F]s≤[K:F].

In particular the relative automorphism group is finite.

Facts & Assumptions

Given: A field extension K/F; for the inequalities, a finite extension, an algebraic closure Ω of F, and the Axiom of Choice used by the embedding-extension theorem.

[F1]

An F-automorphism of K is an F-isomorphism K→K (Relative field automorphisms and Aut⁡(K/F)).

[A1]

Assuming the Axiom of Choice, an embedding F→Ω extends across the algebraic extension K/F to an F-embedding τ:K→Ω (Assuming Choice, a base-field embedding extends across every algebraic extension); the separable degree [K:F]s is the number of F-embeddings K→Ω (The separable degree [K:F]s as a count of embeddings into an algebraic closure).

[L1]

For every finite field extension K/F, one has [K:F]s≤[K:F] (For a finite extension, [K:F]s≤[K:F]).

Proof

technique · direct
1.1F1algebra

The identity map is an F-automorphism, the composite of two F-automorphisms is an F-automorphism, and the inverse of an F-isomorphism is again an F-isomorphism fixing F; associativity is inherited from composition. Thus Aut⁡(K/F) is a group. Every such map fixes 0 and 1, so no zero case is excluded.

1.2A1F1choose

For finite K/F, choose τ:K→Ω as in [A1]. The map σ↦τ∘σ sends Aut⁡(K/F) into the set of F-embeddings K→Ω and is injective, because τ∘σ1=τ∘σ2 and injectivity of τ imply σ1=σ2.

2.1step 1.2L1∎

Step 1.2 and the definition of separable degree give ∣Aut⁡(K/F)∣≤[K:F]s, while [L1] gives [K:F]s≤[K:F]. If K=F, all three numbers are 1, so this includes the degree-one endpoint.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The fixed field KG of a group of field automorphisms

Definition

Let K be a field and let G be a subgroup of its automorphism group. The fixed field of G is

KG:={x∈K:σ(x)=x for every σ∈G}.

This is a subfield of K. Every field automorphism fixes 0 and 1, so these elements lie in KG. If x,y∈KG and σ∈G, then σ(x−y)=x−y and σ(xy)=xy; if also x≠0, then σ(x−1)=σ(x)−1=x−1. Thus KG is closed under subtraction, multiplication, and inverses of nonzero elements. In particular, when G≤Aut⁡(K/F) (Relative field automorphisms and Aut⁡(K/F)), one has F⊆KG⊆K.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Dedekind's linear independence theorem for distinct characters

Statement

Let G be a group and K a field. Every finite family of distinct group homomorphisms G→K× is linearly independent over K as a family of functions.

Facts & Assumptions

[A1]

For every character χ, one has χ(gx)=χ(g)χ(x), and every value χ(g) lies in K× and is nonzero.

Proof

technique · contradiction
1.1assume-contrachoose

The empty family is independent vacuously, and a singleton is independent because its character never vanishes. Suppose, for contradiction, that some finite distinct family is dependent; among all nonzero relations choose one with the least support, relabel its supported characters as χ1,…,χr, and divide by the first nonzero coefficient to write ∑i=1raiχi(x)=0 for every x∈G, where r≥2 and a1=1.

2.1step 1.1A1choosealgebra

Since χ1≠χr, choose g∈G with χ1(g)≠χr(g). Evaluate the relation of step 1.1 at gx and subtract χr(g) times its value at x to obtain ∑i=1r−1ai(χi(g)−χr(g))χi(x)=0 for every x∈G.

3.1step 1.1step 2.1discharge-contradiction∎

The new relation has support smaller than r but is nonzero because its χ1-coefficient is χ1(g)−χr(g)≠0. This contradicts the minimality in step 1.1, so no nontrivial relation exists and the characters are linearly independent.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Artin's fixed-field lower bound [K:KG]≥∣G∣

Statement

If G is a finite group of automorphisms of K, then [K:KG]≥∣G∣.

Facts & Assumptions

Given: A field K, a finite group G={σ1,…,σm} of automorphisms of K, and its fixed field KG (The fixed field KG of a group of field automorphisms).

[L1]

Every finite family of distinct group homomorphisms G→K× is linearly independent over K as a family of functions (Dedekind's linear independence theorem for distinct characters).

Proof

technique · direct
1.1L1choose

Restricted to K×, the distinct automorphisms σ1,…,σm are distinct characters K×→K×, so [L1] makes them linearly independent as functions. Hence their evaluation vectors span Km: otherwise a nonzero linear functional on their span would give a nontrivial K-linear relation among the σi. Choose nonzero x1,…,xm∈K such that the evaluation matrix A=(σi(xj))i,j is invertible. For m=1, one may take x1=1.

2.1step 1.1L1algebra

Suppose c1,…,cm∈KG satisfy ∑jcjxj=0. Applying each σi and using σi(cj)=cj gives A(c1,…,cm)T=0, so invertibility of A forces every cj=0. Thus x1,…,xm are linearly independent over KG.

3.1step 2.1∎

A KG-linearly independent family of m=∣G∣ elements of K gives [K:KG]≥m=∣G∣.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Artin's fixed-field upper bound [K:KG]≤∣G∣

Statement

If G is a finite group of automorphisms of K, then [K:KG]≤∣G∣.

Facts & Assumptions

Given: A field K, a finite group G={σ1,…,σm} of automorphisms of K with σ1 the identity, and arbitrary elements x1,…,xm+1∈K.

[L1]

If T:V→W is linear and V is finite-dimensional, then dim⁡V=dim⁡ker⁡T+dim⁡im⁡T (Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T).

Proof

technique · direct
1.1L1

Define the K-linear map T:Km+1→Km by T(c1,…,cm+1)=(∑jcjσi(xj))i=1m. Since the domain has dimension m+1 and the codomain dimension m, [L1] gives a nonzero vector in ker⁡T.

2.1step 1.1choosealgebra

Among nonzero vectors in ker⁡T, choose c=(cj) with least support and scale it so its first supported coordinate is 1. For τ∈G, applying τ to all equations T(c)=0 and reindexing the rows by σi↦τσi shows that τ(c)=(τ(cj)) also lies in ker⁡T. The vector τ(c)−c has a zero in the normalized coordinate and support strictly smaller than that of c unless it vanishes; minimality therefore gives τ(cj)=cj for every j and every τ∈G, so all cj lie in KG.

3.1step 2.1∎

The identity row of T(c)=0 is ∑jcjxj=0, a nontrivial KG-linear dependence among the arbitrary m+1 elements. Thus no m+1 elements of K are linearly independent over KG, and [K:KG]≤m=∣G∣. This includes m=1 and also covers repeated or zero xj.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G

Statement

If G is a finite group of automorphisms of K, then [K:KG]=∣G∣ and Aut⁡(K/KG)=G.

Facts & Assumptions

Given: A field K, a finite automorphism group G, and the fixed field KG.

[L1]

If G is a finite group of automorphisms of K, then [K:KG]≥∣G∣ (Artin's fixed-field lower bound [K:KG]≥∣G∣).

[L2]

If G is a finite group of automorphisms of K, then [K:KG]≤∣G∣ (Artin's fixed-field upper bound [K:KG]≤∣G∣).

[L3]

For a finite extension K/E, one has ∣Aut⁡(K/E)∣≤[K:E] (Aut⁡(K/F) is a group and ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F]).

Proof

technique · direct
1.1L1L2

The opposing bounds [L1] and [L2] give [K:KG]=∣G∣. In particular K/KG is finite. For G={1} this says KG=K and the degree is 1.

2.1step 1.1L3algebra∎

Every σ∈G fixes KG, so G⊆Aut⁡(K/KG). By [L3] and step 1.1, ∣Aut⁡(K/KG)∣≤[K:KG]=∣G∣; a finite set containing G and having at most its cardinality equals G.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Distinct finite automorphism groups have distinct fixed fields

Statement

For a field K, the assignment G↦KG is injective on finite groups of automorphisms of K. Equivalently, distinct finite automorphism groups have distinct fixed fields.

Facts & Assumptions

Given: Finite groups G,H of automorphisms of one field K.

[L1]

If G is a finite group of automorphisms of K, then [K:KG]=∣G∣ and Aut⁡(K/KG)=G (Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G).

Proof

technique · direct
1.1L1

If KG=KH=E, then [L1] applied to each group gives G=Aut⁡(K/E)=H. Thus equal fixed fields force equal groups, including when either group is trivial.

2.1step 1.1∎

Step 1.1 is precisely injectivity of G↦KG; its contrapositive says that distinct finite automorphism groups have distinct fixed fields.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

For a finite extension, ∣Aut⁡(K/F)∣ divides [K:F]

Statement

If K/F is a finite extension, then ∣Aut⁡(K/F)∣ divides [K:F].

Facts & Assumptions

Given: A finite extension K/F, the finite group G:=Aut⁡(K/F) supplied by Aut⁡(K/F) is a group and ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F], and its fixed field E:=KG (The fixed field KG of a group of field automorphisms).

[L1]

If G is a finite group of automorphisms of K, then [K:KG]=∣G∣ and Aut⁡(K/KG)=G (Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G).

[L2]

If F⊆E⊆K and both successive extensions are finite, then [K:F]=[K:E][E:F] (Tower law for finite extensions: [L:F]=[L:K][K:F]).

Proof

technique · direct
1.1L1

Artin's theorem gives ∣Aut⁡(K/F)∣=∣G∣=[K:E].

2.1step 1.1L2∎

The tower formula gives [K:F]=[K:E][E:F]=∣Aut⁡(K/F)∣[E:F], proving the divisibility. Degree one and a trivial automorphism group both give divisor 1.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Finite Galois extensions and Gal⁡(K/F)

Definition

A finite extension K/F is Galois when it is normal (A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there) and separable (Separable algebraic elements and separable extensions). Its Galois group is

Gal⁡(K/F):=Aut⁡(K/F),

with the group operation supplied by Relative field automorphisms and Aut⁡(K/F). The notation Gal⁡(K/F) is reserved here for an extension already known to be finite Galois; for an arbitrary extension the notation remains Aut⁡(K/F).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Equivalent characterizations of a finite Galois extension

Statement

Let K/F be a finite extension and put G=Aut⁡(K/F). The following conditions are equivalent:

  1. K/F is Galois, that is, normal and separable.
  2. K is the splitting field over F of a separable polynomial.
  3. ∣G∣=[K:F].
  4. KG=F.

In particular, a finite extension is Galois if and only if it is the splitting field of a separable polynomial.

Facts & Assumptions

Given: A finite extension K/F and G=Aut⁡(K/F); splitting fields as in Polynomials that split and splitting fields of a polynomial or a family of polynomials; the facts that endomorphisms of a splitting field permute its roots (Every F-endomorphism of a splitting field permutes the distinct roots and is an automorphism), K/F is separable exactly when [K:F]s=[K:F] (A finite extension is separable if and only if [K:F]s=[K:F]), and finite degrees multiply in towers (Tower law for finite extensions: [L:F]=[L:K][K:F]); the separable degree [K:F]s is the number of F-embeddings of K into an algebraic closure of F (The separable degree [K:F]s as a count of embeddings into an algebraic closure).

[L1]

If H is a finite group of automorphisms of a field L, then [L:LH]=∣H∣ and Aut⁡(L/LH)=H (Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G).

[L2]

If E/F is normal and E=F(α1,…,αm), then E is the splitting field of the product of the minimal polynomials of the generators; for m=0 the product is 1 and E=F (A normal extension generated by finitely many elements is the splitting field of the product of their minimal polynomials).

[L3]

If K/F is algebraic and K=F(S) for a set S of elements separable over F, then K/F is separable (An algebraic extension generated by separable elements is separable).

[L4]

For every field extension K/F composition makes Aut⁡(K/F) a group, and if K/F is finite then ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F]; in particular the relative automorphism group is finite (Aut⁡(K/F) is a group and ∣Aut⁡(K/F)∣≤[K:F]s≤[K:F]).

Proof

technique · direct
1.1L2given

For the implication from condition 1 to condition 2, choose a finite generating family for K/F. By [L2], normality makes K the splitting field of the product of their distinct minimal polynomials; separability makes each factor separable, so their distinct product is separable. If K=F, the empty product 1 has splitting field F.

1.2givenL3

For the implication from condition 2 to condition 3, let K be the splitting field of the separable f∈F[x]. Then K is generated over F by the roots of f, and the minimal polynomial of each root divides f and therefore has no repeated root, so every generator is separable over F; by [L3], K/F is separable and the full-degree criterion in the Given gives [K:F]s=[K:F]. Every F-embedding of K into an algebraic closure permutes the roots of f and hence maps K onto itself, so the [K:F]s embeddings are precisely the elements of G and ∣G∣=[K:F].

1.3L1given

For the implication from condition 3 to condition 4, [L1] gives [K:KG]=∣G∣=[K:F]. Since F⊆KG⊆K, the tower law forces [KG:F]=1, hence KG=F.

2.1L1L4givenalgebra∎

For the implication from condition 4 to condition 1, [L4] makes G finite, so [L1] applies to H=G and gives [K:KG]=∣G∣; with KG=F this reads ∣G∣=[K:F]. The bound in [L4] then gives [K:F]=∣G∣≤[K:F]s≤[K:F], so [K:F]s=[K:F] and the full-degree criterion in the Given makes K/F separable. For α∈K, the orbit polynomial qα(x)=∏β∈Gα(x−β) has distinct roots in K and coefficients fixed by G, hence in KG=F. The minimal polynomial of α divides qα, while every orbit element is one of its roots; separability makes qα divide that minimal polynomial. They are therefore equal, so every minimal polynomial over F splits in K and K/F is normal. This also covers α=0 and the degree-one extension.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A finite Galois extension is Galois over every intermediate field

Statement

If K/F is finite Galois and F⊆E⊆K, then K/E is finite Galois.

Facts & Assumptions

Given: A finite normal and separable extension K/F (Finite Galois extensions and Gal⁡(K/F)) and an intermediate field E; separability means every element has a separable minimal polynomial (Separable algebraic elements and separable extensions), and a finite F-basis of K also spans K over E.

[L1]

If K/F is a normal algebraic extension and F⊆E⊆K, then K/E is a normal algebraic extension (If K/F is normal and F⊆E⊆K, then K/E is normal).

Proof

technique · direct
1.1L1

Normality of K/F descends through the intermediate field, so K/E is normal.

1.2givenalgebra

For α∈K, its minimal polynomial over E divides its separable minimal polynomial over F, since the latter lies in E[x] and vanishes at α. A divisor of a separable polynomial is separable, so K/E is separable. This includes α=0.

2.1step 1.1step 1.2given∎

The extension K/E is finite because a finite F-basis spans it over E; together with steps 1.1 and 1.2 this makes K/E finite Galois. Both endpoints are included: E=F recovers the hypothesis and E=K gives the degree-one extension.

Remarks

The conclusion concerns K/E. The extension E/F need not be normal; the normal-subgroup criterion identifies exactly when it is.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Galois closure of a finite separable extension

Definition

Let K/F be a finite separable extension embedded in a fixed algebraic closure Ω of F. Its Galois closure in Ω is the normal closure NΩ(K/F) of The normal closure of an algebraic extension inside a fixed algebraic closure.

Equivalently, it is the least subfield L of Ω containing K for which L/F is finite Galois (Finite Galois extensions and Gal⁡(K/F)). The existence, finiteness, separability, and leastness asserted by this terminology are established in Finite separable extensions have finite minimal Galois closures ↗.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Finite separable extensions have finite minimal Galois closures

Statement

Let K/F be a finite separable extension inside an algebraic closure Ω of F. Its Galois closure L=NΩ(K/F) exists, is finite Galois over F, and is contained in every subfield of Ω that contains K and is Galois over F.

Facts & Assumptions

Given: A finite separable extension K/F⊆Ω, the Galois-closure definition of The Galois closure of a finite separable extension, the fact that an algebraic extension generated by separable elements is separable (An algebraic extension generated by separable elements is separable), and the equivalence between finite Galois extensions and separable splitting fields (Equivalent characterizations of a finite Galois extension).

[L1]

The normal closure in Ω of a finite extension is finite over F and is the splitting field of the product of the minimal polynomials of a finite generating family (The normal closure of a finite extension exists and is finite).

Proof

technique · direct
1.1L1

Choose a finite generating family K=F(α1,…,αr). By [L1], the normal closure L is finite over F and is the splitting field of the product of the minimal polynomials of the generators. If r=0, then K=F and L=F. Repeated minimal polynomials may be removed from the product.

2.1step 1.1given

Each generator is separable over F, so every root of its minimal polynomial is separable over F. The field L is generated by those roots, hence is separable; it is normal by construction, so it is finite Galois.

3.1L1step 2.1∎

If M is a subfield of Ω containing K and Galois over F, then M/F is normal. The normal closure is the intersection of all normal subextensions containing K, so L⊆M. Thus L is the required minimal Galois overfield.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The fundamental theorem of finite Galois theory

Statement

Let K/F be finite Galois and let G=Gal⁡(K/F). The assignments H↦KH and E↦Gal⁡(K/E) are mutually inverse inclusion-reversing bijections between subgroups H≤G and intermediate fields F⊆E⊆K. Moreover,

[K:KH]=∣H∣and[KH:F]=[G:H].

Facts & Assumptions

Given: A finite Galois extension K/F, its finite group G, the fact that K/E is finite Galois for every intermediate field E (A finite Galois extension is Galois over every intermediate field), the tower law (Tower law for finite extensions: [L:F]=[L:K][K:F]), and the finite-group formula ∣G∣=∣H∣[G:H] (Lagrange's theorem: ∣G∣=[G:H]∣H∣ for every subgroup H of a finite group G).

[L1]

If H is a finite group of automorphisms of K, then [K:KH]=∣H∣ and Aut⁡(K/KH)=H (Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G).

[L2]

For a finite extension L/E with G=Aut⁡(L/E), being Galois, being the splitting field of a separable polynomial, ∣G∣=[L:E], and LG=E are equivalent (Equivalent characterizations of a finite Galois extension).

Proof

technique · direct
1.1L1

For the subgroup-to-field-to-subgroup direction, Artin applied to H gives Gal⁡(K/KH)=Aut⁡(K/KH)=H. This includes H={1}, whose fixed field is K, and H=G.

1.2L1L2given

For the field-to-subgroup-to-field direction, put H=Gal⁡(K/E). Since K/E is finite Galois, [L2] gives ∣H∣=[K:E]. Artin gives [K:KH]=∣H∣=[K:E], while E⊆KH; the tower law forces E=KH. This includes E=K and E=F.

2.1step 1.1step 1.2L1L2given∎

If H1⊆H2, then every element fixed by H2 is fixed by H1, so KH2⊆KH1; the reverse map is likewise inclusion-reversing. Artin gives [K:KH]=∣H∣, while [L2] applied to K/F gives [K:F]=∣G∣, so the tower and Lagrange formulas give [KH:F]=∣G∣/∣H∣=[G:H]. Together with steps 1.1 and 1.2 these statements prove the claimed bijections and degree formulas.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence

Statement

Let K/F be finite Galois, let G=Gal⁡(K/F), let H≤G, and put E=KH. For every σ∈G,

Gal⁡(K/σ(E))=σHσ−1.

An intermediate field E/F is Galois exactly when its corresponding subgroup is normal. In that case restriction gives a surjective homomorphism G→Gal⁡(E/F) with kernel H, and hence

Gal⁡(E/F)≅G/H.

Facts & Assumptions

Given: The finite Galois correspondence; normal subgroups and quotient groups (Normal subgroup: invariance under conjugation, The quotient group G/N and coset product (gN)(hN)=ghN); the characterization of a normal algebraic extension by stability of conjugates (A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there); the Axiom of Choice and algebraic embedding extension (Assuming Choice, a base-field embedding extends across every algebraic extension); and the first isomorphism theorem for groups (First isomorphism theorem for groups: G/ker⁡f≅im⁡f).

[L1]

The assignments H↦KH and E↦Gal⁡(K/E) are mutually inverse inclusion-reversing bijections (The fundamental theorem of finite Galois theory).

[F1]

A subgroup is normal exactly when it is invariant under conjugation (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

Proof

technique · direct
1.1L1algebra

For x∈K, the element x is fixed by σHσ−1 exactly when σ−1(x) is fixed by H, exactly when σ−1(x)∈E, and exactly when x∈σ(E). Thus KσHσ−1=σ(E), and [L1] gives Gal⁡(K/σ(E))=σHσ−1.

2.1step 1.1L1F1given

For the forward direction, if H⊴G, then step 1.1 gives σ(E)=E for every σ∈G; every F-conjugate of an element of E is obtained by extending its embedding to K and hence lies in E, so E/F is normal, and it is separable as a subextension of the separable extension K/F, hence Galois. For the reverse direction, if E/F is Galois, normality gives σ(E)=E for every σ∈G, so step 1.1 and [L1] give σHσ−1=H and [F1] gives H⊴G.

3.1step 2.1L1given∎

In the normal case, restriction ρ:G→Gal⁡(E/F) is defined by step 2.1. Every F-automorphism of E extends to an embedding of K in an algebraic closure; normality of K/F makes the extension an element of G, so ρ is surjective. Its kernel consists exactly of the automorphisms fixing E, namely H by [L1]. The first isomorphism theorem therefore gives G/H≅Gal⁡(E/F); for H={1} and H=G this yields the two endpoint quotients.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A finite Galois extension has finitely many intermediate fields

Statement

A finite Galois extension has only finitely many intermediate fields.

Facts & Assumptions

Given: A finite Galois extension K/F and its finite Galois group G.

[L1]

The assignments H↦KH and E↦Gal⁡(K/E) are mutually inverse inclusion-reversing bijections (The fundamental theorem of finite Galois theory).

Proof

technique · direct
1.1given

A finite group has a finite power set, and its subgroups form a subcollection of that power set; hence G has finitely many subgroups.

2.1step 1.1L1∎

By [L1], the intermediate fields are in bijection with those subgroups, so there are finitely many. When K=F, both collections have one member, and the base and top endpoints coincide.

Remarks

The library proves more than this elsewhere: A finite separable extension has only finitely many intermediate fields drops normality and keeps the conclusion, by the Steinitz primitive-element route rather than by the correspondence. The corollary here is recorded because it is what the Galois correspondence gives immediately, not because the separable statement is unavailable.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Galois correspondence exchanges composita with subgroup intersections and field intersections with generated subgroups

Statement

Let K/F be finite Galois, and let Ei=KHi correspond to subgroups Hi≤Gal⁡(K/F) for i=1,2. Then

Gal⁡(K/E1E2)=H1∩H2,

and

Gal⁡(K/E1∩E2)=⟨H1,H2⟩.

Facts & Assumptions

Given: The compositum E1E2, the generated subgroup ⟨H1,H2⟩ of The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups, and the subgroup intersection of The intersection of a nonempty family of subgroups of G is a subgroup of G.

[L1]

The assignments H↦KH and E↦Gal⁡(K/E) are mutually inverse inclusion-reversing bijections (The fundamental theorem of finite Galois theory).

Proof

technique · direct
1.1L1algebra

An automorphism of K fixes E1E2 exactly when it fixes every element of both E1 and E2, exactly when it belongs to both H1 and H2. Therefore Gal⁡(K/E1E2)=H1∩H2.

2.1L1step 1.1∎

An element of K is fixed by ⟨H1,H2⟩ exactly when it is fixed by every element of both generating subgroups, so K⟨H1,H2⟩=KH1∩KH2=E1∩E2. Applying [L1] gives the second formula. These membership equivalences also cover equal fields, the base and top fields, and trivial or full subgroups.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Galois translation theorem

Statement

Let E/F be finite Galois and let L/F be a field extension inside a common overfield. Then EL/L is finite Galois, and restriction gives

Gal⁡(EL/L)≅Gal⁡(E/E∩L).

Facts & Assumptions

Given: The compositum EL and intersection D:=E∩L inside the common overfield.

[L1]

A finite extension is Galois if and only if it is the splitting field of a separable polynomial, and for a finite Galois extension the fixed field of the full Galois group is the base field (Equivalent characterizations of a finite Galois extension).

[L2]

If H is a finite group of automorphisms of a field K, then [K:KH]=∣H∣ and Aut⁡(K/KH)=H (Artin's fixed-field theorem: [K:KG]=∣G∣ and Aut⁡(K/KG)=G).

Proof

technique · direct
1.1L1

By [L1], E is the splitting field over F of a separable polynomial f. The same polynomial over L remains separable and has splitting field EL, so [L1] makes EL/L finite Galois.

2.1step 1.1

An element of Gal⁡(EL/L) permutes the roots of f, hence preserves E, and its restriction to E fixes D=E∩L. Restriction therefore defines a homomorphism into Gal⁡(E/D); it is injective because EL is generated by E and L.

3.1step 2.1L1L2∎

Let H be the restriction image. By [L1], an element of E is fixed by H exactly when it is fixed by every automorphism of EL/L, exactly when it lies in L; thus EH=E∩L=D. By [L2], H=Aut⁡(E/EH)=Gal⁡(E/D), so restriction is surjective and hence an isomorphism. If E⊆L, both groups are trivial; if L=F or D=F, the displayed formula specializes directly.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Galois group of a compositum is a fibre product of Galois groups

Statement

Let E1/F and E2/F be finite Galois extensions inside a common overfield, and put D=E1∩E2. Then E1E2/F is finite Galois and restriction identifies its Galois group with the fibre product

{(σ1,σ2)∈Gal⁡(E1/F)×Gal⁡(E2/F):σ1∣D=σ2∣D}.

This image is the full direct product exactly when D=F.

Facts & Assumptions

Given: Finite Galois extensions E1/F and E2/F; writing fi for a separable polynomial with splitting field Ei, their compositum is the splitting field over F of the product of the distinct irreducible factors of f1f2, a polynomial with the same roots as f1f2 and no repeated one, so the compositum is Galois by Equivalent characterizations of a finite Galois extension; restriction from a Galois extension onto a Galois intermediate field is surjective by Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence; and the fixed field of a full finite Galois group is the base field by The fundamental theorem of finite Galois theory.

[L1]

For finite Galois E/L0 and any extension L/L0, restriction gives Gal⁡(EL/L)≅Gal⁡(E/E∩L) (The Galois translation theorem).

Proof

technique · direct
1.1given

Restriction sends Gal⁡(E1E2/F) injectively into the product of the two relative Galois groups, since E1E2 is generated by E1 and E2. Both restrictions agree on D, so the image lies in the displayed fibre product.

2.1step 1.1L1given

Conversely, let (σ1,σ2) have equal restrictions to D. Extend σ2 to some τ∈Gal⁡(E1E2/F) using surjectivity of restriction. Then ρ:=σ1(τ∣E1)−1 fixes D, and [L1] supplies h∈Gal⁡(E1E2/E2) with h∣E1=ρ. The automorphism hτ restricts to σ1 and σ2, proving that every compatible pair is in the image.

3.1step 2.1given∎

For the forward implication of the last assertion, if D=F then compatibility is automatic and step 2.1 gives the full product. For the reverse implication, if the image is the full product, every pair (1,σ2) is compatible, so every σ2∈Gal⁡(E2/F) fixes D; its fixed field is F, hence D=F. If E1=E2, the fibre product is instead the diagonal subgroup, as the formula requires.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Galois group of a separable polynomial

Definition

Let 0≠f∈F[x] be separable, and let L/F be a splitting field of f (Polynomials that split and splitting fields of a polynomial or a family of polynomials). By Equivalent characterizations of a finite Galois extension, the extension L/F is finite Galois. The Galois group of f over F is

Gf:=Gal⁡(L/F).

An ordering of the roots identifies Gf with a permutation group. A different ordering conjugates that subgroup in the corresponding symmetric group. Isomorphisms between splitting fields exist by A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials and conjugate their automorphism groups. Thus the abstract group, and its root action up to relabelling, do not depend on the chosen splitting field.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A polynomial Galois group acts faithfully on its roots

Statement

Let 0≠f∈F[x] be separable, let L be its splitting field, and let X be its set of roots in L. The natural action of Gf=Gal⁡(L/F) on X is faithful, so it embeds Gf in the symmetric group Sym⁡(X). After ordering X, this gives a subgroup of Sn; changing the ordering conjugates the subgroup.

Facts & Assumptions

Given: The polynomial Galois group of The Galois group of a separable polynomial and the fact that a splitting field is generated over F by its roots (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

[L1]

Every field homomorphism τ:L→L fixing F maps the finite set of distinct roots of f bijectively to itself (Every F-endomorphism of a splitting field permutes the distinct roots and is an automorphism).

Proof

technique · direct
1.1L1

By [L1], each element of Gf gives a permutation of X, and composition of automorphisms gives composition of permutations.

2.1step 1.1given

If an automorphism induces the identity permutation, it fixes every root of f and fixes F; because those roots generate L, it fixes all of L. Thus the action homomorphism has trivial kernel and is faithful. For a nonzero constant polynomial, X is empty, L=F, and both groups are trivial; a linear polynomial gives the singleton case.

3.1step 2.1algebra∎

If two orderings of X differ by π∈Sn, then the two permutation representatives of every σ∈Gf are related by ρ′(σ)=πρ(σ)π−1. Hence the embedded subgroup changes only by conjugation.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A positive-degree separable polynomial is irreducible exactly when its Galois group is transitive on the roots

Statement

A positive-degree separable polynomial is irreducible if and only if its Galois group acts transitively on its roots.

Facts & Assumptions

Given: A positive-degree separable polynomial f∈F[x], its splitting field L, and the faithful root action of A polynomial Galois group acts faithfully on its roots; the minimal-polynomial correspondence for a simple algebraic extension (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

[L1]

An isomorphism between base fields taking one polynomial to another extends to an isomorphism between their splitting fields (A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials).

Proof

technique · direct
1.1L1givenchoose

For the forward direction, suppose f is irreducible and let α,β be roots. The rule sending α to β gives an F-isomorphism F(α)→F(β) because both have minimal polynomial associated to f; by [L1] it extends to an F-automorphism of L. Thus some Galois element sends any chosen root to any other, so the action is transitive. This includes degree one.

2.1givenalgebra∎

For the reverse direction, suppose the action is transitive and let g be a monic irreducible factor of f containing one root α. For every σ∈Gf, the coefficients of g are fixed, so g(σα)=σ(g(α))=0. Transitivity puts every root of f among the roots of g; since f is separable, g has the full degree of f, so f is a scalar multiple of g and is irreducible. A root equal to zero causes no exception.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The Vandermonde product transforms by the sign of the root permutation

Statement

Let f∈F[x] be separable of degree n, order its roots as α1,…,αn, and put

δ:=∏1≤i<j≤n(αi−αj).

For σ in the Galois group, let the same symbol denote its induced root permutation. Then σ(δ)=sgn⁡(σ)δ for the Vandermonde product of an ordered root list. Consequently δ2 is fixed by the Galois group.

Facts & Assumptions

[F1]

The sign of σ is the integer sgn⁡(σ):=(−1)inv⁡(σ)∈{+1,−1}, where inv⁡(σ) counts the pairs i<j with σ(i)>σ(j) (Inversions, inversion number, the sign sgn⁡(σ)=(−1)inv⁡(σ), and even and odd permutations).

[L1]

For every natural n, the function sgn⁡:Sn→{+1,−1} is a group homomorphism (The sign is a homomorphism Sn→{+1,−1}, surjective exactly when n≥2).

[L2]

Every permutation of a finite set is a product of transpositions, and the identity is represented by the empty product (Every finite permutation is a product of transpositions, so the transpositions generate Sn).

[L3]

If σ=τ1⋯τr is any factorisation of a finite permutation into transpositions, then (−1)r=(−1)inv⁡(σ) (Every transposition factorisation of σ has parity (−1)inv⁡(σ)).

Proof

technique · direct
1.1algebra

Swapping two entries of the ordered root list reverses the factor belonging to that pair, while the remaining affected factors exchange in pairs; hence a transposition multiplies δ by −1.

1.2F1L3

Taking the one-factor factorisation τ=τ in [L3] gives (−1)inv⁡(τ)=−1, so sgn⁡(τ)=−1 for every transposition τ by [F1].

2.1step 1.1L2

By [L2] write σ=τ1⋯τr as a product of transpositions, and apply step 1.1 once for each factor: each application multiplies the current Vandermonde product by −1, so σ(δ)=(−1)rδ.

3.1step 2.1step 1.2L1L2

By [L1] and step 1.2, sgn⁡(σ)=sgn⁡(τ1)⋯sgn⁡(τr)=(−1)r, so step 2.1 gives σ(δ)=sgn⁡(σ)δ. For n=0 or n=1 the factorisation is empty by [L2], the product defining δ is likewise empty and equals 1, and the sign is 1, so the identity holds there as 1=1.

4.1step 3.1algebra∎

Squaring the identity of step 3.1 removes the sign, so σ(δ2)=δ2 for every σ. A root equal to zero creates no exception; separability ensures distinct roots and hence δ≠0.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

For a monic separable polynomial in characteristic not two, the Galois group lies in An exactly when the discriminant is a square

Statement

Let f∈F[x] be a monic separable polynomial of degree n, where char⁡F≠2. The Galois group lies in An exactly when the discriminant is a square in the base field.

Facts & Assumptions

Given: A splitting field L/F, an ordered root list, the discriminant definition of The discriminant of a monic polynomial as the coefficient expression of Δn2, the root formula Disc⁡(f)=δ2 and the fact that separability makes it nonzero (The discriminant is ∏i<j(αi−αj)2 and vanishes exactly when a monic polynomial has a repeated root), the definition An=ker⁡(sgn⁡) (The alternating group An=ker⁡(sgn⁡) of even permutations), and the finite Galois correspondence, which gives LGal⁡(L/F)=F (The fundamental theorem of finite Galois theory).

[L1]

For the Vandermonde product, σ(δ)=sgn⁡(σ)δ for every Galois automorphism (The Vandermonde product transforms by the sign of the root permutation).

Proof

technique · direct
1.1L1given

For the forward direction, suppose the Galois group lies in An. Then every sign is 1, so [L1] shows that every automorphism fixes δ. The fixed field is F, hence δ∈F and Disc⁡(f)=δ2 is a square in F. This also covers n=0 and n=1, when δ=1.

2.1L1givenalgebra∎

For the reverse direction, suppose Disc⁡(f)=d2 for some d∈F. Since δ2=d2, the field law gives δ=d or δ=−d, so δ∈F. Thus every automorphism fixes δ, and [L1] gives sgn⁡(σ)δ=δ. Separability gives δ≠0, so cancellation and 1≠−1 in characteristic not two force sgn⁡(σ)=1. Therefore every Galois permutation lies in An.

Remarks

The characteristic hypothesis is essential to this argument: in characteristic two the two signs have the same scalar action, so the Vandermonde equation cannot detect parity.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

A monic irreducible separable cubic in characteristic not two has Galois group A3 or S3 according to its discriminant

Statement

Let f∈F[x] be a monic irreducible separable cubic over a field of characteristic not two. Then its Galois group is A3 when its discriminant is a square and S3 when its discriminant is not a square.

Facts & Assumptions

[L1]

A positive-degree separable polynomial is irreducible if and only if its Galois group acts transitively on its roots (A positive-degree separable polynomial is irreducible exactly when its Galois group is transitive on the roots).

[L2]

For a monic separable polynomial in characteristic not two, the Galois group lies in An exactly when the discriminant is a square in the base field (For a monic separable polynomial in characteristic not two, the Galois group lies in An exactly when the discriminant is a square).

Proof

technique · direct
1.1L1givenalgebra

By [L1], the Galois group G≤S3 acts transitively on three roots. Orbit-stabilizer makes 3 divide ∣G∣, while Lagrange makes ∣G∣ divide 6; hence ∣G∣ is 3 or 6. In the first case every nonidentity element is a three-cycle and G=A3, while in the second G=S3.

2.1step 1.1L2∎

If the discriminant is a square, [L2] gives G≤A3, so step 1.1 forces G=A3. If it is not a square, [L2] gives G≰A3, so step 1.1 forces G=S3. The two square classes are exhaustive, and separability remains an explicit hypothesis in characteristic three.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The resolvent cubic of a monic quartic

Definition

Let

f(x)=x4+ax3+bx2+cx+d∈F[x]

be monic, and let α1,α2,α3,α4 be its roots in a splitting field (Polynomials that split and splitting fields of a polynomial or a family of polynomials). Put

β1=α1α2+α3α4,β2=α1α3+α2α4,β3=α1α4+α2α3.

The resolvent cubic of f is

Rf(y):=(y−β1)(y−β2)(y−β3).

Permuting the four roots permutes the set of pairings, so the coefficients are symmetric expressions in the roots and lie in F by A symmetric polynomial in the roots of a monic polynomial is a polynomial in its coefficients and lies in the base ring. The explicit coefficient formula and its discriminant identity are proved in The coefficient formula and discriminant of the quartic resolvent ↗.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The coefficient formula and discriminant of the quartic resolvent

Statement

For

f(x)=x4+ax3+bx2+cx+d,

the resolvent of The resolvent cubic of a monic quartic is

Rf(y)=y3−by2+(ac−4d)y−(a2d+c2−4bd).

A monic quartic and its resolvent cubic have the same discriminant.

Facts & Assumptions

Given: Four roots α1,…,α4 in a splitting field, their elementary symmetric functions e1=−a, e2=b, e3=−c, e4=d, and the discriminant convention of The discriminant of a monic polynomial as the coefficient expression of Δn2.

[L1]

Every symmetric polynomial has a unique expression Q(e1,…,en) (Fundamental theorem of symmetric polynomials: unique expression as a polynomial in e1,…,en).

Proof

technique · direct
1.1L1algebra

For the three pairing roots β1,β2,β3, direct expansion gives β1+β2+β3=e2=b, β1β2+β1β3+β2β3=e1e3−4e4=ac−4d, and β1β2β3=e12e4+e32−4e2e4=a2d+c2−4bd. These are symmetric identities licensed by [L1], and substitution in ∏i(y−βi) gives the displayed formula.

1.2algebra

The differences factor as β1−β2=(α2−α3)(α1−α4), β1−β3=(α2−α4)(α1−α3), and β2−β3=(α3−α4)(α1−α2).

2.1step 1.2algebra∎

Multiplying the squares of the three identities in step 1.2 uses each of the six differences αi−αj exactly once. The root-product formulas for the two discriminants therefore give Disc⁡(Rf)=Disc⁡(f). The identity remains valid when coefficients or root differences vanish.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The transitive subgroups of S4 and their action on the three pairings

Statement

Up to conjugacy, the transitive subgroups of S4 are S4,A4,D4,C4, and V4, with the stated action on the three pairings. If

V4={1,(12)(34),(13)(24),(14)(23)},

then the action on the three partitions of {1,2,3,4} into two unordered pairs has kernel V4. The corresponding data are:

H∣H∩V4∣image on pairingsH≤A4
S44S3no
A44A3yes
D44C2no
C42C2no
V44trivialyes

Facts & Assumptions

Proof

technique · direct
1.1algebra

Acting on the explicitly listed pairings gives a homomorphism θ:S4→S3. A permutation fixes all three pairings exactly when it is the identity or one of the three double transpositions, so ker⁡θ=V4.

2.1step 1.1given

If H≤S4 is transitive on four symbols, orbit-stabilizer makes 4 divide ∣H∣ and Lagrange makes ∣H∣ divide 24, so ∣H∣∈{4,8,12,24}. Order 24 gives S4. An order-12 subgroup has index two and is normal; if it contained an odd permutation, the conjugates of that transposition or four-cycle would generate S4, so it is A4. An order-8 subgroup is Sylow and hence conjugate to the standard D4. For order 4 the action is regular; an element of order four gives C4, and otherwise all nonidentity elements have order two and give V4.

3.1step 1.1step 2.1L1algebra∎

Intersecting representatives with the kernel in step 1.1 gives the second column of the table, and the quotient orders give the pairing images. By [L1], S4,D4,C4 contain odd permutations, whereas A4 and V4 do not. These invariants give the displayed rows; only D4 and C4 share the same nontrivial intransitive pairing image, and their different kernel orders distinguish them.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The five-case resolvent classification of an irreducible quartic Galois group

Statement

Let f∈F[x] be a monic irreducible separable quartic over a field of characteristic not two, let Rf be its resolvent cubic, let M be the splitting field of Rf, and let Δ=Disc⁡(f). Exactly one row applies:

  1. An irreducible separable quartic with irreducible resolvent and nonsquare discriminant has Galois group S4.
  2. An irreducible separable quartic with irreducible resolvent and square discriminant has Galois group A4.
  3. If Rf splits completely over F, then the group is V4.
  4. If Rf has exactly one root in F and f remains irreducible over M, then the group is D4.
  5. If Rf has exactly one root in F and f is reducible over M, then the group is C4.

In the unique-root resolvent branch, irreducibility over the resolvent splitting field distinguishes D4 from C4.

Facts & Assumptions

[L1]

The transitive subgroups of S4 are S4,A4,D4,C4, and V4, with the stated action on the three pairings (The transitive subgroups of S4 and their action on the three pairings).

[L2]

A monic quartic and its resolvent cubic have the same discriminant (The coefficient formula and discriminant of the quartic resolvent).

Proof

technique · direct
1.1L1given

Let L be the splitting field of f and G=Gal⁡(L/F)≤S4. Irreducibility makes G transitive. The kernel of its action on the three pairing roots is G∩V4 by [L1]. The field generated by those roots is M, so the Galois correspondence identifies M=LG∩V4.

2.1step 1.1L1L2given

If Rf is irreducible, its pairing action is transitive, so [L1] leaves S4 or A4; by [L2] and the discriminant criterion, nonsquare Δ gives S4 and square Δ gives A4. If Rf splits completely, the pairing action is trivial and transitivity on four roots forces G=V4. If Rf has exactly one root in F, its other two roots form one orbit, so the pairing image is C2 and [L1] leaves D4 or C4. A cubic cannot have exactly two roots in F, and [L2] plus separability makes the resolvent separable, so these branches are exhaustive.

3.1step 2.1L1given∎

In the unique-root branch, Gal⁡(L/M)=G∩V4. For G=D4 this intersection is V4, which acts transitively on the four roots, so f remains irreducible over M. For G=C4 the intersection has order two and two root orbits, so f factors over M. The transitivity criterion proves both implications and completes the five-case classification.

5 · Examples, counterexamples and false statements

None yet.

Sources