NYLL
Module

FinitePlaceUnramifiedH1Transport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceUnramifiedH1Transport
8 declarations indexed from sourceView source ↗

Module documentation

Transport of unramified first-cohomology characters at a finite place

The local--global Galois comparison gives a linear equivalence between characters of the global decomposition group and of the completion's separable-closure Galois group. This equivalence identifies inertia-trivial characters with the intrinsic unramified residue-degree line.

Imports2
Imported by2

Declarations

instance

finitePlaceUnramifiedH1TransportTopology

L32 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1TransportTopology
Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p)
instance

finitePlaceUnramifiedH1TransportDiscreteTopology

L35 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1TransportDiscreteTopology
Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
Lean source · statement
instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p)
instance

finitePlaceUnramifiedH1TransportZModAddCommGroup

L38 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1TransportZModAddCommGroup
Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
Lean source · statement
instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p)
instance

finitePlaceUnramifiedH1TransportModule

L41 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceUnramifiedH1TransportModule
Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
Lean source · statement
instance finitePlaceUnramifiedH1TransportModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G))
def

continuousH1PullbackAddHom

L46 ↗
ClassFieldTower.Martinet.Shafarevich.continuousH1PullbackAddHom
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance finitePlaceUnramifiedH1TransportModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
def continuousH1PullbackAddHom
    {G H : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    (e : G ≃ₜ* H) :
    ContinuousH1ZMod (p := p) (G := H) →+
      ContinuousH1ZMod (p := p) (G := G) where
  toFun chi :=
    { toFun := fun sigma ↦ chi (Additive.ofMul (e sigma.toMul))
      map_zero' := by
        change chi (Additive.ofMul (e 1)) = 0
        rw [map_one]
        exact chi.map_zero
      map_add' := fun sigma tau ↦ by
        change chi (Additive.ofMul (e (sigma.toMul * tau.toMul))) =
          chi (Additive.ofMul (e sigma.toMul)) +
            chi (Additive.ofMul (e tau.toMul))
        rw [map_mul]
        exact chi.map_add _ _
      continuous_toFun := chi.continuous_toFun.comp e.continuous }
  map_zero' := by ext sigma; rfl
  map_add' := by intro chi psi; ext sigma; rfl
def

finitePlaceDecompositionH1LinearEquivLocalSeparable

L70 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1LinearEquivLocalSeparable
Documentation

Transport from the chosen global finite-place decomposition group to the intrinsic separable-closure absolute Galois group of the completion.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance finitePlaceUnramifiedH1TransportModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceDecompositionH1LinearEquivLocalSeparable
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) ≃ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p)
        (G := Gal(SeparableClosure
          (NumberField.HeightOneSpectrum.adicAbv F
            v).Completion/(NumberField.HeightOneSpectrum.adicAbv F v).Completion))
theorem

finitePlaceDecompositionH1LinearEquivLocalSeparable_apply

L101 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1LinearEquivLocalSeparable_apply
Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance finitePlaceUnramifiedH1TransportModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceDecompositionH1LinearEquivLocalSeparable_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : ContinuousH1ZMod
      (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v))
    (sigma : Gal(SeparableClosure
      (NumberField.HeightOneSpectrum.adicAbv F
        v).Completion/(NumberField.HeightOneSpectrum.adicAbv F v).Completion)) :
    finitePlaceDecompositionH1LinearEquivLocalSeparable F p v chi
        (Additive.ofMul sigma) =
      chi (Additive.ofMul
        ((finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup
          F v).symm sigma))
theorem

finitePlaceDecompositionH1LinearEquivLocalSeparable_mem_unramified_iff

L117 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1LinearEquivLocalSeparable_mem_unramified_iff
Documentation

Under the local--global Galois comparison, inertia-trivial characters are exactly the intrinsic residue-degree unramified line.

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NNReal NumberField ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
open LocalClassFieldTheory
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceUnramifiedH1TransportTopology :
    TopologicalSpace (ZMod p) := ⊥
