Existing in Mathlib · Algebra
Fundamental Theorem of Galois Theory — Finite Case
Between a base field F and a finite Galois extension E, every intermediate field determines the symmetries that fix it, and every subgroup of symmetries determines the elements it fixes. These operations recover the original field or subgroup and reverse containment.
- field extensions
- Galois groups
- intermediate fields
- fixed fields
- fixing subgroups
- order duality
Exact definition
Exact Mathlib definition
def IsGalois.intermediateFieldEquivSubgroup {F E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [IsGalois F E] : IntermediateField F E ≃o (Subgroup Gal(E/F))ᵒᵈThe theorem at a glance
Finite Galois correspondence at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Finite Galois correspondence at a glance
Detailed visual description
The poster places the finite Galois hypotheses above two mirrored lattices. It follows an intermediate field to its fixing subgroup and a subgroup to its fixed field, closes both inverse loops, and identifies the endpoint as a constructed order isomorphism.
Statement structure
From hypotheses to conclusion
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Finite Galois correspondence schematic
Detailed visual description
A lattice from F to E is mirrored by a lattice from the full Galois group to the trivial subgroup. Cross-connections pair each intermediate field with its fixing subgroup, while two closed return paths show that fixed-field and fixing-subgroup operations recover their inputs.
Why it matters
A mathematical landmark
The finite Galois correspondence turns questions about field extensions into questions about symmetry groups. Mathlib records the full correspondence as an order isomorphism to the dual subgroup order, rather than merely asserting that a bijection exists.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's constructed order isomorphism for a finite-dimensional Galois field extension. It matches all intermediate fields with all subgroups in reversed order; it does not cover non-Galois extensions, infinite Galois extensions, or assert that every intermediate extension is itself Galois.
- Proof Atlas did not originate the Galois correspondence or Mathlib's definition.
- The selected endpoint is a constructed OrderIso, not a proposition-valued existence theorem.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
IsGalois.intermediateFieldEquivSubgroupin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.fundamental-theorem-finite-galois-theory.v001