NYLL
Module

FinitePlaceMuPH1RamificationLocalization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FinitePlaceMuPH1RamificationLocalization
19 declarations indexed from sourceView source ↗

Module documentation

Finite-place ramification of natural mu_p Kummer classes

The natural mu_p representation on a chosen finite-place decomposition group restricts further to absolute inertia. This file packages the induced map on continuous H¹, its unramified kernel, and the family of inertia restrictions of natural-coefficient Kummer classes over all finite places.

Imports3
Imported by2

Declarations

abbrev

finitePlaceAbsoluteInertiaMuPTopRep

L34 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertiaMuPTopRep
Documentation

The natural mu_p representation restricted from decomposition to absolute inertia at v.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteInertiaMuPTopRep
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    TopRep (ZMod p) (finitePlaceAbsoluteInertiaSubgroup F v)
abbrev

finitePlaceAbsoluteMuPInertiaRestrictionHom

L44 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPInertiaRestrictionHom
Documentation

The identity coefficient morphism from the literal inertia restriction.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteMuPInertiaRestrictionHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    TopRep.res
        (finitePlaceAbsoluteInertiaInclusion F v :
          finitePlaceAbsoluteInertiaSubgroup F v →*
            finitePlaceAbsoluteDecompositionGroup F v)
        (finitePlaceAbsoluteMuPTopRep F p v) ⟶
      finitePlaceAbsoluteInertiaMuPTopRep F p v
abbrev

finitePlaceAbsoluteMuPInertiaCocyclesMap

L56 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPInertiaCocyclesMap
Documentation

Restriction of natural-coefficient degree-one cocycles from decomposition to inertia.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteMuPInertiaCocyclesMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousCohomology.cocycles (finitePlaceAbsoluteMuPTopRep F p v) 1 ⟶
      ContinuousCohomology.cocycles
        (finitePlaceAbsoluteInertiaMuPTopRep F p v) 1
abbrev

finitePlaceAbsoluteMuPH1InertiaRestrictionHom

L66 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1InertiaRestrictionHom
Documentation

The categorical restriction on natural-coefficient continuous H¹.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteMuPH1InertiaRestrictionHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v) ⟶
      continuousCohomology 1
        (finitePlaceAbsoluteInertiaMuPTopRep F p v)
def

finitePlaceAbsoluteMuPH1InertiaRestriction

L76 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1InertiaRestriction
Documentation

Restriction from decomposition to inertia as a ZMod p-linear map.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def finitePlaceAbsoluteMuPH1InertiaRestriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v) →ₗ[ZMod p]
      continuousCohomology 1
        (finitePlaceAbsoluteInertiaMuPTopRep F p v)
theorem

finitePlaceAbsoluteMuPH1InertiaRestriction_quotientMap

L85 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1InertiaRestriction_quotientMap
Documentation

Inertia restriction sends a cocycle class to the class of its restricted cocycle.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem finitePlaceAbsoluteMuPH1InertiaRestriction_quotientMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (z : ContinuousCohomology.cocycles
      (finitePlaceAbsoluteMuPTopRep F p v) 1) :
    finitePlaceAbsoluteMuPH1InertiaRestriction F p v
        (ContinuousCohomology.π
          (finitePlaceAbsoluteMuPTopRep F p v) 1 z) =
      ContinuousCohomology.π
        (finitePlaceAbsoluteInertiaMuPTopRep F p v) 1
        (finitePlaceAbsoluteMuPInertiaCocyclesMap F p v z)
abbrev

finitePlaceAbsoluteMuPUnramifiedH1

L102 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPUnramifiedH1
Documentation

Natural-coefficient classes on decomposition that are unramified at v: those whose inertia restriction vanishes.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteMuPUnramifiedH1
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    Submodule (ZMod p)
      (continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v))
theorem

mem_finitePlaceAbsoluteMuPUnramifiedH1_iff

L108 ↗
ClassFieldTower.Martinet.Shafarevich.mem_finitePlaceAbsoluteMuPUnramifiedH1_iff
Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem mem_finitePlaceAbsoluteMuPUnramifiedH1_iff
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (x : continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v)) :
    x ∈ finitePlaceAbsoluteMuPUnramifiedH1 F p v ↔
      finitePlaceAbsoluteMuPH1InertiaRestriction F p v x = 0
abbrev

finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle

L116 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle
Documentation

The localized absolute Kummer cocycle restricted further to inertia.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    ContinuousCohomology.cocycles
      (finitePlaceAbsoluteInertiaMuPTopRep F p v) 1
