Module

NormedGaloisIsometry.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.NormedGaloisIsometry

2 declarations indexed from sourceView source ↗

Module documentation

Galois isometries over a Henselian normed field

The norm of a finite extension is preserved by every base-field automorphism when the nonarchimedean base valuation ring is Henselian. Completeness of the base field is not required.

Imports4

Nyll.ValuedFieldTheory.Valuation.Henselian.AlgebraicExtensionUniqueness
Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueExtensionPrimitive
Mathlib.Topology.Algebra.Valued.NormedValued
Mathlib.Analysis.Normed.Module.Basic

Imported by2

theorem

normed_valuationSubring_hasExtension

L25 ↗

ValuationTheory.Henselian.normed_valuationSubring_hasExtension

Source context 2 commands

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

namespace ValuationTheory.Henselian
variable {K L : Type*} [NormedField K] [NormedField L]
  [IsUltrametricDist K] [IsUltrametricDist L] [NormedAlgebra K L]

Lean source · full declaration

theorem normed_valuationSubring_hasExtension :
    (NormedField.valuation (K := K)).valuationSubring.valuation.HasExtension
      (NormedField.valuation (K := L)).valuationSubring.valuation where
  val_isEquiv_comap := by
    rw [Valuation.isEquiv_iff_val_le_one]
    intro x
    change (NormedField.valuation (K := K)).valuationSubring.valuation x ≤ 1 ↔
      (NormedField.valuation (K := L)).valuationSubring.valuation
        (algebraMap K L x) ≤ 1
    rw [ValuationSubring.valuation_le_one_iff, ValuationSubring.valuation_le_one_iff]
    change ‖x‖₊ ≤ 1 ↔ ‖algebraMap K L x‖₊ ≤ 1
    rw [nnnorm_algebraMap']

theorem

norm_algEquiv_eq_of_henselianRing

L40 ↗

ValuationTheory.Henselian.norm_algEquiv_eq_of_henselianRing

Documentation

Every automorphism of a finite normed extension of a Henselian nonarchimedean field preserves the norm.