Module

MixedCharPadicIntMapEquivariance.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapEquivariance

2 declarations indexed from sourceView source ↗

Module documentation

Automorphism invariance of the p-adic integer map

A valuation-preserving field automorphism fixes the constructed image of the p-adic integers, by continuity and density of the natural numbers.

Imports3

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapContinuous
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ValuationPreservingContinuous
Mathlib.Topology.DenseEmbedding

Imported by2

theorem

ringEquiv_padicIntToFieldOfMixedChar

L25 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ringEquiv_padicIntToFieldOfMixedChar

Documentation

Valuation-preserving automorphisms fix every scalar in the actual p-adic image.

Source context 3 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K]

Lean source · statement

theorem ringEquiv_padicIntToFieldOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (f : K ≃+* K) (hval : ∀ x : K, v (f x) = v x) (a : ℤ_[p]) :
    f (padicIntToFieldOfMixedChar v p a) = padicIntToFieldOfMixedChar v p a

theorem

ringEquiv_padicIntToFieldOfMixedChar_mul

L41 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ringEquiv_padicIntToFieldOfMixedChar_mul