Module

LocalFiniteInertiaUnramified.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Local.LocalFiniteInertiaUnramified

1 declaration indexed from sourceView source ↗

Module documentation

Inertia-trivial finite embeddings give actual unramified local extensions

The image of the supplied finite field embedding is constructed inside the local separable closure. Inertia fixes that actual intermediate field; the spectral criterion applies there, and the resulting unramifiedness is moved back to the original valued extension using its integral closure.

Instance audit: the original K → L tower is inherited. The image has its single intermediate-field K-algebra and one canonical spectral norm/valuation pair; all remaining local instances are finiteness, Galois, or valuation- compatibility proofs. No second algebra path or valuation on one target is introduced, and the spectral setup occurs only once.

Imports2

Imported by2

theorem

localFiniteExtension_isUnramified_of_inertiaFixes

L40 ↗

ClassFieldTower.Martinet.Shafarevich.localFiniteExtension_isUnramified_of_inertiaFixes

Documentation

Pointwise inertia-triviality on a finite embedding forces actual valuation-ring ramification index one.

Source context 6 commands

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

open scoped ValuativeRel
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open LocalFieldTheory LocalClassFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K L : Type)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L]
  [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
  [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
  [Module.Finite 𝒪[K] 𝒪[L]] [IsIntegralClosure 𝒪[L] 𝒪[K] L]

Lean source · statement

theorem localFiniteExtension_isUnramified_of_inertiaFixes
    (f : L →ₐ[K] SeparableClosure K)
    (hf : ∀ sigma ∈ (localResidueDegree K).toMonoidHom.ker,
      ∀ x : L, sigma (f x) = f x) : IsUnramifiedValuedExtension K L

Module documentation

Inertia-trivial finite embeddings give actual unramified local extensions

Declarations

localFiniteExtension_isUnramified_of_inertiaFixes