Galois correspondence for a finite non-Galois extension

Proved

GaloisFundamental.non_galois_correspondence

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

field-theorygalois-theory

Let $E/F$ be a finite field extension that is not Galois, and let $G = \operatorname{Aut}(E/F)$ . Then:

the map $H \mapsto E^H$ from subgroups of $G$ to intermediate fields is injective but not surjective;
the map $K \mapsto \operatorname{Aut}(E/K)$ from intermediate fields to subgroups of $G$ is surjective but not injective;
$F$ is not the fixed field of any subgroup of $G$ : $E^H \ne F$ for every $H \le G$ .

Preamble

import Mathlib

Formal statement

namespace GaloisFundamental

theorem non_galois_correspondence (F E : Type*) [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] (hE : ¬ IsGalois F E) :
    Function.Injective (fun H : Subgroup (E ≃ₐ[F] E) => IntermediateField.fixedField H) ∧
      ¬ Function.Surjective (fun H : Subgroup (E ≃ₐ[F] E) => IntermediateField.fixedField H) ∧
      Function.Surjective (fun K : IntermediateField F E => K.fixingSubgroup) ∧
      ¬ Function.Injective (fun K : IntermediateField F E => K.fixingSubgroup) ∧
      ∀ H : Subgroup (E ≃ₐ[F] E), IntermediateField.fixedField H ≠ ⊥ := by sorry

end GaloisFundamental

Source

Wikipedia, "Fundamental theorem of Galois theory", revision oldid=1345286594, https://en.wikipedia.org/w/index.php?title=Fundamental_theorem_of_Galois_theory&oldid=1345286594, section "Explicit description of the correspondence", last paragraph ("If E/F is not Galois, then the correspondence gives only an injective (but not surjective) map ... In particular, if E/F is not Galois, then F is not the fixed field of any subgroup")

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, with full knowledge of the source and of the intended meaning. It is not the blind, independent auditor read-back the platform recommends, and no reviewer should treat it as independent evidence of faithfulness. Please compare the Lean code against the source yourself (or regenerate this read-back with an independent auditor) before confirming this item.

What is fixed. Arbitrary fields $F$ , $E$ with $E$ an $F$ -algebra (a field extension $E/F$ ) that is finite-dimensional over $F$ , together with the hypothesis that $E/F$ is not Galois, i.e. it fails to be both separable and normal.

Notation. $G$ = group of $F$ -algebra automorphisms of $E$ ; $\mathcal S$ = set of all subgroups of $G$ ; $\mathcal I$ = set of all intermediate fields $F \subseteq K \subseteq E$ . $\Phi : \mathcal S \to \mathcal I$ , $\Phi(H) = E^H = \{x \in E : \sigma x = x\ \forall \sigma \in H\}$ . $\Psi : \mathcal I \to \mathcal S$ , $\Psi(K) = \{\sigma \in G : \sigma x = x\ \forall x \in K\}$ . $\bot$ denotes the smallest intermediate field, i.e. (the image of) $F$ itself.

Assertion. All five of the following hold:

$\Phi$ is injective;
$\Phi$ is not surjective (some intermediate field is not of the form $E^H$ );
$\Psi$ is surjective;
$\Psi$ is not injective (two distinct intermediate fields have the same fixing subgroup);
for every subgroup $H \le G$ , $E^H \ne \bot$ , i.e. $E^H \neq F$ .

The hypothesis "not Galois" is satisfiable (e.g. $\mathbb{Q}(\sqrt[3]{2})/\mathbb{Q}$ ), so the statement is not vacuous; it excludes the trivial extension $E = F$ , which is Galois.

Human review

Endorsed by Shuze Chen · Sep 28, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 28, 2026
Confirmed by the mission captain (proposal self-audit).

View graph