NYLL
Module

InertiaRootsOfUnity.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.InertiaRootsOfUnity
2 declarations indexed from sourceView source ↗

Module documentation

Roots of unity in the actual inertia field

In residue characteristic zero, inertia fixes every root of unity. Each root is a valuation-ring unit. Its image under inertia has the same reduction, so the injectivity of Henselian root reduction identifies the two roots. This gives membership in the actual inertia fixed field without assuming any comparison or surjectivity of residue-field maps.

Imports7
Imported by2

Declarations

theorem

inertia_fixes_of_isOfFinOrder

L38 ↗
RamificationTheory.HilbertRamification.ValuationSubring.inertia_fixes_of_isOfFinOrder
Documentation

Every actual inertia automorphism fixes every finite-order field element when the upper Henselian DVF has residue characteristic zero.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  (F : HenselianDVF.{v, w} L) [CharZero F.residueField]

-- The actions on the valuation ring and residue field are the canonical
-- decomposition-subgroup actions. No new algebra, action, or topology is installed.
Lean source · statement
theorem inertia_fixes_of_isOfFinOrder
    (σ : inertiaGroup K F.valuation.valuationSubring)
    (ζ : L) (hζ : IsOfFinOrder ζ) :
    ((σ : decompositionGroup K F.valuation.valuationSubring) : L ≃ₐ[K] L) ζ = ζ
theorem

mem_inertiaField_of_isOfFinOrder

L77 ↗
RamificationTheory.HilbertRamification.ValuationSubring.mem_inertiaField_of_isOfFinOrder
Documentation

All roots of unity lie in the actual inertia fixed field in residue characteristic zero. No finiteness or residue-field comparison is required.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
open ValuationTheory.DiscreteValuationField
universe u v w
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
  (F : HenselianDVF.{v, w} L) [CharZero F.residueField]

-- The actions on the valuation ring and residue field are the canonical
-- decomposition-subgroup actions. No new algebra, action, or topology is installed.
Lean source · statement
theorem mem_inertiaField_of_isOfFinOrder (ζ : L) (hζ : IsOfFinOrder ζ) :
    ζ ∈ inertiaField K F.valuation.valuationSubring

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.