NYLL
Module

FinitePlaceH1AdicRestriction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceH1AdicRestriction
9 declarations indexed from sourceView source ↗

Module documentation

Actual absolute-character restriction to the adic completion

The inverse of the decomposition--adic equivalence transports the already constructed decomposition-group restriction to intrinsic local H¹.

Imports2
Imported by8

Declarations

instance

finitePlaceH1AdicCanonicalZModAddCommGroup

L28 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1AdicCanonicalZModAddCommGroup
Source context 6 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p)
instance

finitePlaceH1AdicCharacterTopology

L31 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1AdicCharacterTopology
Source context 7 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
Lean source · statement
instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p))
instance

finitePlaceH1AdicCharacterDiscreteTopology

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1AdicCharacterDiscreteTopology
Source context 8 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
Lean source · statement
instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p))
instance

finitePlaceH1AdicModule

L37 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceH1AdicModule
Source context 9 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
Lean source · statement
instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G))
def

finitePlaceDecompositionH1ToAdic

L43 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1ToAdic
Documentation

Transport decomposition-group H¹ through the actual inverse localization.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
local instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceDecompositionH1ToAdic
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v) →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup (v.adicCompletion F))
theorem

finitePlaceAdicH1Restriction_decompositionH1ToAdic

L57 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicH1Restriction_decompositionH1ToAdic
Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
local instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAdicH1Restriction_decompositionH1ToAdic
    (v : HeightOneSpectrum (RingOfIntegers F))
    (chi : ContinuousH1ZMod (p := p) (G := finitePlaceAbsoluteDecompositionGroup F v)) :
    finitePlaceAdicH1Restriction F p v (finitePlaceDecompositionH1ToAdic F p v chi) =
      chi
theorem

finitePlaceDecompositionH1ToAdic_adicH1Restriction

L68 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionH1ToAdic_adicH1Restriction
Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
local instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceDecompositionH1ToAdic_adicH1Restriction
    (v : HeightOneSpectrum (RingOfIntegers F))
    (chi : ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup (v.adicCompletion F))) :
    finitePlaceDecompositionH1ToAdic F p v (finitePlaceAdicH1Restriction F p v chi) =
      chi
def

finitePlaceAbsoluteH1AdicRestriction

L80 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1AdicRestriction
Documentation

Actual global absolute-character restriction, now valued in intrinsic adic H¹.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
local instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
def finitePlaceAbsoluteH1AdicRestriction
    (v : HeightOneSpectrum (RingOfIntegers F)) :
    absoluteContinuousZModCharacterModP F p →ₗ[ZMod p]
      ContinuousH1ZMod (p := p) (G := Field.absoluteGaloisGroup (v.adicCompletion F))
theorem

finitePlaceAbsoluteH1AdicRestriction_decomposition

L89 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteH1AdicRestriction_decomposition
Documentation

Pulling back the intrinsic local restriction recovers the original actual decomposition-group restriction, with no change of character.

Source context 10 commands

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

open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.ProP
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceH1AdicCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceH1AdicCharacterTopology :
    TopologicalSpace (Multiplicative (ZMod p)) := ⊥
local instance finitePlaceH1AdicCharacterDiscreteTopology :
    DiscreteTopology (Multiplicative (ZMod p)) := discreteTopology_bot _
local instance finitePlaceH1AdicModule
    {q : ℕ} {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule
Lean source · statement
theorem finitePlaceAbsoluteH1AdicRestriction_decomposition
    (v : HeightOneSpectrum (RingOfIntegers F))
    (chi : absoluteContinuousZModCharacterModP F p) :
    finitePlaceAdicH1Restriction F p v (finitePlaceAbsoluteH1AdicRestriction F p v chi) =
      finitePlaceAbsoluteH1DecompositionRestriction F p v chi

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