NYLL
Module

MixedCharPadicIntMapContinuous.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapContinuous
1 declaration indexed from sourceView source ↗

Module documentation

Continuity of the p-adic integer map into a complete valued field

The lifted map carries the open kernel of reduction modulo p^n into the nth maximal-ideal power. The adic topology on the valuation ring is its actual subtype topology, so the map to the field is continuous.

Imports4
Imported by4

Declarations

theorem

continuous_padicIntToFieldOfMixedChar

L29 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.continuous_padicIntToFieldOfMixedChar
Documentation

The actual map from p-adic integers is continuous in the valuation topology.

Source context 4 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open scoped Topology
universe u
variable {K : Type u} [Field K]
Lean source · statement
theorem continuous_padicIntToFieldOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
    @Continuous ℤ_[p] K (inferInstance : TopologicalSpace ℤ_[p])
      (Valued.mk' v).toUniformSpace.toTopologicalSpace (padicIntToFieldOfMixedChar v p)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.