Module

FinitePlaceH2LocalizationFamily.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceH2LocalizationFamily

3 declarations indexed from sourceView source ↗

Module documentation

The family of finite-place degree-two localization maps

The restriction maps to all absolute decomposition subgroups are assembled into one linear map with dependent function codomain.

Imports2

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceH2Localization
Mathlib.LinearAlgebra.Pi

Imported by2

abbrev

FinitePlaceH2LocalizationTarget

ClassFieldTower.Martinet.Shafarevich.FinitePlaceH2LocalizationTarget

Documentation

The product of degree-two continuous cohomology spaces of the finite-place absolute decomposition subgroups.

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.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

abbrev FinitePlaceH2LocalizationTarget

def

finitePlaceH2LocalizationFamily

ClassFieldTower.Martinet.Shafarevich.finitePlaceH2LocalizationFamily

Documentation

Simultaneous restriction of an absolute degree-two class to every finite-place decomposition subgroup.

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.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

def finitePlaceH2LocalizationFamily :
    continuousCohomologyZModPLifted p (Field.absoluteGaloisGroup F) 2 →ₗ[ZMod p]
      FinitePlaceH2LocalizationTarget F p

theorem

finitePlaceH2LocalizationFamily_apply

ClassFieldTower.Martinet.Shafarevich.finitePlaceH2LocalizationFamily_apply

Documentation

Each component of the family map is the corresponding finite-place localization.

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.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

theorem finitePlaceH2LocalizationFamily_apply
    (x : continuousCohomologyZModPLifted p (Field.absoluteGaloisGroup F) 2)
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceH2LocalizationFamily F p x v =
      finitePlaceH2Localization F p v x