This file exposes the chosen singleton-radical construction used in Kummer theory. For b : Kˣ, it chooses an embedded field K(ⁿ√b) inside the separable closure and proves that, when K contains the n-th roots of unity, this is a finite cyclic Galois extension.
A chosen n-th root of b in the separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def chosenSimpleKummerRoot
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
SeparableClosure KThe chosen root belongs to the maximal Kummer root set.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRoot_mem
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
chosenSimpleKummerRoot K n hnK b ∈
kummerRootSet (K := K) (Omega := SeparableClosure K) n
(maximalKummerSubgroup K n).1The chosen element is an actual n-th root of b.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRoot_pow
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
chosenSimpleKummerRoot K n hnK b ^ (n : ℕ) =
algebraMap K (SeparableClosure K) (b : K)The simple Kummer extension generated by the chosen root of b.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def chosenSimpleKummerExtension
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
IntermediateField K (SeparableClosure K)The simple extension generated by one chosen radical is contained in the extension generated by all radicals of the maximal Kummer subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_le_maximalKummerExtension
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
chosenSimpleKummerExtension K n hnK b ≤
kummerRadicalExtension
(K := K) (Omega := SeparableClosure K) n
(maximalKummerSubgroup K n).1The chosen radical as a unit of K(ⁿ√b).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def chosenSimpleKummerRootUnit
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
(chosenSimpleKummerExtension K n hnK b)ˣThe radical still has n-th power b in the simple extension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRootUnit_pow
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
chosenSimpleKummerRootUnit K n hnK b ^ (n : ℕ) =
Units.map
(algebraMap K (chosenSimpleKummerExtension K n hnK b)).toMonoidHom bThe chosen radical generates the whole simple extension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_adjoin_root_eq_top
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
let E := chosenSimpleKummerExtension K n hnK b
IntermediateField.adjoin K
{((chosenSimpleKummerRootUnit K n hnK b : Eˣ) : E)} = ⊤ := by
let E := chosenSimpleKummerExtension K n hnK b
let beta : E := (chosenSimpleKummerRootUnit K n hnK b : Eˣ)
let R : IntermediateField K E :=
IntermediateField.adjoin K {beta}
change R = ⊤
apply top_unique
intro x _
have hall : ∀ y : SeparableClosure K, ∀ hy : y ∈ E,
(⟨y, hy⟩ : E) ∈ R := by
intro y hy
change y ∈ IntermediateField.adjoin K
{chosenSimpleKummerRoot K n hnK b} at hy
induction hy using IntermediateField.adjoin_induction with
| mem y hy =>
have hy' : y = chosenSimpleKummerRoot K n hnK b :=
Set.mem_singleton_iff.mp hy
subst y
apply IntermediateField.subset_adjoin K
rw [Set.mem_singleton_iff]
apply Subtype.ext
rfl
| algebraMap a => exact R.algebraMap_mem a
| add x y hx hy ihx ihy => exact R.add_mem ihx ihy
| inv x hx ihx => exact R.inv_mem ihx
| mul x y hx hy ihx ihy => exact R.mul_mem ihx ihy
exact hall x.1 x.propertyThe extension generated by the chosen simple Kummer root is finite-dimensional.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_finiteDimensional
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ) :
FiniteDimensional K (chosenSimpleKummerExtension K n hnK b)If K contains μₙ, then K(ⁿ√b) / K is abelian Galois.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_isAbelianGalois
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
IsAbelianGalois K (chosenSimpleKummerExtension K n hnK b)Every Galois root quotient of the chosen radical is an n-th root of unity.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummer_rootQuotient_mem
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ)
(sigma : Gal((chosenSimpleKummerExtension K n hnK b)/K)) :
rootQuotient
(K := K) (L := chosenSimpleKummerExtension K n hnK b)
(chosenSimpleKummerRootUnit K n hnK b) sigma ∈
nthRootsSubgroup (chosenSimpleKummerExtension K n hnK b) (n : ℕ)The root quotient of the chosen radical is a character of the Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]def chosenSimpleKummerRootCharacter
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
Gal((chosenSimpleKummerExtension K n hnK b)/K) →*
nthRootsSubgroup (chosenSimpleKummerExtension K n hnK b) (n : ℕ)The character attached to the chosen Kummer root agrees with the root quotient of the chosen generator.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRootCharacter_apply
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ)
(sigma : Gal((chosenSimpleKummerExtension K n hnK b)/K)) :
chosenSimpleKummerRootCharacter K n hnK hmu b sigma =
⟨rootQuotient
(K := K) (L := chosenSimpleKummerExtension K n hnK b)
(chosenSimpleKummerRootUnit K n hnK b) sigma,
chosenSimpleKummer_rootQuotient_mem K n hnK b sigma⟩A Galois automorphism fixes the chosen radical exactly when it is the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRootQuotient_eq_one_iff
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0) (b : Kˣ)
(sigma : Gal((chosenSimpleKummerExtension K n hnK b)/K)) :
rootQuotient
(K := K) (L := chosenSimpleKummerExtension K n hnK b)
(chosenSimpleKummerRootUnit K n hnK b) sigma = 1 ↔
sigma = 1Evaluation on the generating radical separates all automorphisms.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerRootCharacter_injective
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
Function.Injective
(chosenSimpleKummerRootCharacter K n hnK hmu b)The Galois group of a simple Kummer extension is cyclic.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_isCyclic
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ) :
IsCyclic Gal((chosenSimpleKummerExtension K n hnK b)/K)Every automorphism of a simple Kummer extension has exponent dividing n.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
variable (K : Type) [Field K]theorem chosenSimpleKummerExtension_galois_pow_eq_one
(n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
(hmu : (primitiveRoots (n : ℕ) K).Nonempty) (b : Kˣ)
(sigma : Gal((chosenSimpleKummerExtension K n hnK b)/K)) :
sigma ^ (n : ℕ) = 1