Module

IdealRadicalGoverningField.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealRadicalGoverningField

10 declarations indexed from sourceView source ↗

Module documentation

The ideal-radical governing field

For a number field F and a prime p, this file adjoins the p-th roots of the empty-support ideal radical after passing to F(μ_p). Kummer theory identifies the resulting finite abelian exponent-p Galois group with the character group of the restricted radical quotient.

Imports2

Imported by2

theorem

idealRadicalCyclotomicBase_isSepClosure

L31 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicBase_isSepClosure

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalCyclotomicBase_isSepClosure :
    IsSepClosure (IdealRadicalCyclotomicBase F p hp) (AlgebraicClosure F)

def

IdealRadicalGoverningField

L41 ↗

ClassFieldTower.Martinet.Shafarevich.IdealRadicalGoverningField

Documentation

The Kummer extension of F(μ_p) governed by the empty-support ideal p-power radical of F.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

def IdealRadicalGoverningField :
    IntermediateField (IdealRadicalCyclotomicBase F p hp)
      (AlgebraicClosure F)

theorem

idealRadicalGoverningField_isGalois

L50 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningField_isGalois

Documentation

The governing extension is Galois over the cyclotomic base.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalGoverningField_isGalois :
    IsGalois (IdealRadicalCyclotomicBase F p hp)
      (IdealRadicalGoverningField F p hp)

def

idealRadicalGoverningFieldCharacterDuality

L61 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningFieldCharacterDuality

Documentation

The canonical Kummer character duality for the ideal-radical governing extension.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

def idealRadicalGoverningFieldCharacterDuality :
    Gal(IdealRadicalGoverningField F p hp/
      IdealRadicalCyclotomicBase F p hp) ≃*
      (RestrictedRadicalQuotient (p.toPNat hp.pos)
          (idealRadicalCyclotomicKummerSubgroup F p hp) →*
        nthRootsSubgroup (IdealRadicalGoverningField F p hp) p)

theorem

finite_idealRadicalGoverningField_galois

L75 ↗

ClassFieldTower.Martinet.Shafarevich.finite_idealRadicalGoverningField_galois

Documentation

The Galois group of the governing extension is finite.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem finite_idealRadicalGoverningField_galois :
    Finite Gal(IdealRadicalGoverningField F p hp/
      IdealRadicalCyclotomicBase F p hp)

theorem

finiteDimensional_idealRadicalGoverningField

L93 ↗

ClassFieldTower.Martinet.Shafarevich.finiteDimensional_idealRadicalGoverningField

Documentation

The governing extension is finite-dimensional over F(μ_p).

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem finiteDimensional_idealRadicalGoverningField :
    FiniteDimensional (IdealRadicalCyclotomicBase F p hp)
      (IdealRadicalGoverningField F p hp)

theorem

idealRadicalGoverningField_isAbelianGalois

L110 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningField_isAbelianGalois

Documentation

The governing extension is abelian Galois over F(μ_p).

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalGoverningField_isAbelianGalois :
    IsAbelianGalois (IdealRadicalCyclotomicBase F p hp)
      (IdealRadicalGoverningField F p hp)

theorem

idealRadicalGoverningField_galois_pow_eq_one

L121 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalGoverningField_galois_pow_eq_one

Documentation

Every automorphism of the governing extension has exponent dividing p.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalGoverningField_galois_pow_eq_one
    (sigma :
      Gal(IdealRadicalGoverningField F p hp/IdealRadicalCyclotomicBase F p hp)) :
    sigma ^ p = 1

theorem

idealRadicalCyclotomicKummerSubgroup_le_governingRadical

L134 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicKummerSubgroup_le_governingRadical

Documentation

The chosen cyclotomic Kummer subgroup lies in the radical of its governing extension.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalCyclotomicKummerSubgroup_le_governingRadical :
    (idealRadicalCyclotomicKummerSubgroup F p hp).1 ≤
      finiteKummerRadicalSubgroup
        (K := IdealRadicalCyclotomicBase F p hp)
        (L := IdealRadicalGoverningField F p hp) (p.toPNat hp.pos)

theorem

idealRadicalToCyclotomicBase_mem_governingRadical

L147 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalToCyclotomicBase_mem_governingRadical

Documentation

In particular, every element of the base-field ideal radical maps into the Kummer radical of the governing extension.

Source context 7 commands

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

open scoped NumberField
namespace ClassFieldTower.Martinet.Shafarevich
open NumberField
open KummerTheory
noncomputable section
variable (F : Type*) [Field F] [NumberField F]
variable (p : ℕ) (hp : p.Prime)

Lean source · statement

theorem idealRadicalToCyclotomicBase_mem_governingRadical
    (a : (idealNthPowerRadicalKummerSubgroup F (p.toPNat hp.pos)).1) :
    idealRadicalToCyclotomicBase F p hp a ∈
      finiteKummerRadicalSubgroup
        (K := IdealRadicalCyclotomicBase F p hp)
        (L := IdealRadicalGoverningField F p hp) (p.toPNat hp.pos)

Module documentation

The ideal-radical governing field

Declarations