local instance finitePlaceUnramifiedH1TransportDiscreteTopology :
    DiscreteTopology (ZMod p) := discreteTopology_bot _
local instance finitePlaceUnramifiedH1TransportZModAddCommGroup :
    AddCommGroup (ZMod p) := (ZMod.commRing p).toAddCommGroup
local instance finitePlaceUnramifiedH1TransportModule
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod p) (ContinuousH1ZMod (p := p) (G := G)) :=
  continuousH1ZModModule
Lean source · full declaration
theorem finitePlaceDecompositionH1LinearEquivLocalSeparable_mem_unramified_iff
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (chi : ContinuousH1ZMod
      (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    let vF := NumberField.HeightOneSpectrum.adicAbv F v
    let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
    letI : Valued vF.Completion NNReal :=
      finitePlaceCompletionValued vF hvFna
    letI : ValuativeRel vF.Completion :=
      finitePlaceCompletionValuativeRel vF hvFna
    letI : IsNonarchimedeanLocalField vF.Completion :=
      finitePlaceNormCompletionIsNonarchimedeanLocalField F v
    finitePlaceDecompositionH1LinearEquivLocalSeparable F p v chi ∈
        localIntrinsicUnramifiedH1 vF.Completion p ↔
      chi ∈ finitePlaceUnramifiedH1 F p v := by
  let vF := NumberField.HeightOneSpectrum.adicAbv F v
  let hvFna := NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv F v
  let _ : Valued vF.Completion NNReal :=
    finitePlaceCompletionValued vF hvFna
  let _ : ValuativeRel vF.Completion :=
    finitePlaceCompletionValuativeRel vF hvFna
  let _ : IsNonarchimedeanLocalField vF.Completion :=
    finitePlaceNormCompletionIsNonarchimedeanLocalField F v
  let e :=
    finitePlaceDecompositionGroupContinuousMulEquivSeparableAbsoluteGaloisGroup F v
  let I := finitePlaceAbsoluteInertiaSubgroup F v
  let J := localIntrinsicInertiaSubgroup vF.Completion
  have hmap : Subgroup.map e.toMonoidHom I = J :=
    finitePlaceAbsoluteInertia_map_eq_localResidueDegree_ker F v
  change
    (localIntrinsicH1InertiaRestriction vF.Completion p)
        (finitePlaceDecompositionH1LinearEquivLocalSeparable F p v chi) = 0 ↔
      (finitePlaceH1InertiaRestriction F p v) chi = 0
  constructor
  · intro hlocal
    apply ContinuousAddMonoidHom.ext
    intro sigma
    let sigmaI : I := sigma.toMul
    have hmem : e sigmaI.1 ∈ J := by
      rw [← hmap]
      exact ⟨sigmaI.1, sigmaI.property, rfl⟩
    have hv := DFunLike.congr_fun hlocal
      (Additive.ofMul (⟨e sigmaI.1, hmem⟩ : J))
    change chi (Additive.ofMul (e.symm (e sigmaI.1))) = 0 at hv
    change chi (Additive.ofMul sigmaI.1) = 0
    simpa only [e.symm_apply_apply] using hv
  · intro hglobal
    apply ContinuousAddMonoidHom.ext
    intro tau
    have hmemMap : tau.toMul.1 ∈ Subgroup.map e.toMonoidHom I := by
      rw [hmap]
      exact tau.toMul.property
    obtain ⟨sigma, hsigma, heq⟩ := hmemMap
    let sigmaI : I := ⟨sigma, hsigma⟩
    have hv := DFunLike.congr_fun hglobal (Additive.ofMul sigmaI)
    have heq' : e.symm tau.toMul.1 = sigma := by
      rw [← heq]
      exact e.symm_apply_apply sigma
    change chi (Additive.ofMul sigmaI.1) = 0 at hv
    change chi (Additive.ofMul (e.symm tau.toMul.1)) = 0
    rw [heq']
    exact hv

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