NYLL
Module

SeparableAbsoluteKummer.lean

Nyll.GaloisCohomology.Kummer.Concrete.SeparableAbsoluteKummer
4 declarations indexed from sourceView source ↗

Module documentation

Absolute constant-coefficient Kummer theory through the separable closure

The actual Krull restriction equivalence transfers separable Kummer characters to the existing absolute Galois group. The exponent need only be nonzero in the base field; no characteristic-zero or perfectness assumption is needed.

Imports7
Imported by5

Declarations

def

continuousCharacterDomainCoefficientsEquiv

L30 ↗
ClassFieldTower.Martinet.Shafarevich.continuousCharacterDomainCoefficientsEquiv
Source context 3 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory

-- Four group carriers and their four topologies; no new data instances.
Lean source · full declaration
def continuousCharacterDomainCoefficientsEquiv
    {G H A B : Type*} [Group G] [TopologicalSpace G]
    [Group H] [TopologicalSpace H]
    [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
    [CommGroup B] [TopologicalSpace B] [IsTopologicalGroup B]
    (e : G ≃ₜ* H) (d : A ≃ₜ* B) :
    (H →ₜ* A) ≃* (G →ₜ* B) where
  toFun f :=
    { toMonoidHom := d.toMulEquiv.toMonoidHom.comp
        (f.toMonoidHom.comp e.toMulEquiv.toMonoidHom)
      continuous_toFun := d.continuous.comp (f.continuous.comp e.continuous) }
  invFun f :=
    { toMonoidHom := d.symm.toMulEquiv.toMonoidHom.comp
        (f.toMonoidHom.comp e.symm.toMulEquiv.toMonoidHom)
      continuous_toFun := d.symm.continuous.comp (f.continuous.comp e.symm.continuous) }
  left_inv f := by
    apply ContinuousMonoidHom.ext
    intro h
    change d.symm (d (f (e (e.symm h)))) = f h
    rw [ContinuousMulEquiv.apply_symm_apply, ContinuousMulEquiv.symm_apply_apply]
  right_inv f := by
    apply ContinuousMonoidHom.ext
    intro g
    change d (d.symm (f (e.symm (e g)))) = f g
    rw [ContinuousMulEquiv.symm_apply_apply, ContinuousMulEquiv.apply_symm_apply]
  map_mul' f g := by
    apply ContinuousMonoidHom.ext
    intro x
    exact map_mul d (f (e x)) (g (e x))
def

separableDiscreteNthRootsContinuousMulEquivMultiplicativeZMod

L64 ↗
ClassFieldTower.Martinet.Shafarevich.separableDiscreteNthRootsContinuousMulEquivMultiplicativeZMod
Documentation

The chosen primitive base root identifies separable-closure roots with constant cyclic coefficients, using the canonical discrete topologies.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory

-- Four group carriers and their four topologies; no new data instances.
variable (K : Type*) [Field K]
Lean source · statement
def separableDiscreteNthRootsContinuousMulEquivMultiplicativeZMod
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    DiscreteNthRootsSubgroup (SeparableClosure K) (n : ℕ) ≃ₜ*
      Multiplicative (ZMod (n : ℕ))
def

separableAbsoluteKummerContinuousZModCharacterEquiv

L84 ↗
ClassFieldTower.Martinet.Shafarevich.separableAbsoluteKummerContinuousZModCharacterEquiv
Documentation

Absolute Kummer theory with constant mod-n coefficients for any field whose characteristic does not divide n.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory

-- Four group carriers and their four topologies; no new data instances.
variable (K : Type*) [Field K]
Lean source · statement
def separableAbsoluteKummerContinuousZModCharacterEquiv
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
      (Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod (n : ℕ)))
theorem

separableAbsoluteKummerContinuousZModCharacterEquiv_apply

L96 ↗
ClassFieldTower.Martinet.Shafarevich.separableAbsoluteKummerContinuousZModCharacterEquiv_apply
Documentation

Evaluation is the existing separable Kummer character on the actual restriction of the absolute automorphism, followed by the root coefficient map.

Source context 4 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory

-- Four group carriers and their four topologies; no new data instances.
variable (K : Type*) [Field K]
Lean source · statement
theorem separableAbsoluteKummerContinuousZModCharacterEquiv_apply
    (n : ℕ+) [NeZero ((n : ℕ) : K)]
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range)
    (σ : Field.absoluteGaloisGroup K) :
    separableAbsoluteKummerContinuousZModCharacterEquiv K n hmu a σ =
      separableDiscreteNthRootsContinuousMulEquivMultiplicativeZMod K n hmu
        (separableKummerContinuousNthRootsCharacterEquiv K n hmu a
          (ValuationTheory.Completion.separableClosureAutContinuousEquiv K σ))

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