The normal basis theorem #
We prove the normal basis theorem IsGalois.normalBasis:
every finite Galois extension has a basis that is an orbit under the Galois group action.
The proof follows [Cona] Keith Conrad, Linear Independence of Characters.
theorem
exists_linearIndependent_algEquiv_apply
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
:
∃ (x : L), LinearIndependent K fun (σ : L ≃ₐ[K] L) => σ x
noncomputable def
IsGalois.normalBasis
(K : Type u_1)
(L : Type u_2)
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[IsGalois K L]
:
Module.Basis (L ≃ₐ[K] L) K L
Given a finite Galois extension L/K, normalBasis K L is a basis of L over K
that is an orbit under the Galois group action.
Equations
Instances For
theorem
IsGalois.normalBasis_apply
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[FiniteDimensional K L]
[IsGalois K L]
(e : L ≃ₐ[K] L)
: