Module

HenselianAutomorphismValuation.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianAutomorphismValuation

1 declaration indexed from sourceView source ↗

Module documentation

Galois invariance of extensions of Henselian discrete valuations

Every base-field automorphism of a finite extension preserves the actual extension valuation. Henselianity supplies uniqueness of the valuation ring; the finite order of the automorphism then forces equality of values.

Imports3

Imported by4

theorem

valuation_algEquiv_eq

L26 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuation_algEquiv_eq

Documentation

Automorphisms of a finite extension preserve its chosen extension valuation.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
universe u v w z
variable {K : Type u} {L : Type w} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem valuation_algEquiv_eq [FiniteDimensional K L]
    (base : HenselianDVF.{u, v} K) (target : DVF.{w, z} L)
    [base.toDVF.valuation.HasExtension target.valuation]
    (f : L ≃ₐ[K] L) (x : L) : target.valuation (f x) = target.valuation x

Module documentation

Galois invariance of extensions of Henselian discrete valuations

Declarations

valuation_algEquiv_eq