Module

FinitePlaceCyclotomicMuPKummerComparison.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCyclotomicMuPKummerComparison

34 declarations indexed from sourceView source ↗

Module documentation

Finite-place comparison of natural and intrinsic-local Kummer H¹

This file compares the restriction of the natural mu_p Kummer class to a finite-place decomposition group with intrinsic Kummer theory over the adic completion. The coefficient map uses the actual algebraic-localization embedding selected by the decomposition--completion equivalence.

Imports9

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.AbsoluteMuPKummerComparison
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceAlgebraicLocalizationAlgClosure
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.FinitePlaceCyclotomicKummerH1
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FinitePlaceMuPH1Localization
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Radical.LocalValuationKummerDual
Mathlib.Algebra.Field.ZMod
Mathlib.Topology.Algebra.Group.Basic
Mathlib.Topology.Algebra.ContinuousMonoidHom
Mathlib.Topology.Instances.ZMod

Imported by6

def

finitePlacePowerClassLocalizationMonoidHom

L44 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlacePowerClassLocalizationMonoidHom

Documentation

Localization of multiplicative power classes from a number field to one adic completion.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
section PowerClassLocalization
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def finitePlacePowerClassLocalizationMonoidHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    (Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) →*
      ((v.adicCompletion K)ˣ ⧸
        (powMonoidHom p :
          (v.adicCompletion K)ˣ →* (v.adicCompletion K)ˣ).range)

def

finitePlacePowerClassLocalization

L63 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlacePowerClassLocalization

Documentation

Finite-place localization as a ZMod p-linear map on power classes.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
section PowerClassLocalization
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def finitePlacePowerClassLocalization
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    absolutePowerClassModP K p →ₗ[ZMod p]
      FinitePlaceLocalPowerClassModP K p v

theorem

finitePlacePowerClassLocalization_mk

L84 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlacePowerClassLocalization_mk

Documentation

A represented global power class localizes to the class of its diagonal image in the completion.

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
section PowerClassLocalization
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlacePowerClassLocalization_mk
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (a : Kˣ) :
    finitePlacePowerClassLocalization K p v
        (Additive.ofMul
          (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a)) =
      Additive.ofMul
        (QuotientGroup.mk'
          (powMonoidHom p :
            (v.adicCompletion K)ˣ →* (v.adicCompletion K)ˣ).range
          (Units.map (algebraMap K (v.adicCompletion K)).toMonoidHom a))

instance

finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup

L101 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p)

instance

finitePlaceCyclotomicComparisonFiniteDimensional

L104 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicComparisonFiniteDimensional

Source context 10 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup

Lean source · statement

instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p)

instance

finitePlaceCyclotomicComparisonNumberField

L109 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicComparisonNumberField

Source context 11 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)

Lean source · statement

instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p)

instance

finitePlaceCyclotomicComparisonH1Module

L113 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicComparisonH1Module

Source context 12 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)

Lean source · statement

instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G))

theorem

fieldAlgebra_isTorsionFree_forCyclotomicComparison

L118 ↗

ClassFieldTower.Martinet.Shafarevich.fieldAlgebra_isTorsionFree_forCyclotomicComparison

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem fieldAlgebra_isTorsionFree_forCyclotomicComparison
    {K L : Type} [Field K] [Field L] [Algebra K L] :
    Module.IsTorsionFree K L

def

absoluteGaloisSemilinearCongrContinuousMonoidHom

