NYLL
Module

LocalKummerInertia.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.LocalKummerInertia
12 declarations indexed from sourceView source ↗

Module documentation

Intrinsic inertia and local Kummer characters

The standard algebraic-closure Kummer character is transported to the local separable-closure model. Its kernel is the stabilizer of the chosen simple Kummer root, without imposing a residue-characteristic restriction.

Imports4
Imported by3

Declarations

instance

localKummerInertiaTopology

L30 ↗
ClassFieldTower.Martinet.Shafarevich.localKummerInertiaTopology
Source context 5 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance localKummerInertiaTopology : TopologicalSpace (ZMod p)
instance

localKummerInertiaDiscreteTopology

L31 ↗
ClassFieldTower.Martinet.Shafarevich.localKummerInertiaDiscreteTopology
Source context 6 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p)
instance

localKummerInertiaZModAddCommGroup

L33 ↗
ClassFieldTower.Martinet.Shafarevich.localKummerInertiaZModAddCommGroup
Source context 7 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
Lean source · statement
instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p)
instance

localKummerInertiaH1Module

L35 ↗
ClassFieldTower.Martinet.Shafarevich.localKummerInertiaH1Module
Source context 8 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
Lean source · statement
instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

continuousH1ZModCongr

L41 ↗
ClassFieldTower.Martinet.Shafarevich.continuousH1ZModCongr
Documentation

Continuous H¹ is transported covariantly along a topological group equivalence.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def continuousH1ZModCongr
    {G H : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) :
    ContinuousH1ZMod (p := p) (G := G) ≃ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := H)
theorem

continuousH1ZModCongr_apply

L73 ↗
ClassFieldTower.Martinet.Shafarevich.continuousH1ZModCongr_apply
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem continuousH1ZModCongr_apply
    {G H : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) (chi : ContinuousH1ZMod (p := p) (G := G)) (sigma : H) :
    continuousH1ZModCongr p e chi (Additive.ofMul sigma) =
      chi (Additive.ofMul (e.symm sigma))
def

localStandardH1LinearEquivSeparable

L81 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1LinearEquivSeparable
Documentation

Change from the algebraic-closure model to the intrinsic separable-closure model.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def localStandardH1LinearEquivSeparable
    (K : Type) [Field K] :
    ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K) ≃ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := Gal(SeparableClosure K / K))
theorem

localStandardH1LinearEquivSeparable_apply

L89 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1LinearEquivSeparable_apply
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localStandardH1LinearEquivSeparable_apply
    (K : Type) [Field K]
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup K))
    (sigma : Gal(SeparableClosure K/K)) :
    localStandardH1LinearEquivSeparable p K chi (Additive.ofMul sigma) =
      chi (Additive.ofMul
        ((RamificationTheory.Field.absoluteGaloisGroup.separableClosureContinuousMulEquiv
          K).symm sigma))
theorem

rootQuotient_eq_of_same_pow

L98 ↗
ClassFieldTower.Martinet.Shafarevich.rootQuotient_eq_of_same_pow
Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem rootQuotient_eq_of_same_pow
    {K L : Type} [Field K] [Field L] [Algebra K L]
    (n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (u u' : Lˣ)
    (hu : u ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a)
    (hu' : u' ^ (n : ℕ) = Units.map (algebraMap K L).toMonoidHom a)
    (sigma : Gal(L/K)) :
    rootQuotient (K := K) (L := L) u sigma =
      rootQuotient (K := K) (L := L) u' sigma
theorem

absoluteKummerH1_mk_eq_zero_iff_root_fixed

L116 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteKummerH1_mk_eq_zero_iff_root_fixed
Documentation

The kernel of a Kummer character is precisely the stabilizer of any root with the prescribed power.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem absoluteKummerH1_mk_eq_zero_iff_root_fixed
    (K : Type) [Field K] [CharZero K]
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ)
    (u : (AlgebraicClosure K)ˣ)
    (hu : u ^ p = Units.map (algebraMap K (AlgebraicClosure K)).toMonoidHom a)
    (sigma : Field.absoluteGaloisGroup K) :
    absoluteKummerContinuousH1LinearEquiv K p hmu
        (Additive.ofMul
          (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a))
        (Additive.ofMul sigma) = 0 ↔
      absoluteGaloisGroupContinuousMulEquiv K sigma • u = u
theorem

localStandardH1LinearEquivSeparable_kummer_eq_zero_iff

L157 ↗
ClassFieldTower.Martinet.Shafarevich.localStandardH1LinearEquivSeparable_kummer_eq_zero_iff
Documentation

In the separable-closure model the Kummer character vanishes exactly on automorphisms fixing the chosen simple Kummer root.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localStandardH1LinearEquivSeparable_kummer_eq_zero_iff
    (K : Type) [Field K] [CharZero K]
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ)
    (sigma : Gal(SeparableClosure K/K)) :
    localStandardH1LinearEquivSeparable p K
        (absoluteKummerContinuousH1LinearEquiv K p hmu
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)))
        (Additive.ofMul sigma) = 0 ↔
      sigma (chosenSimpleKummerRoot K ⟨p, (Fact.out : p.Prime).pos⟩
          (Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero) a) =
        chosenSimpleKummerRoot K ⟨p, (Fact.out : p.Prime).pos⟩
          (Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero) a
theorem

localKummerH1_mem_unramified_iff_inertia_le

L226 ↗
ClassFieldTower.Martinet.Shafarevich.localKummerH1_mem_unramified_iff_inertia_le
Documentation

The intrinsic unramified condition on a Kummer class says exactly that local inertia fixes its simple Kummer extension.

Source context 9 commands

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

open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP KummerTheory LocalClassFieldTheory
variable (p : ℕ) [Fact p.Prime]
local instance localKummerInertiaTopology : TopologicalSpace (ZMod p) := ⊥
local instance localKummerInertiaDiscreteTopology : DiscreteTopology (ZMod p) :=
  discreteTopology_bot _
local instance localKummerInertiaZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.commRing p).toAddCommGroup
local instance localKummerInertiaH1Module
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem localKummerH1_mem_unramified_iff_inertia_le
    (K : Type) [Field K] [CharZero K]
    [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ) :
    localStandardH1LinearEquivSeparable p K
        (absoluteKummerContinuousH1LinearEquiv K p hmu
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a))) ∈
        localIntrinsicUnramifiedH1 K p ↔
      localIntrinsicInertiaSubgroup K ≤
        (chosenSimpleKummerExtension K ⟨p, (Fact.out : p.Prime).pos⟩
          (Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero) a).fixingSubgroup

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