NYLL
Module

FinitePlaceUnramifiedH1.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceUnramifiedH1
12 declarations indexed from sourceView source ↗

Module documentation

Unramified degree-one characters at a finite place

The valuation-subring inertia group is pulled back to the chosen absolute decomposition group. Restriction to this inertia subgroup defines the unramified continuous H¹ subspace.

Imports4
Imported by15

Declarations

instance

finitePlaceUnramifiedH1Module

L33 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1Module
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
Lean source · statement
instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H))
theorem

finitePlaceAbsoluteValueExtension_nonarchimedean

L39 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteValueExtension_nonarchimedean
Documentation

The chosen absolute-value extension at a finite place is nonarchimedean.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteValueExtension_nonarchimedean
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    LubinTate.Valuations.NonarchimedeanAbsoluteValue
      (finitePlaceAbsoluteValueExtension F v).1
abbrev

finitePlaceAbsoluteValuationSubring

L46 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteValuationSubring
Documentation

The valuation subring of the algebraic closure selected by the chosen finite place.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev finitePlaceAbsoluteValuationSubring
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ValuationSubring (AlgebraicClosure F)
def

finitePlaceAbsoluteDecompositionValuationEquiv

L55 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteDecompositionValuationEquiv
Documentation

The canonical comparison from the absolute decomposition group to its valuation-subring form.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteDecompositionValuationEquiv
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v ≃*
      RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup F
        (finitePlaceAbsoluteValuationSubring F v)
abbrev

finitePlaceAbsoluteInertiaSubgroup

L67 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertiaSubgroup
Documentation

Absolute inertia inside the chosen absolute decomposition group.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev finitePlaceAbsoluteInertiaSubgroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Subgroup (finitePlaceAbsoluteDecompositionGroup F v)
def

finitePlaceAbsoluteInertiaInclusion

L75 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertiaInclusion
Documentation

The continuous inclusion of absolute inertia into absolute decomposition.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteInertiaInclusion
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteInertiaSubgroup F v →ₜ*
      finitePlaceAbsoluteDecompositionGroup F v
theorem

finitePlaceAbsoluteInertiaInclusion_apply

L82 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertiaInclusion_apply
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteInertiaInclusion_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    finitePlaceAbsoluteInertiaInclusion F v sigma = sigma.1
def

finitePlaceH1InertiaRestrictionAddHom

L89 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1InertiaRestrictionAddHom
Documentation

Restriction of continuous mod-p characters from decomposition to inertia.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · full declaration
def finitePlaceH1InertiaRestrictionAddHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) →+
      ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteInertiaSubgroup F v) where
  toFun chi :=
    { toFun := fun sigma ↦ chi (Additive.ofMul sigma.toMul.1)
      map_zero' := chi.map_zero
      map_add' := fun sigma tau ↦ chi.map_add
        (Additive.ofMul sigma.toMul.1) (Additive.ofMul tau.toMul.1)
      continuous_toFun := chi.continuous_toFun.comp continuous_subtype_val }
  map_zero' := by
    ext sigma
    rfl
  map_add' := by
    intro chi psi
    ext sigma
    rfl
def

finitePlaceH1InertiaRestriction

L108 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1InertiaRestriction
Documentation

Linear restriction of continuous mod-p characters from decomposition to inertia.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceH1InertiaRestriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteInertiaSubgroup F v)
theorem

finitePlaceH1InertiaRestriction_apply

L115 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1InertiaRestriction_apply
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceH1InertiaRestriction_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v))
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    finitePlaceH1InertiaRestriction F p v chi (Additive.ofMul sigma) =
      chi (Additive.ofMul sigma.1)
abbrev

finitePlaceUnramifiedH1

L124 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1
Documentation

Continuous degree-one characters unramified at v: those trivial on absolute inertia.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
abbrev finitePlaceUnramifiedH1
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Submodule (ZMod p)
      (ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v))
theorem

mem_finitePlaceUnramifiedH1_iff

L130 ↗
ClassFieldTower.Martinet.Shafarevich.mem_finitePlaceUnramifiedH1_iff
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)
local instance finitePlaceUnramifiedH1Module
    {q : ℕ} {H : Type*} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := H)) :=
  continuousH1ZModModule
Lean source · statement
theorem mem_finitePlaceUnramifiedH1_iff
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    chi ∈ finitePlaceUnramifiedH1 F p v ↔
      ∀ sigma : finitePlaceAbsoluteInertiaSubgroup F v,
        chi (Additive.ofMul sigma.1) = 0

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