L127 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteGaloisSemilinearCongrContinuousMonoidHom

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def absoluteGaloisSemilinearCongrContinuousMonoidHom
    (K K' : Type) [Field K] [Field K'] (c : K ≃+* K') :
    Field.absoluteGaloisGroup K →ₜ* Field.absoluteGaloisGroup K'

def

finitePlaceCompletionAbsoluteGaloisSemilinearCongr

L168 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCompletionAbsoluteGaloisSemilinearCongr

Documentation

Conjugation between the absolute Galois groups of the two canonical models of a finite-place completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceCompletionAbsoluteGaloisSemilinearCongr
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    Field.absoluteGaloisGroup
        (NumberField.HeightOneSpectrum.adicAbv K v).Completion →ₜ*
      Field.absoluteGaloisGroup (v.adicCompletion K)

def

finitePlaceDecompositionToAdicAbsoluteGaloisGroup

L181 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceDecompositionToAdicAbsoluteGaloisGroup

Documentation

The selected decomposition group mapped to the absolute Galois group of the concrete adic completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceDecompositionToAdicAbsoluteGaloisGroup
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    finitePlaceAbsoluteDecompositionGroup K v →ₜ*
      Field.absoluteGaloisGroup (v.adicCompletion K)

structure

FinitePlaceAlgebraicClosureEmbeddingData

L194 ↗

ClassFieldTower.Martinet.Shafarevich.FinitePlaceAlgebraicClosureEmbeddingData

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

structure FinitePlaceAlgebraicClosureEmbeddingData
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) where
  embedding : AlgebraicClosure K →+* AlgebraicClosure (v.adicCompletion K)
  action : ∀ (sigma : finitePlaceAbsoluteDecompositionGroup K v)
      (x : AlgebraicClosure K),
    absoluteGaloisGroupContinuousMulEquiv
        (v.adicCompletion K)
        (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma)
        (embedding x) = embedding (sigma.1 x)
  algebraMap : ∀ x : K,
    embedding (algebraMap K (AlgebraicClosure K) x) =
      algebraMap (v.adicCompletion K)
        (AlgebraicClosure (v.adicCompletion K))
        (algebraMap K (v.adicCompletion K) x)

def

finitePlaceAlgebraicClosureEmbeddingData

L210 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureEmbeddingData

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAlgebraicClosureEmbeddingData
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    FinitePlaceAlgebraicClosureEmbeddingData K v

def

finitePlaceAlgebraicClosureEmbedding

L264 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureEmbedding

Documentation

The selected algebraic-localization embedding from a number field's algebraic closure to an algebraic closure of one concrete adic completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAlgebraicClosureEmbedding
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    AlgebraicClosure K →+* AlgebraicClosure (v.adicCompletion K)

theorem

finitePlaceAlgebraicClosureEmbedding_action

L272 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureEmbedding_action

Documentation

The selected global-to-local algebraic-closure embedding intertwines the decomposition action with the concrete local absolute-Galois action.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAlgebraicClosureEmbedding_action
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (sigma : finitePlaceAbsoluteDecompositionGroup K v)
    (x : AlgebraicClosure K) :
    absoluteGaloisGroupContinuousMulEquiv
        (v.adicCompletion K)
        (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma)
        (finitePlaceAlgebraicClosureEmbedding K v x) =
      finitePlaceAlgebraicClosureEmbedding K v (sigma.1 x)

theorem

finitePlaceAlgebraicClosureEmbedding_algebraMap

L286 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAlgebraicClosureEmbedding_algebraMap

Documentation

The selected algebraic-closure embedding extends the diagonal embedding of the number field into its concrete adic completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAlgebraicClosureEmbedding_algebraMap
    (K : Type) [Field K] [NumberField K]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (x : K) :
    finitePlaceAlgebraicClosureEmbedding K v
        (algebraMap K (AlgebraicClosure K) x) =
      algebraMap (v.adicCompletion K)
        (AlgebraicClosure (v.adicCompletion K))
        (algebraMap K (v.adicCompletion K) x)

theorem

rootQuotient_eq_of_same_pow_of_primitiveRoots_forComparison

L296 ↗

