Module

UnramifiedBaseUnitNorm.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.UnramifiedBaseUnitNorm

1 declaration indexed from sourceView source ↗

Module documentation

Base-field units are norms in a divisible unramified local tower

For finite local extensions K → L → M with M/L unramified, a base-field unit has L-valuation divisible by e(L/K). If [M:L] divides that actual ramification index, the unramified norm subgroup calculation produces a unit of M whose field norm is the given base-field unit embedded in L.

Imports9

Imported by2

theorem

exists_normUnits_eq_mapBaseUnitsToExtensionUnits_of_finrank_dvd_ramificationIdx

L34 ↗

LocalClassFieldTheory.exists_normUnits_eq_mapBaseUnitsToExtensionUnits_of_finrank_dvd_ramificationIdx

Documentation

A base-field unit has an actual norm preimage when the unramified top extension degree divides the ramification index of the lower extension.

Source context 4 commands

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

namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem exists_normUnits_eq_mapBaseUnitsToExtensionUnits_of_finrank_dvd_ramificationIdx
    (K L M : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Field M] [ValuativeRel M] [TopologicalSpace M]
    [IsNonarchimedeanLocalField M]
    [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L]
    [Algebra L M] [FiniteDimensional L M] [IsGalois L M]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [Valuation.HasExtension (ValuativeRel.valuation L)
      (ValuativeRel.valuation M)]
    [Module.Finite 𝒪[L] 𝒪[M]] [IsUnramifiedValuedExtension L M]
    (hd : Module.finrank L M ∣
      (𝓂[L] : Ideal 𝒪[L]).ramificationIdx 𝒪[K]) (x : Kˣ) :
    ∃ y : Mˣ, normUnits L M y = mapBaseUnitsToExtensionUnits K L x

Module documentation

Base-field units are norms in a divisible unramified local tower

Declarations

exists_normUnits_eq_mapBaseUnitsToExtensionUnits_of_finrank_dvd_ramificationIdx