NYLL
Module

MixedCharPadicIntMap.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMap
6 declarations indexed from sourceView source ↗

Module documentation

The map from p-adic integers to a complete valuation ring

Reduction modulo p^n maps to reduction modulo the nth maximal-ideal power. Adic completeness lifts these compatible maps to the actual valuation ring. Neither characteristic zero nor finiteness of the residue field is required.

Imports3
Imported by3

Declarations

def

zmodToMaximalIdealQuotient

L25 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.zmodToMaximalIdealQuotient
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
def zmodToMaximalIdealQuotient
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (p : ℕ) [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (n : ℕ) :
    ZMod (p ^ n) →+* v.valuationSubring ⧸ (IsLocalRing.maximalIdeal v.valuationSubring) ^ n
def

padicIntQuotientMap

L42 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.padicIntQuotientMap
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
def padicIntQuotientMap
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (n : ℕ) :
    ℤ_[p] →+* v.valuationSubring ⧸ (IsLocalRing.maximalIdeal v.valuationSubring) ^ n
theorem

padicIntQuotientMap_compatible

L49 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.padicIntQuotientMap_compatible
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 padicIntQuotientMap_compatible
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    {m n : ℕ} (h : m ≤ n) :
    (Ideal.Quotient.factorPow (IsLocalRing.maximalIdeal v.valuationSubring) h).comp
      (padicIntQuotientMap v p n) = padicIntQuotientMap v p m
def

padicIntToValuationSubringOfMixedChar

L66 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.padicIntToValuationSubringOfMixedChar
Documentation

The p-adic integers map to the actual complete valuation ring.

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
def padicIntToValuationSubringOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
    ℤ_[p] →+* v.valuationSubring
theorem

padicIntToValuationSubringOfMixedChar_mod_pow

L77 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.padicIntToValuationSubringOfMixedChar_mod_pow
Documentation

Each coordinate of the lifted map is the canonical cast of reduction modulo p^n.

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 padicIntToValuationSubringOfMixedChar_mod_pow
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (n : ℕ) (a : ℤ_[p]) :
    Ideal.Quotient.mk ((IsLocalRing.maximalIdeal v.valuationSubring) ^ n)
        (padicIntToValuationSubringOfMixedChar v p a) =
      ZMod.cast (PadicInt.toZModPow n a)
def

padicIntToFieldOfMixedChar

L90 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.padicIntToFieldOfMixedChar
Documentation

The induced map from p-adic integers to the valued field.

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
def padicIntToFieldOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
    ℤ_[p] →+* K

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