Module

LocalMultiplicativeCompletion.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.LocalMultiplicativeCompletion

5 declarations indexed from sourceView source ↗

Module documentation

The profinite completion of a local multiplicative group

Every nontrivial element of Kˣ is detected by an open finite quotient. A nonzero valuation is detected by a finite cyclic quotient of ℤ; an element of valuation zero is detected by a finite quotient of the profinite unit group. Consequently the canonical map from Kˣ to its completion by open finite quotients is injective.

Imports6

Nyll.ClassFieldTheory.LocalClassFieldTheory.Infinite.ProfiniteCompletion
Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.MultiplicativeDecomposition
Mathlib.Data.ZMod.Basic
Batteries.Tactic.Init
Lean.Elab.Tactic.Omega
Lean.Elab.Tactic.RCases

Imported by2

def

finiteTargetKernelOpenFiniteIndexNormalSubgroup

L37 ↗

LocalClassFieldTheory.finiteTargetKernelOpenFiniteIndexNormalSubgroup

Documentation

The kernel of a continuous homomorphism to a finite discrete group is an open finite-index normal subgroup.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalClassFieldTheory
open scoped ValuativeRel WithZero
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def finiteTargetKernelOpenFiniteIndexNormalSubgroup
    {G : Type u} {F : Type v}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group F] [Finite F] [TopologicalSpace F] [DiscreteTopology F]
    (f : G →ₜ* F) : OpenFiniteIndexNormalSubgroup G

def

valuationModContinuousMonoidHom

L55 ↗

LocalClassFieldTheory.valuationModContinuousMonoidHom

Documentation

The normalized valuation reduced modulo n, as a continuous multiplicative homomorphism. The topology on the finite target is supplied by the caller so that no global instance is introduced for the type tag.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalClassFieldTheory
open scoped ValuativeRel WithZero
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

def valuationModContinuousMonoidHom
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (n : ℕ)
    [TopologicalSpace (Multiplicative (ZMod n))]
    [DiscreteTopology (Multiplicative (ZMod n))] :
    Kˣ →ₜ* Multiplicative (ZMod n) where
  toMonoidHom :=
    (Int.castAddHom (ZMod n)).toMultiplicative.comp (valuationUnitsMulHom K)
  continuous_toFun := by
    exact (continuous_of_discreteTopology : Continuous
      (Int.castAddHom (ZMod n)).toMultiplicative).comp
        (valuationUnitsMulHom_continuous K)

theorem

exists_openFiniteIndexNormalSubgroup_not_mem_localMultiplicativeGroup

L70 ↗

LocalClassFieldTheory.exists_openFiniteIndexNormalSubgroup_not_mem_localMultiplicativeGroup

Documentation

Every nontrivial element of Kˣ is omitted by some open finite-index normal subgroup.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalClassFieldTheory
open scoped ValuativeRel WithZero
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem exists_openFiniteIndexNormalSubgroup_not_mem_localMultiplicativeGroup
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] (x : Kˣ) (hx : x ≠ 1) :
    ∃ H : OpenFiniteIndexNormalSubgroup Kˣ,
      x ∉ H.toOpenNormalSubgroup.toSubgroup

theorem

localMultiplicativeGroup_residuallyFinite

L133 ↗

LocalClassFieldTheory.localMultiplicativeGroup_residuallyFinite

Documentation

The intersection of the open finite-index normal subgroups of Kˣ is trivial.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalClassFieldTheory
open scoped ValuativeRel WithZero
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem localMultiplicativeGroup_residuallyFinite
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    (⨅ H : OpenFiniteIndexNormalSubgroup Kˣ,
      H.toOpenNormalSubgroup.toSubgroup) = ⊥

theorem

topologicalProfiniteCompletionMap_injective_localField

L149 ↗

LocalClassFieldTheory.topologicalProfiniteCompletionMap_injective_localField

Documentation

The canonical map from a local multiplicative group to its completion by open finite quotients is injective.

Source context 5 commands

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

noncomputable section
universe u v
namespace LocalClassFieldTheory
open scoped ValuativeRel WithZero
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem topologicalProfiniteCompletionMap_injective_localField
    (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K] :
    Function.Injective (topologicalProfiniteCompletionMap Kˣ)

Module documentation

The profinite completion of a local multiplicative group

Declarations

finiteTargetKernelOpenFiniteIndexNormalSubgroup

valuationModContinuousMonoidHom

exists_openFiniteIndexNormalSubgroup_not_mem_localMultiplicativeGroup

localMultiplicativeGroup_residuallyFinite

topologicalProfiniteCompletionMap_injective_localField