Module

ValuationPreservingContinuous.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationPreservingContinuous

1 declaration indexed from sourceView source ↗

Module documentation

Continuity of valuation-preserving field automorphisms

A valuation-preserving automorphism preserves every basic neighbourhood of zero for the actual topology induced by the valuation. No completeness or discreteness hypothesis is required.

Imports3

Mathlib.Data.Int.WithZero
Mathlib.Topology.Algebra.Valued.ValuationTopology
Mathlib.Topology.Algebra.Group.Basic

Imported by4

theorem

continuous_ringEquiv_of_preserves

L27 ↗

ValuationTheory.DiscreteValuationField.Valuation.continuous_ringEquiv_of_preserves

Documentation

A valuation-preserving field automorphism is continuous for the topology induced by that valuation.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.Valuation
open scoped Topology
variable {K : Type*} [Field K]

Lean source · statement

theorem continuous_ringEquiv_of_preserves
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (f : K ≃+* K) (hval : ∀ x : K, v (f x) = v x) :
    @Continuous K K (Valued.mk' v).toUniformSpace.toTopologicalSpace
      (Valued.mk' v).toUniformSpace.toTopologicalSpace f

Module documentation

Continuity of valuation-preserving field automorphisms

Declarations

continuous_ringEquiv_of_preserves