NYLL
Module

RadicalExtension.lean

Nyll.GaloisCohomology.Kummer.Concrete.RadicalExtension
19 declarations indexed from sourceView source ↗

Module documentation

the radical-extension construction

Let Delta be a subgroup of Kˣ. Inside a fixed separable closure Omega/K, we adjoin all roots beta of the equations beta ^ n = a, for a ∈ Delta. Using all roots makes the construction independent of choices and visibly stable under Gal(Omega/K).

The hypothesis (n : K) ≠ 0 is the usual assumption that n is prime to the characteristic. It is used exactly to make X ^ n - a separable. The primitive-root hypothesis is used later to make the resulting Galois group abelian of exponent dividing n.

Imports3
Imported by4

Declarations

def

unitNthPowersSubgroup

L38 ↗
KummerTheory.unitNthPowersSubgroup
Documentation

The subgroup Kˣ^n of n-th powers in the unit group.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def unitNthPowersSubgroup (K : Type*) [Field K] (n : ℕ+) : Subgroup Kˣ
theorem

mem_unitNthPowersSubgroup_iff

L42 ↗
KummerTheory.mem_unitNthPowersSubgroup_iff
Documentation

A unit lies in the unit power subgroup exactly when it is an nth power of a unit.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem mem_unitNthPowersSubgroup_iff
    (n : ℕ+) {a : Kˣ} :
    a ∈ unitNthPowersSubgroup K n ↔ ∃ b : Kˣ, b ^ (n : ℕ) = a
def

KummerSubgroup

L49 ↗
KummerTheory.KummerSubgroup
Documentation

The subgroup-side objects in the Kummer correspondence: subgroups Delta ≤ Kˣ containing Kˣ^n.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def KummerSubgroup (K : Type*) [Field K] (n : ℕ+)
def

kummerRootSet

L53 ↗
KummerTheory.kummerRootSet
Documentation

All roots in Omega of the Kummer equations belonging to Delta.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def kummerRootSet (n : ℕ+) (Delta : Subgroup Kˣ) : Set Omega
def

kummerRadicalExtension

L58 ↗
KummerTheory.kummerRadicalExtension
Documentation

The field K(√[n]{Delta}) inside the chosen separable closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
def kummerRadicalExtension (n : ℕ+) (Delta : Subgroup Kˣ) :
    IntermediateField K Omega
theorem

exists_kummerRootSet

L64 ↗
KummerTheory.exists_kummerRootSet
Documentation

Every prescribed Kummer equation has a root in the separable closure. This is the only point where the characteristic hypothesis is needed.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem exists_kummerRootSet
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0) (Delta : Subgroup Kˣ) (a : Delta) :
    ∃ beta : Omega,
      beta ∈ kummerRootSet (K := K) (Omega := Omega) n Delta ∧
        beta ^ (n : ℕ) = algebraMap K Omega (a.1 : K)
theorem

le_finiteKummerRadicalSubgroup_kummerRadicalExtension

L89 ↗
KummerTheory.le_finiteKummerRadicalSubgroup_kummerRadicalExtension
Documentation

Every element of Delta acquires an n-th root in the constructed field. This is the elementary inclusion Delta ≤ Delta_{K(√[n]{Delta})} in the Kummer correspondence.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem le_finiteKummerRadicalSubgroup_kummerRadicalExtension
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0) (Delta : Subgroup Kˣ) :
    Delta ≤ finiteKummerRadicalSubgroup
      (K := K) (L := kummerRadicalExtension (K := K) (Omega := Omega) n Delta) n
theorem

unitNthPowersSubgroup_le_constructedRadical

L115 ↗
KummerTheory.unitNthPowersSubgroup_le_constructedRadical
Documentation

In particular, for an admissible subgroup-side object, the radical subgroup recovered from its field still contains Kˣ^n.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem unitNthPowersSubgroup_le_constructedRadical
    [IsSepClosure K Omega]
    (n : ℕ+) (hn : ((n : ℕ) : K) ≠ 0) (Delta : KummerSubgroup K n) :
    unitNthPowersSubgroup K n ≤ finiteKummerRadicalSubgroup
      (K := K)
      (L := kummerRadicalExtension (K := K) (Omega := Omega) n Delta.1) n
theorem

kummerRootSet_ne_zero

L125 ↗
KummerTheory.kummerRootSet_ne_zero
Documentation

