Module

FinitePlaceH2Localization.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.FinitePlaceH2Localization

6 declarations indexed from sourceView source ↗

Module documentation

Degree-two localization at a finite place

For a number field and a finite place, the chosen extension of the adic absolute value to the algebraic closure defines an absolute decomposition subgroup. Its continuous inclusion in the absolute Galois group induces the actual restriction map on degree-two continuous cohomology.

This file deliberately stops at the decomposition-group target. Identifying that target with the absolute Galois group of the completed field requires a topological local--global Galois comparison which is not presently available in the imported libraries.

Imports5

Imported by17

def

finitePlaceAbsoluteValueExtension

L39 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteValueExtension

Documentation

The chosen extension of the finite-place absolute value to the algebraic closure.

Source context 8 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 AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

def finitePlaceAbsoluteValueExtension
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    AbsoluteValueExtension
      (NumberField.HeightOneSpectrum.adicAbv F v) (AlgebraicClosure F)

abbrev

finitePlaceAbsoluteDecompositionGroup

L48 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteDecompositionGroup

Documentation

The decomposition subgroup of the absolute Galois group selected by a finite place.

Source context 8 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 AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

abbrev finitePlaceAbsoluteDecompositionGroup
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))

def

finitePlaceAbsoluteDecompositionInclusion

L54 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteDecompositionInclusion

Documentation

The continuous inclusion of the selected decomposition subgroup in the absolute Galois group.

Source context 8 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 AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

def finitePlaceAbsoluteDecompositionInclusion
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F)) :
    finitePlaceAbsoluteDecompositionGroup F v →ₜ* Field.absoluteGaloisGroup F

theorem

finitePlaceAbsoluteDecompositionInclusion_apply

L62 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteDecompositionInclusion_apply

Source context 8 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 AlgebraicNumberTheory.Valuations
open ClassFieldTower.Cohomology
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ)

Lean source · statement

theorem finitePlaceAbsoluteDecompositionInclusion_apply
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteDecompositionGroup F v) :
    finitePlaceAbsoluteDecompositionInclusion F v sigma = sigma.1

def