Galois theory

Galois theory relates a field extension to its group of automorphisms, covering the Galois correspondence, infinite Galois groups, Hilbert's theorem 90, solvability by radicals and essential dimension.

• Additive Hilbert's theorem 90
• Essential dimension of symmetric groups
• Galois extensions of the real numbers
• Gauss–Wantzel theorem on constructible polygons
• Solvability by radicals

TheoremExtensions of prime degree with a nontrivial automorphism are Galois#✓fully proved

In an extension of prime degree, a nontrivial automorphism witnesses that the extension is Galois, has order equal to the degree, and generates the automorphism group.

theorem AlgEquiv.isGalois_and_orderOf_eq_finrank_of_finrank_prime_of_ne_one
    (K L : Type*) [Field K] [Field L] [Algebra K L]
    (hdeg : (Module.finrank K L).Prime) (σ : L ≃ₐ[K] L) (hσ : σ ≠ 1) :
    IsGalois K L ∧ orderOf σ = Module.finrank K L ∧ Subgroup.zpowers σ = ⊤

TheoremIntermediate fields of an abelian extension form a modular lattice#✓fully proved

If \(L/K\) is a finite-dimensional abelian Galois extension, then the lattice of intermediate fields of \(L/K\) is modular.

The proof transports the modular lattice of subgroups of the commutative Galois group across the Galois correspondence.

theorem isModularLattice_intermediateField :
    IsModularLattice (IntermediateField K L)

Used by 1

Used byA field strictly above one cyclotomic subfield meets the other

TheoremNorm in a tensor product with a Galois extension#✓fully proved

For a Galois extension M / F and any F-algebra R, the norm of an element of R ⊗[F] M over R is the product of its Galois conjugates.

theorem algebraMap_norm_eq_prod_map_algEquiv
    (F M : Type*) [Field F] [Field M] [Algebra F M] [FiniteDimensional F M] [IsGalois F M]
    (R : Type*) [CommRing R] [Algebra F R] (z : R ⊗[F] M) :
    algebraMap R (R ⊗[F] M) (Algebra.norm R z) =
      ∏ g : M ≃ₐ[F] M, Algebra.TensorProduct.map (AlgHom.id F R) (g : M →ₐ[F] M) z

TheoremThe closure of a Galois subgroup is the fixing group of its fixed field#✓fully proved

Let \(K/k\) be a Galois extension, not necessarily finite, and give \(\operatorname{Gal}(K/k)\) the Krull topology. For every subgroup \(H\) of \(\operatorname{Gal}(K/k)\) with fixed field \(K^H\), the closure of \(H\) equals the subgroup of \(\operatorname{Gal}(K/k)\) consisting of the automorphisms that fix \(K^H\) pointwise.

theorem topologicalClosure_eq_fixingSubgroup_fixedField [IsGalois k K]
    (H : Subgroup Gal(K/k)) :
    H.topologicalClosure = (IntermediateField.fixedField H).fixingSubgroup

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.