ClassFieldTower.Martinet.Shafarevich.rootQuotient_eq_of_same_pow_of_primitiveRoots_forComparison

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem rootQuotient_eq_of_same_pow_of_primitiveRoots_forComparison
    {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

def

finitePlaceAbsoluteMuPToAdicAddHom

L320 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPToAdicAddHom

Documentation

Roots of unity transported through the selected global-to-adic algebraic-closure embedding.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · full declaration

def finitePlaceAbsoluteMuPToAdicAddHom
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    AbsoluteMuP K p →+ AbsoluteMuP (v.adicCompletion K) p where
  toFun := fun x ↦ Additive.ofMul
    ⟨Units.map (finitePlaceAlgebraicClosureEmbedding K v).toMonoidHom x.toMul,
      by
        change
          Units.map (finitePlaceAlgebraicClosureEmbedding K v).toMonoidHom
              x.toMul ^ p = 1
        rw [← map_pow]
        rw [(mem_nthRootsSubgroup_iff (AlgebraicClosure K)).mp x.toMul.property]
        exact map_one _⟩
  map_zero' := by
    apply Additive.toMul.injective
    apply Subtype.ext
    apply Units.ext
    exact map_one _
  map_add' := by
    intro x y
    apply Additive.toMul.injective
    apply Subtype.ext
    apply Units.ext
    exact map_mul _ _ _

def

finitePlaceAbsoluteMuPToAdic

L347 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPToAdic

Documentation

The preceding root-of-unity transport as a ZMod p-linear map.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAbsoluteMuPToAdic
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    AbsoluteMuP K p →ₗ[ZMod p] AbsoluteMuP (v.adicCompletion K) p

theorem

finitePlaceAbsoluteMuPToAdic_action

L356 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPToAdic_action

Documentation

Root-of-unity transport intertwines the decomposition action with the absolute-Galois action of the concrete adic completion.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPToAdic_action
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (sigma : finitePlaceAbsoluteDecompositionGroup K v)
    (x : AbsoluteMuP K p) :
    finitePlaceAbsoluteMuPToAdic K p v
        (absoluteMuPActionContinuousLinearMap K p sigma.1 x) =
      absoluteMuPActionContinuousLinearMap (v.adicCompletion K) p
        (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma)
        (finitePlaceAbsoluteMuPToAdic K p v x)

def

finitePlaceAbsoluteMuPAdicCoordinate

L384 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPAdicCoordinate

Documentation

The actual algebraic-localization coefficient transport, followed by the chosen local mu_p ≃ ZMod p coordinate.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAbsoluteMuPAdicCoordinate
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty) :
    AbsoluteMuP K p →ₗ[ZMod p] ZMod p

def

finitePlaceAbsoluteMuPAdicCoordinateContinuous

L394 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPAdicCoordinateContinuous

Documentation

Coefficient transport as a continuous linear map.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAbsoluteMuPAdicCoordinateContinuous
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty) :
    AbsoluteMuP K p →L[ZMod p] ZMod p

def

finitePlaceAbsoluteMuPAdicCoordinateHom

L405 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPAdicCoordinateHom

Documentation

The actual local coefficient coordinate is an intertwining map from the natural decomposition representation to the trivial ZMod p line.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAbsoluteMuPAdicCoordinateHom
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty) :
    TopRep.res
        (ContinuousMonoidHom.id (finitePlaceAbsoluteDecompositionGroup K v) :
          finitePlaceAbsoluteDecompositionGroup K v →*
            finitePlaceAbsoluteDecompositionGroup K v)
        (finitePlaceAbsoluteMuPTopRep K p v) ⟶
      trivialZModP p (finitePlaceAbsoluteDecompositionGroup K v)

def

finitePlaceAbsoluteMuPH1AdicCoordinate

L435 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1AdicCoordinate

Documentation

Degree-one natural-coefficient classes on the decomposition group, expressed in the local ZMod p coordinate.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAbsoluteMuPH1AdicCoordinate
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty) :
    continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep K p v) →ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup K v)

def

finitePlaceAdicH1Restriction

L450 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicH1Restriction

Documentation

Pull intrinsic local continuous H¹ back to the selected decomposition group through the concrete decomposition--adic Galois map.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAdicH1Restriction
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    ContinuousH1ZMod
        (p := p) (G := Field.absoluteGaloisGroup (v.adicCompletion K)) →ₗ[ZMod p]
      ContinuousH1ZMod
        (p := p) (G := finitePlaceAbsoluteDecompositionGroup K v)

