Module

IdealRadicalCyclotomicBase.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealRadicalCyclotomicBase

12 declarations indexed from sourceView source ↗

Module documentation

The ideal radical over a cyclotomic base

For a number field F and a prime p, this file chooses a primitive p-th root in AlgebraicClosure F, names F(μ_p), and maps the empty-support ideal p-power radical into an admissible Kummer subgroup over that cyclotomic base. Its restricted radical quotient is finite, by a source-proved surjection from the base-field ideal radical quotient.

Imports2

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.IdealPowerRadicalExact
Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed

Imported by6

def

idealRadicalPrimitiveRoot

L32 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalPrimitiveRoot

Documentation

A chosen primitive p-th root of unity in the fixed algebraic closure.

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 idealRadicalPrimitiveRoot : AlgebraicClosure F

theorem

idealRadicalPrimitiveRoot_isPrimitiveRoot

L37 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalPrimitiveRoot_isPrimitiveRoot

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 idealRadicalPrimitiveRoot_isPrimitiveRoot :
    IsPrimitiveRoot (idealRadicalPrimitiveRoot F p hp) p

def

IdealRadicalCyclotomicBase

L44 ↗

ClassFieldTower.Martinet.Shafarevich.IdealRadicalCyclotomicBase

Documentation

The cyclotomic base F(μ_p) inside AlgebraicClosure 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 IdealRadicalCyclotomicBase :
    IntermediateField F (AlgebraicClosure F)

theorem

finiteDimensional_idealRadicalCyclotomicBase

L48 ↗

ClassFieldTower.Martinet.Shafarevich.finiteDimensional_idealRadicalCyclotomicBase

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_idealRadicalCyclotomicBase :
    FiniteDimensional F (IdealRadicalCyclotomicBase F p hp)

theorem

idealRadicalCyclotomicBase_primitiveRoots_nonempty

L55 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicBase_primitiveRoots_nonempty

Documentation

The named cyclotomic base contains a primitive p-th root.

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_primitiveRoots_nonempty :
    (primitiveRoots p (IdealRadicalCyclotomicBase F p hp)).Nonempty

def

idealRadicalToCyclotomicBase

L70 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalToCyclotomicBase

Documentation

Map the base-field ideal radical into the unit group of 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

def idealRadicalToCyclotomicBase :
    (idealNthPowerRadicalKummerSubgroup F (p.toPNat hp.pos)).1 →*
      (IdealRadicalCyclotomicBase F p hp)ˣ

def

idealRadicalCyclotomicKummerSubgroup

L79 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalCyclotomicKummerSubgroup

Documentation

The Kummer subgroup over F(μ_p) generated by the mapped ideal radical and all ambient p-th powers.

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 idealRadicalCyclotomicKummerSubgroup :
    KummerSubgroup (IdealRadicalCyclotomicBase F p hp) (p.toPNat hp.pos)

def

idealRadicalToCyclotomicKummerSubgroup

L86 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalToCyclotomicKummerSubgroup

Documentation

The base-field ideal radical, with codomain restricted to the cyclotomic Kummer subgroup.

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 idealRadicalToCyclotomicKummerSubgroup :
    (idealNthPowerRadicalKummerSubgroup F (p.toPNat hp.pos)).1 →*
      (idealRadicalCyclotomicKummerSubgroup F p hp).1

def

idealRadicalToCyclotomicQuotientRaw

L94 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalToCyclotomicQuotientRaw

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 idealRadicalToCyclotomicQuotientRaw :
    (idealNthPowerRadicalKummerSubgroup F (p.toPNat hp.pos)).1 →*
      RestrictedRadicalQuotient (p.toPNat hp.pos)
        (idealRadicalCyclotomicKummerSubgroup F p hp)

def

idealRadicalQuotientToCyclotomicQuotient

L104 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalQuotientToCyclotomicQuotient

Documentation

The induced map from the base-field ideal radical quotient to the cyclotomic Kummer quotient.

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 idealRadicalQuotientToCyclotomicQuotient :
    IdealNthPowerRadicalQuotient F (p.toPNat hp.pos) →*
      RestrictedRadicalQuotient (p.toPNat hp.pos)
        (idealRadicalCyclotomicKummerSubgroup F p hp)

theorem

idealRadicalQuotientToCyclotomicQuotient_surjective

L134 ↗

ClassFieldTower.Martinet.Shafarevich.idealRadicalQuotientToCyclotomicQuotient_surjective

Documentation

Every cyclotomic Kummer class is represented by a mapped base-field ideal radical class.

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 idealRadicalQuotientToCyclotomicQuotient_surjective :
    Function.Surjective (idealRadicalQuotientToCyclotomicQuotient F p hp)

theorem

finite_idealRadicalCyclotomicRestrictedQuotient

L167 ↗

ClassFieldTower.Martinet.Shafarevich.finite_idealRadicalCyclotomicRestrictedQuotient

Documentation

The cyclotomic Kummer quotient generated by the ideal radical 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_idealRadicalCyclotomicRestrictedQuotient :
    Finite (RestrictedRadicalQuotient (p.toPNat hp.pos)
      (idealRadicalCyclotomicKummerSubgroup F p hp))

Module documentation

The ideal radical over a cyclotomic base

Declarations