NYLL
Module

FinitePlaceMuPH1Localization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Kummer.FinitePlaceMuPH1Localization
11 declarations indexed from sourceView source ↗

Module documentation

Finite-place restriction of natural mu_p Kummer classes

The natural mu_p representation of the absolute Galois group restricts to each chosen finite-place decomposition subgroup. This file packages the induced map on continuous H¹ and composes it with the linear Kummer map from global power classes.

Imports3
Imported by3

Declarations

abbrev

finitePlaceAbsoluteMuPTopRep

L32 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPTopRep
Documentation

The natural mu_p representation restricted to the chosen decomposition subgroup 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 finitePlaceAbsoluteMuPTopRep
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    TopRep (ZMod p) (finitePlaceAbsoluteDecompositionGroup F v)
abbrev

finitePlaceAbsoluteMuPRestrictionHom

L42 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPRestrictionHom
Documentation

The identity coefficient morphism from the literal restricted representation.

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 finitePlaceAbsoluteMuPRestrictionHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    TopRep.res
        (finitePlaceAbsoluteDecompositionInclusion F v :
          finitePlaceAbsoluteDecompositionGroup F v →*
            Field.absoluteGaloisGroup F)
        (absoluteMuPTopRep F p) ⟶
      finitePlaceAbsoluteMuPTopRep F p v
abbrev

finitePlaceAbsoluteMuPCocyclesMap

L53 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPCocyclesMap
Documentation

Restriction of natural-coefficient degree-one cocycles.

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 finitePlaceAbsoluteMuPCocyclesMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    ContinuousCohomology.cocycles (absoluteMuPTopRep F p) 1 ⟶
      ContinuousCohomology.cocycles (finitePlaceAbsoluteMuPTopRep F p v) 1
abbrev

finitePlaceAbsoluteMuPH1RestrictionHom

L62 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1RestrictionHom
Documentation

Restriction of natural-coefficient continuous H¹ to the decomposition subgroup.

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 finitePlaceAbsoluteMuPH1RestrictionHom
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    continuousCohomology 1 (absoluteMuPTopRep F p) ⟶
      continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v)
def

finitePlaceAbsoluteMuPH1Restriction

L71 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1Restriction
Documentation

Restriction of natural-coefficient continuous H¹, viewed 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 finitePlaceAbsoluteMuPH1Restriction
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    continuousCohomology 1 (absoluteMuPTopRep F p) →ₗ[ZMod p]
      continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v)
theorem

finitePlaceAbsoluteMuPH1Restriction_quotientMap

L78 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1Restriction_quotientMap
Documentation

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 finitePlaceAbsoluteMuPH1Restriction_quotientMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (z : ContinuousCohomology.cocycles (absoluteMuPTopRep F p) 1) :
    finitePlaceAbsoluteMuPH1Restriction F p v
        (ContinuousCohomology.π (absoluteMuPTopRep F p) 1 z) =
      ContinuousCohomology.π (finitePlaceAbsoluteMuPTopRep F p v) 1
        (finitePlaceAbsoluteMuPCocyclesMap F p v z)
abbrev

finitePlaceAbsoluteKummerMuPHomogeneousOneCocycle

L91 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPHomogeneousOneCocycle
Documentation

The absolute Kummer cocycle restricted to the decomposition subgroup 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 finitePlaceAbsoluteKummerMuPHomogeneousOneCocycle
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    ContinuousCohomology.cocycles (finitePlaceAbsoluteMuPTopRep F p v) 1
def

finitePlaceAbsoluteKummerMuPH1Class

L98 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1Class
Documentation

The natural-coefficient Kummer H¹ class localized at the decomposition subgroup.

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 finitePlaceAbsoluteKummerMuPH1Class
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v)
theorem

finitePlaceAbsoluteMuPH1Restriction_absoluteKummerMuPH1Class

L105 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteMuPH1Restriction_absoluteKummerMuPH1Class
Documentation

Localization of the absolute Kummer class is its restricted cocycle 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 finitePlaceAbsoluteMuPH1Restriction_absoluteKummerMuPH1Class
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    finitePlaceAbsoluteMuPH1Restriction F p v
        (absoluteKummerMuPH1Class F p a) =
      finitePlaceAbsoluteKummerMuPH1Class F p v a
def

finitePlaceAbsoluteKummerMuPH1LinearMap

L114 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1LinearMap
Documentation

Natural-coefficient Kummer localization as a linear map from global power 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 · statement
def finitePlaceAbsoluteKummerMuPH1LinearMap
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    absolutePowerClassModP F p →ₗ[ZMod p]
      continuousCohomology 1 (finitePlaceAbsoluteMuPTopRep F p v)
theorem

finitePlaceAbsoluteKummerMuPH1LinearMap_mk

L123 ↗
ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1LinearMap_mk
Documentation

Evaluation on a represented power class is the localized natural 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 finitePlaceAbsoluteKummerMuPH1LinearMap_mk
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) (a : Fˣ) :
    finitePlaceAbsoluteKummerMuPH1LinearMap F p v
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Fˣ →* Fˣ).range a)) =
      finitePlaceAbsoluteKummerMuPH1Class F p v a

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