A Kummer root is nonzero because its prescribed power is a unit.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRootSet_ne_zero
    (n : ℕ+) (Delta : Subgroup Kˣ) {beta : Omega}
    (hbeta : beta ∈ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    beta ≠ 0
theorem

kummerRootSet_mapsTo

L137 ↗
KummerTheory.kummerRootSet_mapsTo
Documentation

Every K-automorphism of the separable closure preserves the full root set.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRootSet_mapsTo
    (n : ℕ+) (Delta : Subgroup Kˣ) (sigma : Gal(Omega/K)) :
    Set.MapsTo sigma
      (kummerRootSet (K := K) (Omega := Omega) n Delta)
      (kummerRootSet (K := K) (Omega := Omega) n Delta)
theorem

kummerRootSet_image

L152 ↗
KummerTheory.kummerRootSet_image
Documentation

Because inverse automorphisms preserve the same equations, the root set is carried onto itself, not merely into itself.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRootSet_image
    (n : ℕ+) (Delta : Subgroup Kˣ) (sigma : Gal(Omega/K)) :
    sigma '' kummerRootSet (K := K) (Omega := Omega) n Delta =
      kummerRootSet (K := K) (Omega := Omega) n Delta
theorem

kummerRadicalExtension_map

L165 ↗
KummerTheory.kummerRadicalExtension_map
Documentation

The actual radical field is stable under every automorphism of the separable closure.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_map
    (n : ℕ+) (Delta : Subgroup Kˣ) (sigma : Gal(Omega/K)) :
    (kummerRadicalExtension (K := K) (Omega := Omega) n Delta).map sigma =
      kummerRadicalExtension (K := K) (Omega := Omega) n Delta
theorem

kummerRadicalExtension_normal

L174 ↗
KummerTheory.kummerRadicalExtension_normal
Documentation

The stability just proved is precisely normality over K.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_normal
    [IsSepClosure K Omega]
    (n : ℕ+) (Delta : Subgroup Kˣ) :
    Normal K (kummerRadicalExtension (K := K) (Omega := Omega) n Delta)
theorem

kummerRadicalExtension_isGalois

L184 ↗
KummerTheory.kummerRadicalExtension_isGalois
Documentation

The extension K(√[n]{Delta})/K is Galois. Separability comes from the ambient separable closure and normality from invariance of the full root set.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_isGalois
    [IsSepClosure K Omega]
    (n : ℕ+) (Delta : Subgroup Kˣ) :
    IsGalois K (kummerRadicalExtension (K := K) (Omega := Omega) n Delta)
theorem

kummerRadicalExtension_generator_commute

L194 ↗
KummerTheory.kummerRadicalExtension_generator_commute
Documentation

On every radical generator, two automorphisms commute. The quotient sigma(beta) / beta is an n-th root of unity, hence lies in and is fixed by the base field under the primitive-root hypothesis.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_generator_commute
    [IsSepClosure K Omega]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : Subgroup Kˣ)
    (sigma tau : Gal(kummerRadicalExtension (K := K) (Omega := Omega) n Delta/K))
    {beta : Omega}
    (hbeta : beta ∈ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    (sigma * tau)
        ⟨beta, IntermediateField.subset_adjoin K
          (kummerRootSet (K := K) (Omega := Omega) n Delta) hbeta⟩ =
      (tau * sigma)
        ⟨beta, IntermediateField.subset_adjoin K
          (kummerRootSet (K := K) (Omega := Omega) n Delta) hbeta⟩
theorem

kummerRadicalExtension_isMulCommutative

L248 ↗
KummerTheory.kummerRadicalExtension_isMulCommutative
Documentation

Hence Gal(K(√[n]{Delta})/K) is commutative. Equality is checked on the radical generators of the adjoin.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_isMulCommutative
    [IsSepClosure K Omega]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : Subgroup Kˣ) :
    IsMulCommutative Gal(kummerRadicalExtension (K := K) (Omega := Omega) n Delta/K)
theorem

kummerRadicalExtension_generator_pow_eq_one

L261 ↗
KummerTheory.kummerRadicalExtension_generator_pow_eq_one
Documentation

On every radical generator, the n-th power of an automorphism is the identity.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_generator_pow_eq_one
    [IsSepClosure K Omega]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : Subgroup Kˣ)
    (sigma : Gal(kummerRadicalExtension (K := K) (Omega := Omega) n Delta/K))
    {beta : Omega}
    (hbeta : beta ∈ kummerRootSet (K := K) (Omega := Omega) n Delta) :
    (sigma ^ (n : ℕ))
        ⟨beta, IntermediateField.subset_adjoin K
          (kummerRootSet (K := K) (Omega := Omega) n Delta) hbeta⟩ =
      ⟨beta, IntermediateField.subset_adjoin K
        (kummerRootSet (K := K) (Omega := Omega) n Delta) hbeta⟩
theorem

kummerRadicalExtension_galois_pow_eq_one

L316 ↗
KummerTheory.kummerRadicalExtension_galois_pow_eq_one
Documentation

Every element of the Galois group has n-th power one.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem kummerRadicalExtension_galois_pow_eq_one
    [IsSepClosure K Omega]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : Subgroup Kˣ)
    (sigma : Gal(kummerRadicalExtension (K := K) (Omega := Omega) n Delta/K)) :
    sigma ^ (n : ℕ) = 1
theorem

kummerRadicalExtension_isAbelianGalois

L329 ↗
KummerTheory.kummerRadicalExtension_isAbelianGalois
Documentation

the Kummer correspondence, forward construction: adjoining the radicals attached to Delta produces an abelian Galois extension.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace KummerTheory
section RadicalExtension
open Polynomial
variable {K Omega : Type*} [Field K] [Field Omega] [Algebra K Omega]
Lean source · full declaration
theorem kummerRadicalExtension_isAbelianGalois
    [IsSepClosure K Omega]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (Delta : Subgroup Kˣ) :
    IsAbelianGalois K
      (kummerRadicalExtension (K := K) (Omega := Omega) n Delta) where
  toIsGalois := kummerRadicalExtension_isGalois n Delta
  toIsMulCommutative := kummerRadicalExtension_isMulCommutative n hmu Delta

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.