Module

AbsoluteUnramifiedH2LocalizationKernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.AbsoluteUnramifiedH2LocalizationKernel

3 declarations indexed from sourceView source ↗

Module documentation

Absolute unramified degree two in the localization kernel

Inflation from the maximal everywhere-unramified pro-p quotient has zero restriction at every finite place. This file bundles that source theorem as a linear map into the kernel of simultaneous localization.

Imports1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FinitePlaceUnramifiedH2LocalizationVanishing

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

def

absoluteUnramifiedH2InflationToLocalizationKernel

L32 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2InflationToLocalizationKernel

Documentation

Inflation of an everywhere-unramified degree-two class, bundled in the kernel of simultaneous finite-place localization.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

def absoluteUnramifiedH2InflationToLocalizationKernel :
    continuousCohomologyZModPLifted p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) 2 →ₗ[ZMod p]
      LinearMap.ker (finitePlaceH2LocalizationFamily F p)

theorem

absoluteUnramifiedH2InflationToLocalizationKernel_apply

L46 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2InflationToLocalizationKernel_apply

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedH2InflationToLocalizationKernel_apply
    (x : continuousCohomologyZModPLifted p
      (MaxEverywhereUnramifiedProPGaloisGroup F p) 2) :
    (absoluteUnramifiedH2InflationToLocalizationKernel F p x).1 =
      absoluteUnramifiedH2Inflation F p x

theorem

absoluteUnramifiedH2Inflation_range_le_localization_ker

L55 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteUnramifiedH2Inflation_range_le_localization_ker

Documentation

The entire absolute inflation range lies in the finite-place localization kernel.

Source context 8 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Cohomology
open ClassFieldTower.Martinet
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteUnramifiedH2Inflation_range_le_localization_ker :
    LinearMap.range (absoluteUnramifiedH2Inflation F p) ≤
      LinearMap.ker (finitePlaceH2LocalizationFamily F p)

Module documentation

Absolute unramified degree two in the localization kernel

Declarations

absoluteUnramifiedH2InflationToLocalizationKernel

absoluteUnramifiedH2InflationToLocalizationKernel_apply

absoluteUnramifiedH2Inflation_range_le_localization_ker