theorem

finitePlaceAdicH1Restriction_apply

L475 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicH1Restriction_apply

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAdicH1Restriction_apply
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (chi : ContinuousH1ZMod
      (p := p) (G := Field.absoluteGaloisGroup (v.adicCompletion K)))
    (sigma : finitePlaceAbsoluteDecompositionGroup K v) :
    finitePlaceAdicH1Restriction K p v chi (Additive.ofMul sigma) =
      chi (Additive.ofMul
        (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma))

theorem

finitePlaceAbsoluteMuPAdicCoordinate_rootCocycle

L489 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPAdicCoordinate_rootCocycle

Documentation

On Kummer root cocycles, the actual local coefficient coordinate agrees with the intrinsic root cocycle of the localized unit.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPAdicCoordinate_rootCocycle
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) (sigma : finitePlaceAbsoluteDecompositionGroup K v) :
    finitePlaceAbsoluteMuPAdicCoordinate K p v hmu
        (absoluteKummerMuPRootCocycle K p a sigma.1) =
      absoluteMuPLinearEquivZMod (v.adicCompletion K) p hmu
        (absoluteKummerMuPRootCocycle (v.adicCompletion K) p
          (Units.map (algebraMap K (v.adicCompletion K)).toMonoidHom a)
          (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma))

def

finitePlaceAdicKummerH1OfGlobalUnit

L560 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicKummerH1OfGlobalUnit

Documentation

The intrinsic local Kummer class of a global unit, pulled back to the selected decomposition group.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

def finitePlaceAdicKummerH1OfGlobalUnit
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) :
    ContinuousH1ZMod
      (p := p) (G := finitePlaceAbsoluteDecompositionGroup K v)

theorem

finitePlaceAdicKummerH1OfGlobalUnit_apply

L576 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAdicKummerH1OfGlobalUnit_apply

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAdicKummerH1OfGlobalUnit_apply
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) (sigma : finitePlaceAbsoluteDecompositionGroup K v) :
    finitePlaceAdicKummerH1OfGlobalUnit K p v hmu a
        (Additive.ofMul sigma) =
      absoluteMuPLinearEquivZMod (v.adicCompletion K) p hmu
        (absoluteKummerMuPRootCocycle (v.adicCompletion K) p
          (Units.map (algebraMap K (v.adicCompletion K)).toMonoidHom a)
          (finitePlaceDecompositionToAdicAbsoluteGaloisGroup K v sigma))

theorem

finitePlaceAbsoluteMuPCocyclesMap_kummer_eq_adic

L598 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPCocyclesMap_kummer_eq_adic

Documentation

Mapping the restricted natural Kummer cocycle through the actual local coefficient coordinate gives the intrinsic local Kummer cocycle pulled back to the decomposition group.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPCocyclesMap_kummer_eq_adic
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) :
    ContinuousCohomology.cocyclesMap
        (ContinuousMonoidHom.id (finitePlaceAbsoluteDecompositionGroup K v))
        (finitePlaceAbsoluteMuPAdicCoordinateHom K p v hmu) 1
        (finitePlaceAbsoluteKummerMuPHomogeneousOneCocycle K p v a) =
      ClassFieldTower.Cohomology.cocycleOfH1
        (finitePlaceAdicKummerH1OfGlobalUnit K p v hmu a)

theorem

finitePlaceAbsoluteMuPH1AdicCoordinate_kummerClass

L667 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1AdicCoordinate_kummerClass

Documentation

The localized natural Kummer class becomes the intrinsic local Kummer class after applying the actual algebraic-localization coordinate.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPH1AdicCoordinate_kummerClass
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) :
    finitePlaceAbsoluteMuPH1AdicCoordinate K p v hmu
        (finitePlaceAbsoluteKummerMuPH1Class K p v a) =
      finitePlaceAdicKummerH1OfGlobalUnit K p v hmu a

theorem

finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic_mk

L690 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic_mk

Documentation

