Module

PadicCyclotomicInertiaBound.lean

Nyll.ClassFieldTheory.RamificationTheory.HilbertRamification.PadicCyclotomicInertiaBound

2 declarations indexed from sourceView source ↗

Module documentation

Canonical p-adic inertia bounds

This file identifies the inertia cardinality of the canonical valuation on a finite Galois extension of ℚ_p with the intrinsic value-group ramification index, then applies the prime-power cyclotomic ramification bound.

Imports4

Imported by2

theorem

natCard_padicCanonicalInertia_eq_exponentialRamificationIndex

L30 ↗

HilbertRamification.natCard_padicCanonicalInertia_eq_exponentialRamificationIndex

Documentation

For a finite Galois extension of ℚ_p, the inertia group of the canonical norm-formula valuation has cardinality equal to the intrinsic ramification index.

Source context 4 commands

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

noncomputable section
namespace HilbertRamification
open AlgebraicNumberTheory.Valuations
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem natCard_padicCanonicalInertia_eq_exponentialRamificationIndex
    (p : ℕ) [Fact p.Prime]
    (E : Type) [Field E] [Algebra ℚ_[p] E]
    [FiniteDimensional ℚ_[p] E] [IsGalois ℚ_[p] E] :
    Nat.card
        (RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup ℚ_[p]
          (absoluteValueValuationSubring
            (padicFiniteExtensionAbsoluteValue p E)
            (padicFiniteExtensionAbsoluteValue_nonarchimedean p E))) =
      exponentialRamificationIndex
        (padicFieldExponentialValuation p)
        (padicFiniteExtensionExponentialValuation p E)

theorem

natCard_padicCanonicalInertia_le_totient_primePow_of_coprimeEmbedding

L130 ↗

HilbertRamification.natCard_padicCanonicalInertia_le_totient_primePow_of_coprimeEmbedding