Module

FieldMapNaturality.lean

Nyll.GaloisCohomology.Kummer.Concrete.FieldMapNaturality

4 declarations indexed from sourceView source ↗

Module documentation

Kummer characters under embeddings of arbitrary fields

The chosen map of algebraic closures restricts to the separable closures and carries root quotients to root quotients. This gives the naturality of Kummer characters under actual absolute Galois restriction, in every characteristic prime to the exponent.

Imports2

Imported by2

def

separableNthRootsFieldMapEquiv

L27 ↗

ClassFieldTower.Martinet.Shafarevich.separableNthRootsFieldMapEquiv

Documentation

If the source contains the roots of unity, embedding the source field identifies the discrete groups of roots in the two separable closures.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory Field.absoluteGaloisGroup ValuationTheory.Completion
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

def separableNthRootsFieldMapEquiv (f : K →+* L) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ) ≃ₜ*
      DiscreteNthRootsSubgroup (SeparableClosure L) (n : ℕ)

theorem

separableNthRootsFieldMapEquiv_coe

L39 ↗

ClassFieldTower.Martinet.Shafarevich.separableNthRootsFieldMapEquiv_coe

Documentation

The coefficient equivalence is induced by the chosen closure embedding.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory Field.absoluteGaloisGroup ValuationTheory.Completion
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem separableNthRootsFieldMapEquiv_coe (f : K →+* L) (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ)) :
    (separableNthRootsFieldMapEquiv f n hmu u : (SeparableClosure L)ˣ) =
      Units.map (separableClosureLift f).toMonoidHom (u : (SeparableClosure K)ˣ)

theorem

separableKummerCharacter_fieldMap

L58 ↗

ClassFieldTower.Martinet.Shafarevich.separableKummerCharacter_fieldMap

Documentation

The Kummer root quotient commutes with restriction along a field embedding.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory Field.absoluteGaloisGroup ValuationTheory.Completion
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem separableKummerCharacter_fieldMap
    (f : K →+* L) (n : ℕ+) [NeZero ((n : ℕ) : K)] [NeZero ((n : ℕ) : L)]
    (hmuK : (primitiveRoots (n : ℕ) K).Nonempty)
    (hmuL : (primitiveRoots (n : ℕ) L).Nonempty)
    (a : Kˣ) (σ : Gal(AlgebraicClosure L/L)) :
    Units.map (separableClosureLift f).toMonoidHom
      ((separableKummerContinuousNthRootsCharacterEquiv K n hmuK
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (separableClosureAutEquiv K (map f σ)) :
          DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ)) :
          (SeparableClosure K)ˣ) =
      ((separableKummerContinuousNthRootsCharacterEquiv L n hmuL
        ((Units.map f.toMonoidHom a) : Lˣ ⧸ (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range)
        (separableClosureAutEquiv L σ) :
          DiscreteNthRootsSubgroup (SeparableClosure L) (n : ℕ)) :
          (SeparableClosure L)ˣ)

theorem

separableKummerCharacter_fieldMap_equiv

L109 ↗

ClassFieldTower.Martinet.Shafarevich.separableKummerCharacter_fieldMap_equiv

Documentation

Kummer characters are natural under the induced equivalence of root coefficients.

Source context 3 commands

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

namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory Field.absoluteGaloisGroup ValuationTheory.Completion
variable {K L : Type*} [Field K] [Field L]

Lean source · statement

theorem separableKummerCharacter_fieldMap_equiv
    (f : K →+* L) (n : ℕ+) [NeZero ((n : ℕ) : K)] [NeZero ((n : ℕ) : L)]
    (hmuK : (primitiveRoots (n : ℕ) K).Nonempty)
    (hmuL : (primitiveRoots (n : ℕ) L).Nonempty)
    (a : Kˣ) (σ : Gal(AlgebraicClosure L/L)) :
    separableNthRootsFieldMapEquiv f n hmuK
      (separableKummerContinuousNthRootsCharacterEquiv K n hmuK
        (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
        (separableClosureAutEquiv K (map f σ))) =
      separableKummerContinuousNthRootsCharacterEquiv L n hmuL
        ((Units.map f.toMonoidHom a) : Lˣ ⧸ (powMonoidHom (n : ℕ) : Lˣ →* Lˣ).range)
        (separableClosureAutEquiv L σ)

Module documentation

Kummer characters under embeddings of arbitrary fields

Declarations

separableNthRootsFieldMapEquiv

separableNthRootsFieldMapEquiv_coe

separableKummerCharacter_fieldMap

separableKummerCharacter_fieldMap_equiv