Module

FinitePlaceMuPKummerTameUnramified.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FinitePlaceMuPKummerTameUnramified

4 declarations indexed from sourceView source ↗

Module documentation

Tame unramifiedness of finite-place natural `mu_p` Kummer classes

Away from a prescribed finite set and from the residue characteristics dividing p, an S-unit Kummer extension is unramified. This file applies that arithmetic statement to the chosen algebraic-closure root defining the natural-mu_p Kummer cocycle. Absolute inertia therefore fixes the root, so the inertia-restricted cocycle, and hence its continuous H¹ class, vanish.

Imports4

Imported by2

theorem

finitePlaceAbsoluteInertia_fixes_absoluteKummerChosenRoot_of_sUnit

L37 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteInertia_fixes_absoluteKummerChosenRoot_of_sUnit

Documentation

At a tame place outside S, absolute inertia fixes the chosen root used to define the natural-mu_p Kummer cocycle of an S-unit.

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 KummerTheory TopRep
variable (K : Type) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlaceAbsoluteInertia_fixes_absoluteKummerChosenRoot_of_sUnit
    (hmu : (primitiveRoots p K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : SUnitGroup (K := K) S)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ S)
    (hp : v.valuation K (p : K) = 1)
    (sigma : finitePlaceAbsoluteInertiaSubgroup K v) :
    sigma.1.1 • absoluteKummerChosenRoot K p a.1 =
      absoluteKummerChosenRoot K p a.1

theorem

absoluteKummerMuPRootCocycle_eq_zero_on_inertia_of_sUnit

L115 ↗

ClassFieldTower.Martinet.Shafarevich.absoluteKummerMuPRootCocycle_eq_zero_on_inertia_of_sUnit

Documentation

The natural-mu_p Kummer root cocycle of an S-unit vanishes on absolute inertia at a tame place outside S.

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 KummerTheory TopRep
variable (K : Type) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem absoluteKummerMuPRootCocycle_eq_zero_on_inertia_of_sUnit
    (hmu : (primitiveRoots p K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : SUnitGroup (K := K) S)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ S)
    (hp : v.valuation K (p : K) = 1)
    (sigma : finitePlaceAbsoluteInertiaSubgroup K v) :
    absoluteKummerMuPRootCocycle K p a.1
        (finitePlaceAbsoluteDecompositionInclusion K v
          (finitePlaceAbsoluteInertiaInclusion K v sigma)) = 0

theorem

finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle_eq_zero_of_sUnit

L135 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle_eq_zero_of_sUnit

Documentation

The inertia-restricted homogeneous natural-mu_p Kummer cocycle of an S-unit is zero at a tame place outside S.

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 KummerTheory TopRep
variable (K : Type) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle_eq_zero_of_sUnit
    (hmu : (primitiveRoots p K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : SUnitGroup (K := K) S)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ S)
    (hp : v.valuation K (p : K) = 1) :
    finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle K p v a.1 = 0

theorem

finitePlaceAbsoluteKummerMuPInertiaH1Class_eq_zero_of_sUnit

L183 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPInertiaH1Class_eq_zero_of_sUnit

Documentation

At a tame place outside S, the inertia-localized natural-mu_p Kummer H¹ class of an S-unit vanishes.

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 KummerTheory TopRep
variable (K : Type) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

theorem finitePlaceAbsoluteKummerMuPInertiaH1Class_eq_zero_of_sUnit
    (hmu : (primitiveRoots p K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (a : SUnitGroup (K := K) S)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ S)
    (hp : v.valuation K (p : K) = 1) :
    finitePlaceAbsoluteKummerMuPInertiaH1Class K p v a.1 = 0

Module documentation

Tame unramifiedness of finite-place natural mu_p Kummer classes

Declarations

finitePlaceAbsoluteInertia_fixes_absoluteKummerChosenRoot_of_sUnit

absoluteKummerMuPRootCocycle_eq_zero_on_inertia_of_sUnit

finitePlaceAbsoluteKummerMuPInertiaHomogeneousOneCocycle_eq_zero_of_sUnit

finitePlaceAbsoluteKummerMuPInertiaH1Class_eq_zero_of_sUnit

Tame unramifiedness of finite-place natural `mu_p` Kummer classes