Module

SeparableKummerH1.lean

Nyll.GaloisCohomology.Kummer.Concrete.SeparableKummerH1

6 declarations indexed from sourceView source ↗

Module documentation

Kummer characters over the separable closure

For an exponent nonzero in the base field, every unit has a root in the separable closure. The existing Galois Kummer equivalence therefore applies without a perfectness or characteristic-zero hypothesis.

Imports3

Nyll.GaloisCohomology.Kummer.Concrete.InfiniteCharacterEquiv
Mathlib.FieldTheory.IsSepClosed
Mathlib.GroupTheory.QuotientGroup.Basic

Imported by7

theorem

finiteKummerRadicalSubgroup_separableClosure_eq_top

L29 ↗

ClassFieldTower.Martinet.Shafarevich.finiteKummerRadicalSubgroup_separableClosure_eq_top

Documentation

Every base unit admits an n-th root in the separable closure when n is nonzero in the base field.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

theorem finiteKummerRadicalSubgroup_separableClosure_eq_top
    (n : ℕ+) [NeZero ((n : ℕ) : K)] :
    finiteKummerRadicalSubgroup (K := K) (L := SeparableClosure K) n = ⊤

def

unitsEquivSeparableRadicalCarrier

L48 ↗

ClassFieldTower.Martinet.Shafarevich.unitsEquivSeparableRadicalCarrier

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

def unitsEquivSeparableRadicalCarrier
    (n : ℕ+) [NeZero ((n : ℕ) : K)] :
    Kˣ ≃* (chosenFiniteKummerRadicalDatum
      (K := K) (L := SeparableClosure K) n).carrier

theorem

map_powerRange_unitsEquivSeparableRadicalCarrier

L56 ↗

ClassFieldTower.Martinet.Shafarevich.map_powerRange_unitsEquivSeparableRadicalCarrier

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

theorem map_powerRange_unitsEquivSeparableRadicalCarrier
    (n : ℕ+) [NeZero ((n : ℕ) : K)] :
    (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range.map
        (unitsEquivSeparableRadicalCarrier K n).toMonoidHom =
      (chosenFiniteKummerRadicalDatum
        (K := K) (L := SeparableClosure K) n).ambientNthPowersSubgroup

def

separablePowerClassEquivRadicalQuotient

L75 ↗

ClassFieldTower.Martinet.Shafarevich.separablePowerClassEquivRadicalQuotient

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

def separablePowerClassEquivRadicalQuotient
    (n : ℕ+) [NeZero ((n : ℕ) : K)] :
    Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
      (chosenFiniteKummerRadicalDatum
        (K := K) (L := SeparableClosure K) n).RadicalQuotient

def

separableKummerContinuousNthRootsCharacterEquiv

L91 ↗

ClassFieldTower.Martinet.Shafarevich.separableKummerContinuousNthRootsCharacterEquiv

Documentation

Power classes identify with continuous Kummer characters of the actual separable closure, in arbitrary characteristic prime to the exponent.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

def separableKummerContinuousNthRootsCharacterEquiv
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
      (Gal(SeparableClosure K/K) →ₜ*
        DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ))

theorem

separableKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq

L103 ↗

ClassFieldTower.Martinet.Shafarevich.separableKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq

Documentation

Evaluation uses any root with the prescribed power, independently of the root chosen in constructing the character equivalence.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]

Lean source · statement

theorem separableKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (β : (SeparableClosure K)ˣ)
    (hβ : β ^ (n : ℕ) =
      Units.map (algebraMap K (SeparableClosure K)).toMonoidHom a)
    (σ : Gal(SeparableClosure K/K)) :
    ((separableKummerContinuousNthRootsCharacterEquiv K n hmu
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range) σ :
      DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ)) :
        (SeparableClosure K)ˣ) =
      rootQuotient (K := K) (L := SeparableClosure K) β σ

Module documentation

Kummer characters over the separable closure

Declarations

finiteKummerRadicalSubgroup_separableClosure_eq_top

unitsEquivSeparableRadicalCarrier

map_powerRange_unitsEquivSeparableRadicalCarrier

separablePowerClassEquivRadicalQuotient

separableKummerContinuousNthRootsCharacterEquiv

separableKummerContinuousNthRootsCharacterEquiv_apply_of_pow_eq