Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ValuationKrasner

Module documentation

A valuation-theoretic finite Galois form of Krasner's argument

For a finite Galois extension with a uniquely extended discrete valuation, suppose b is closer to an integral element a than any nontrivial automorphic displacement of a. Then every automorphism fixing b also fixes a.

This is the stabilizer step in Krasner's lemma. Stating it directly for the finite Galois overfield avoids introducing a second normed-field topology: invariance of the normalized additive valuation and its ultrametric inequality are sufficient.

theorem

valuationSubringAutOfUniqueExtension_eq_of_fixed_of_close

L45 ↗

RamificationTheory.HilbertRamification.Higher.valuationSubringAutOfUniqueExtension_eq_of_fixed_of_close

Documentation

If σ fixes b, and a-b is strictly deeper than the displacement σ(a)-a whenever that displacement is nonzero, then σ fixes a.

The proof is the elementary Krasner contradiction

v(σ(a)-a) ≥ min(v(σ(a)-b), v(b-a)) = v(a-b).

Source context 8 commands

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

noncomputable section
universe u v w x
namespace RamificationTheory.HilbertRamification
namespace Higher
open ValuationTheory.DiscreteValuationField
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]
variable {base : DVF.{u, v} K} {target : DVF.{w, x} L}
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem valuationSubringAutOfUniqueExtension_eq_of_fixed_of_close
    (huniq :
      RamificationTheory.DiscreteValuationField.DVF.HasUniqueValuationExtension
        base target)
    (σ : Gal(L/K)) (a b : target.valuationSubring)
    (hfix :
      valuationSubringAutOfUniqueExtension
        (base := base) (target := target) huniq σ b = b)
    (hclose :
      valuationSubringAutOfUniqueExtension
            (base := base) (target := target) huniq σ a ≠ a →
        IsDiscreteValuationRing.addVal target.valuationSubring
            (valuationSubringAutOfUniqueExtension
              (base := base) (target := target) huniq σ a - a) <
          IsDiscreteValuationRing.addVal target.valuationSubring
            (a - b)) :
    valuationSubringAutOfUniqueExtension
      (base := base) (target := target) huniq σ a = a

Module documentation

A valuation-theoretic finite Galois form of Krasner's argument

Declarations

valuationSubringAutOfUniqueExtension_eq_of_fixed_of_close