Let L/K be a finite abelian Galois extension whose Galois group is killed by n, and suppose that K contains a primitive n-th root of unity. This file proves that L is generated over K by all nonzero beta : L such that beta ^ n belongs to K.
The proof uses finite-abelian character separation and the finite Kummer character isomorphism. It is the finite n-th-power, actual-field form of the Kummer generation theorem; it is not the general abstract-module or infinite statement.
All nonzero elements of L whose n-th power comes from K.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
section FiniteKummerGeneration
variable {K L : Type*} [Field K] [Field L] [Algebra K L]def finiteKummerRootSet (n : ℕ+) : Set LA primitive n-th root in K implies the field-level hypothesis that all n-th roots of unity occurring in L come from K.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
section FiniteKummerGeneration
variable {K L : Type*} [Field K] [Field L] [Algebra K L]theorem nthRootsOfUnityInBase_of_primitiveRoots
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
NthRootsOfUnityInBase (K := K) (L := L) nFinite actual-field version of The Kummer generation theorem.
An abelian Galois extension of exponent dividing n, over a field containing the n-th roots of unity, is generated by the elements whose n-th powers belong to the base field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open scoped IsMulCommutative
section FiniteKummerGeneration
variable {K L : Type*} [Field K] [Field L] [Algebra K L]theorem finiteKummerRootSet_adjoin_eq_top
[FiniteDimensional K L] [IsGalois K L] [IsMulCommutative Gal(L/K)]
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
(hexponent : ∀ sigma : Gal(L/K), sigma ^ (n : ℕ) = 1) :
IntermediateField.adjoin K (finiteKummerRootSet (K := K) (L := L) n) = ⊤