Module

FinitePlaceAbsoluteInertiaKernel.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FinitePlaceAbsoluteInertiaKernel

2 declarations indexed from sourceView source ↗

Module documentation

Absolute finite-place inertia and the unramified kernel

This file compares the chosen absolute inertia subgroup at a finite place with finite Galois subextensions of the algebraic closure. The finite-level restriction statement is the arithmetic input for showing that absolute inertia fixes the maximal everywhere-unramified pro-p extension.

Imports4

Imported by6

theorem

finitePlaceAbsoluteInertia_restrictNormal_mem_finiteInertia

L34 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertia_restrictNormal_mem_finiteInertia

Documentation

Restricting an element of the chosen absolute inertia group to a finite Galois subextension puts it in the inertia group at the induced finite place.

Source context 6 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
variable (F : Type) [Field F] [NumberField F]

Lean source · statement

theorem finitePlaceAbsoluteInertia_restrictNormal_mem_finiteInertia
    (M : IntermediateField F (AlgebraicClosure F))
    [FiniteDimensional F M] [IsGalois F M] [NumberField M]
    (v : HeightOneSpectrum (NumberField.RingOfIntegers F))
    (sigma : finitePlaceAbsoluteInertiaSubgroup F v) :
    (sigma.1.1 : AlgebraicClosure F ≃ₐ[F] AlgebraicClosure F).restrictNormal M ∈
      HilbertRamification.Dedekind.inertiaGroup
        (finitePlaceExtensionCentre
          (K := F) (L := M) v
          (restrictAbsoluteValueExtensionToIntermediate
            (HeightOneSpectrum.adicAbv F v)
            (finitePlaceAbsoluteValueExtension F v) M)).asIdeal
        (M ≃ₐ[F] M)

theorem

finitePlaceAbsoluteInertia_mem_absoluteUnramifiedKernel

L106 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertia_mem_absoluteUnramifiedKernel