Module

FiniteAbelian.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.Filtered.FiniteAbelian

6 declarations indexed from sourceView source ↗

Module documentation

Filtered reciprocity for arbitrary finite abelian local extensions

An arbitrary finite abelian extension embeds into a standard finite abelian compositum. Passing to its field range inside the fixed separable closure permits descent by restriction, and the resulting algebra equivalence transports both filtrations back to the original extension.

Imports10

Imported by3

theorem

finiteAbelian_filteredLocalReciprocity

L41 ↗

LocalClassFieldTheory.finiteAbelian_filteredLocalReciprocity

Documentation

Characteristic-independent real filtered local reciprocity for every finite abelian extension of a nonarchimedean local field.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem finiteAbelian_filteredLocalReciprocity
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (t : ℝ) (ht : 0 ≤ t) :
    artinPrincipalUnitStepGroup K L t =
      localUpperRamificationGroup K L t

theorem

finiteAbelian_localUpperRamificationGroup_one_eq_localLowerRamificationGroup_one

L124 ↗

LocalClassFieldTheory.finiteAbelian_localUpperRamificationGroup_one_eq_localLowerRamificationGroup_one

Documentation

In a finite abelian local extension the first upper and lower groups coincide. The normalization matters: φ(1) need not equal 1, but it lies in (0, 1], where filtered reciprocity makes the upper group constant.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem finiteAbelian_localUpperRamificationGroup_one_eq_localLowerRamificationGroup_one
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    localUpperRamificationGroup K L 1 =
      localLowerRamificationGroup K L 1

theorem

finiteAbelian_localUpperRamificationGroup_one_eq_hilbertRamificationGroup

L184 ↗

LocalClassFieldTheory.finiteAbelian_localUpperRamificationGroup_one_eq_hilbertRamificationGroup

Documentation

The first upper group of a finite abelian local extension is Hilbert's ramification group for the chosen valuation ring, transported to Gal(L/K).

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem finiteAbelian_localUpperRamificationGroup_one_eq_hilbertRamificationGroup
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    localUpperRamificationGroup K L 1 =
      Subgroup.comap
        (RamificationTheory.HilbertRamification.CompleteDVF.galEquivDecompositionGroup
          (base := localCompleteDVF K)
          (target := chosenLocalExtensionCompleteDVF K L)).toMonoidHom
        (RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroupInDecomposition K
          (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring)

theorem

localConductorExponent_le_one_iff_localUpperRamificationGroup_one_eq_bot

L202 ↗

LocalClassFieldTheory.localConductorExponent_le_one_iff_localUpperRamificationGroup_one_eq_bot

Documentation

For a finite abelian local extension, the conductor exponent is at most one exactly when its first upper ramification group is trivial. This is the filtered-reciprocity bridge used by the tame-ramification criterion.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_le_one_iff_localUpperRamificationGroup_one_eq_bot
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    localConductorExponent K L ≤ 1 ↔
      localUpperRamificationGroup K L 1 = ⊥

theorem

localConductorExponent_le_one_iff_hilbertRamificationGroup_eq_bot

L221 ↗

LocalClassFieldTheory.localConductorExponent_le_one_iff_hilbertRamificationGroup_eq_bot

Documentation

Conductor exponent at most one is equivalent to the absence of wild ramification in the chosen valuation ring.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_le_one_iff_hilbertRamificationGroup_eq_bot
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L] :
    localConductorExponent K L ≤ 1 ↔
      RamificationTheory.HilbertRamification.ValuationSubring.ramificationGroup K
        (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring = ⊥

theorem

localConductorExponent_le_one_iff_residueChar_not_dvd_ramificationIndex

L235 ↗

LocalClassFieldTheory.localConductorExponent_le_one_iff_residueChar_not_dvd_ramificationIndex

Documentation

The first conductor threshold is the usual tame criterion: the residue characteristic does not divide the ramification index.

Source context 7 commands

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

noncomputable section
open scoped ValuativeRel
namespace LocalClassFieldTheory
open RamificationTheory.LocalField
open LubinTate
open LocalClassFieldTheory
open LocalFieldTheory

Lean source · statement

theorem localConductorExponent_le_one_iff_residueChar_not_dvd_ramificationIndex
    (K L : Type) [Field K] [Field L] [Algebra K L]
    [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [FiniteDimensional K L] [IsAbelianGalois K L]
    (p : ℕ) [Fact p.Prime]
    [CharP (IsLocalRing.ResidueField
      (chosenLocalExtensionCompleteDVF K L).valuation.valuationSubring) p] :
    localConductorExponent K L ≤ 1 ↔
      ¬ p ∣ ValuationTheory.DiscreteValuationField.ValuedExtension.ramificationIndex
        (localCompleteDVF K).toDVF
        (chosenLocalExtensionCompleteDVF K L).toDVF

Module documentation

Filtered reciprocity for arbitrary finite abelian local extensions

Declarations

finiteAbelian_filteredLocalReciprocity

finiteAbelian_localUpperRamificationGroup_one_eq_localLowerRamificationGroup_one

finiteAbelian_localUpperRamificationGroup_one_eq_hilbertRamificationGroup

localConductorExponent_le_one_iff_localUpperRamificationGroup_one_eq_bot

localConductorExponent_le_one_iff_hilbertRamificationGroup_eq_bot

localConductorExponent_le_one_iff_residueChar_not_dvd_ramificationIndex