def

finitePlaceAbsoluteKummerMuPInertiaH1Class

L124 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPInertiaH1Class
Documentation

The inertia-localized natural-coefficient Kummer H¹ class.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def finitePlaceAbsoluteKummerMuPInertiaH1Class
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    continuousCohomology 1
      (finitePlaceAbsoluteInertiaMuPTopRep F p v)
theorem

finitePlaceAbsoluteMuPH1InertiaRestriction_kummerClass

L134 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1InertiaRestriction_kummerClass
Documentation

Inertia restriction of a localized Kummer class is represented by the restricted Kummer cocycle.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem finitePlaceAbsoluteMuPH1InertiaRestriction_kummerClass
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    finitePlaceAbsoluteMuPH1InertiaRestriction F p v
        (finitePlaceAbsoluteKummerMuPH1Class F p v a) =
      finitePlaceAbsoluteKummerMuPInertiaH1Class F p v a
def

finitePlaceAbsoluteKummerMuPH1RamificationLinearMap

L143 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationLinearMap
Documentation

The ramification component of the natural Kummer map at v.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def finitePlaceAbsoluteKummerMuPH1RamificationLinearMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absolutePowerClassModP F p →ₗ[ZMod p]
      continuousCohomology 1
        (finitePlaceAbsoluteInertiaMuPTopRep F p v)
theorem

finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_mk

L154 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_mk
Documentation

Evaluation on a represented power class is its inertia-localized Kummer class.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_mk
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    finitePlaceAbsoluteKummerMuPH1RamificationLinearMap F p v
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Fˣ →* Fˣ).range a)) =
      finitePlaceAbsoluteKummerMuPInertiaH1Class F p v a
abbrev

FinitePlaceMuPH1RamificationLocalizationTarget

L170 ↗
ClassFieldTower.Martinet.Shafarevich.FinitePlaceMuPH1RamificationLocalizationTarget
Documentation

The dependent product of natural-coefficient inertia H¹ spaces.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev FinitePlaceMuPH1RamificationLocalizationTarget
def

finitePlaceAbsoluteKummerMuPH1RamificationFamily

L176 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationFamily
Documentation

All finite-place inertia components of the natural Kummer map.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
def finitePlaceAbsoluteKummerMuPH1RamificationFamily :
    absolutePowerClassModP F p →ₗ[ZMod p]
      FinitePlaceMuPH1RamificationLocalizationTarget F p
theorem

finitePlaceAbsoluteKummerMuPH1RamificationFamily_apply

L184 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationFamily_apply
Documentation

Each component of the family is the ramification map at that place.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem finitePlaceAbsoluteKummerMuPH1RamificationFamily_apply
    (x : absolutePowerClassModP F p)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteKummerMuPH1RamificationFamily F p x v =
      finitePlaceAbsoluteKummerMuPH1RamificationLinearMap F p v x
theorem

finitePlaceAbsoluteKummerMuPH1RamificationFamily_mk

L194 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationFamily_mk
Documentation

On a represented global power class, the family consists of its inertia-localized Kummer classes.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · full declaration
theorem finitePlaceAbsoluteKummerMuPH1RamificationFamily_mk
    (a : Fˣ) :
    finitePlaceAbsoluteKummerMuPH1RamificationFamily F p
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Fˣ →* Fˣ).range a)) =
      fun v ↦ finitePlaceAbsoluteKummerMuPInertiaH1Class F p v a := by
  funext v
  change finitePlaceAbsoluteKummerMuPH1RamificationLinearMap F p v
      (Additive.ofMul
        (QuotientGroup.mk'
          (powMonoidHom p : Fˣ →* Fˣ).range a)) = _
  rw [finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_mk]
abbrev

finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses

L210 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses
Documentation

Global power classes whose natural Kummer class is unramified at every finite place.

Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
abbrev finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses :
    Submodule (ZMod p) (absolutePowerClassModP F p)
theorem

mem_finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses_iff

L214 ↗
ClassFieldTower.Martinet.Shafarevich.mem_finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses_iff
Source context 7 commands

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

open CategoryTheory NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory TopRep
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
Lean source · statement
theorem mem_finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses_iff
    (x : absolutePowerClassModP F p) :
    x ∈ finitePlaceAbsoluteKummerMuPEverywhereUnramifiedPowerClasses F p ↔
      ∀ v, finitePlaceAbsoluteKummerMuPH1RamificationLinearMap F p v x = 0

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