Module

FinitePlaceMuPKummerRamificationFiniteSupport.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.FinitePlaceMuPKummerRamificationFiniteSupport

5 declarations indexed from sourceView source ↗

Module documentation

Finite ramification support for natural `mu_p` Kummer classes

A represented global power class can ramify only where its representative or the exponent p fails to be a unit. Both exceptional sets are finite. This packages the resulting finite-support statement for every natural-coefficient Kummer class.

Imports2

Imported by1

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.All

def

finitePlaceKummerPrimeUnit

L32 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceKummerPrimeUnit

Documentation

The field unit represented by the prime exponent p.

Source context 7 commands

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

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

Lean source · statement

def finitePlaceKummerPrimeUnit : Kˣ

def

finitePlaceAbsoluteKummerMuPBadPlaces

L40 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPBadPlaces

Documentation

A finite set containing every possible ramified finite place of the Kummer class represented by a.

Source context 9 commands

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

open NumberField IsDedekindDomain
open scoped NumberField
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
open scoped Classical in
include p in

Lean source · statement

def finitePlaceAbsoluteKummerMuPBadPlaces (a : Kˣ) :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_eq_zero_of_not_mem_badPlaces

L47 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_eq_zero_of_not_mem_badPlaces

Documentation

Outside the finite bad-place set, the inertia component of a represented natural-mu_p Kummer class vanishes.

Source context 7 commands

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

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

Lean source · statement

theorem finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_eq_zero_of_not_mem_badPlaces
    (hmu : (primitiveRoots p K).Nonempty) (a : Kˣ)
    (v : HeightOneSpectrum (𝓞 K))
    (hv : v ∉ finitePlaceAbsoluteKummerMuPBadPlaces K p a) :
    finitePlaceAbsoluteKummerMuPH1RamificationLinearMap K p v
        (Additive.ofMul
          (QuotientGroup.mk'
            (powMonoidHom p : Kˣ →* Kˣ).range a)) = 0

theorem

finitePlaceAbsoluteKummerMuPH1Ramification_exists_finset

L83 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1Ramification_exists_finset

Documentation

Every natural-mu_p Kummer class has only finitely many possibly nonzero inertia components.

Source context 7 commands

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

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

Lean source · statement

theorem finitePlaceAbsoluteKummerMuPH1Ramification_exists_finset
    (hmu : (primitiveRoots p K).Nonempty)
    (x : absolutePowerClassModP K p) :
    ∃ S : Finset (HeightOneSpectrum (𝓞 K)), ∀ v, v ∉ S →
      finitePlaceAbsoluteKummerMuPH1RamificationLinearMap K p v x = 0

theorem

finitePlaceAbsoluteKummerMuPH1Ramification_support_finite

L103 ↗

ClassFieldTower.Martinet.Shafarevich.finitePlaceAbsoluteKummerMuPH1Ramification_support_finite

Documentation

The set of finite places where a natural-mu_p Kummer class has a nonzero inertia component is finite.

Source context 7 commands

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

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

Lean source · statement

theorem finitePlaceAbsoluteKummerMuPH1Ramification_support_finite
    (hmu : (primitiveRoots p K).Nonempty)
    (x : absolutePowerClassModP K p) :
    Set.Finite {v : HeightOneSpectrum (𝓞 K) |
      finitePlaceAbsoluteKummerMuPH1RamificationLinearMap K p v x ≠ 0}

Module documentation

Finite ramification support for natural mu_p Kummer classes

Declarations

finitePlaceKummerPrimeUnit

finitePlaceAbsoluteKummerMuPBadPlaces

finitePlaceAbsoluteKummerMuPH1RamificationLinearMap_eq_zero_of_not_mem_badPlaces

finitePlaceAbsoluteKummerMuPH1Ramification_exists_finset

finitePlaceAbsoluteKummerMuPH1Ramification_support_finite

Finite ramification support for natural `mu_p` Kummer classes