The comparison on a represented global power class.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic_mk
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty)
    (a : Kˣ) :
    finitePlaceAbsoluteMuPH1AdicCoordinate K p v hmu
        (finitePlaceAbsoluteKummerMuPH1LinearMap K p v
          (Additive.ofMul
            (QuotientGroup.mk' (powMonoidHom p : Kˣ →* Kˣ).range a))) =
      finitePlaceAdicH1Restriction K p v
        (absoluteKummerContinuousH1LinearEquiv (v.adicCompletion K) p hmu
          (finitePlacePowerClassLocalization K p v
            (Additive.ofMul
              (QuotientGroup.mk'
                (powMonoidHom p : Kˣ →* Kˣ).range a))))

theorem

finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic

L712 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic

Documentation

Linear-map form of the finite-place natural/intrinsic Kummer comparison for any number field whose completion contains the required roots of unity.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceAbsoluteMuPKummerH1LinearMap_compare_adic
    (K : Type) [Field K] [NumberField K]
    (p : ℕ) [Fact p.Prime]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers K))
    (hmu : (primitiveRoots p (v.adicCompletion K)).Nonempty) :
    (finitePlaceAbsoluteMuPH1AdicCoordinate K p v hmu).comp
        (finitePlaceAbsoluteKummerMuPH1LinearMap K p v) =
      (finitePlaceAdicH1Restriction K p v).comp
        ((absoluteKummerContinuousH1LinearEquiv
          (v.adicCompletion K) p hmu).toLinearMap.comp
          (finitePlacePowerClassLocalization K p v))

theorem

finitePlaceCyclotomicMuPKummerH1LinearMap_compare

L739 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceCyclotomicMuPKummerH1LinearMap_compare

Documentation

Over the cyclotomic base, the natural finite-place Kummer map and the existing intrinsic completion Kummer equivalence agree after transport to the common decomposition-group H¹ coordinate.

Source context 13 commands

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

open NumberField IsDedekindDomain
open scoped NumberField Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open CategoryTheory ClassFieldTower.Cohomology ClassFieldTower.ProP
open ContRepresentation KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance finitePlaceCyclotomicComparisonCanonicalZModAddCommGroup : AddCommGroup (ZMod p) :=
  (ZMod.instField p).toDivisionRing.toAddCommGroup
local instance finitePlaceCyclotomicComparisonFiniteDimensional :
    FiniteDimensional F (FinitePlaceCyclotomicBase F p) :=
  finiteDimensional_idealRadicalCyclotomicBase
    F p (Fact.out : p.Prime)
local instance finitePlaceCyclotomicComparisonNumberField :
    NumberField (FinitePlaceCyclotomicBase F p) :=
  NumberField.of_module_finite F (FinitePlaceCyclotomicBase F p)
local instance finitePlaceCyclotomicComparisonH1Module
    {q : ℕ} {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Module (ZMod q) (ContinuousH1ZMod (p := q) (G := G)) :=
  continuousH1ZModModule

Lean source · statement

theorem finitePlaceCyclotomicMuPKummerH1LinearMap_compare
    (v : HeightOneSpectrum
      (NumberField.RingOfIntegers (FinitePlaceCyclotomicBase F p))) :
    (finitePlaceAbsoluteMuPH1AdicCoordinate
      (FinitePlaceCyclotomicBase F p) p v
      (finitePlaceCyclotomicCompletion_primitiveRoots_nonempty F p v)).comp
        (finitePlaceAbsoluteKummerMuPH1LinearMap
          (FinitePlaceCyclotomicBase F p) p v) =
      (finitePlaceAdicH1Restriction
        (FinitePlaceCyclotomicBase F p) p v).comp
        ((finitePlaceCyclotomicCompletionKummerH1LinearEquiv
          F p v).toLinearMap.comp
          (finitePlacePowerClassLocalization
            (FinitePlaceCyclotomicBase F p) p v))

Module documentation

Finite-place comparison of natural and intrinsic-local Kummer H¹

Declarations