Module

GlobalCompositumValuationInertiaBound.lean

Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumValuationInertiaBound

2 declarations indexed from sourceView source ↗

Module documentation

The fixed-conductor local inertia bound for the auxiliary compositum

At each chosen ramified prime, the localization of the single global compositum embeds in the common local cyclotomic field whose p-power part is exactly the exponent selected from L. The arbitrary-coprime local bound therefore gives the sharp factor φ(p^e).

Imports2

Imported by3

def

kroneckerWeberGlobalCompositumValuationInertiaCard

L33 ↗

KroneckerWeber.kroneckerWeberGlobalCompositumValuationInertiaCard

Documentation

The cardinality of the valuation-theoretic inertia group of the fixed global compositum at its synchronized place above p. Naming this natural number keeps the completion/localization type out of later declaration types.

Source context 6 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory.Valuations
open HilbertRamification
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

def kroneckerWeberGlobalCompositumValuationInertiaCard
    (p : Nat.Primes) [Fact p.1.Prime]
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) : ℕ

theorem

kroneckerWeberGlobalCompositumValuationInertiaCard_le

L48 ↗

KroneckerWeber.kroneckerWeberGlobalCompositumValuationInertiaCard_le