Module

MixedCharPrincipalUnitPadicPow.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicPow

3 declarations indexed from sourceView source ↗

Module documentation

P-adic powers of actual principal units

The residue characteristic of the raw valuation supplies the characteristic of its bundled complete-DVF residue field. Scalar multiplication is then read multiplicatively as a p-adic power.

Imports2

Imported by4

def

principalUnitPadicModuleOfMixedChar

L28 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitPadicModuleOfMixedChar

Documentation

The residue-prime module expressed on the raw valuation's principal units.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
variable (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]

Lean source · statement

def principalUnitPadicModuleOfMixedChar :
    Module ℤ_[p] (Additive (CompleteDVF.higherPrincipalUnitGroup
      (completeDVFOfWithZeroValuation v) 1))

def

principalUnitPadicPowOfMixedChar

L36 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitPadicPowOfMixedChar

Documentation

A p-adic exponent acts on the actual multiplicative principal-unit group.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
variable (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]

Lean source · statement

def principalUnitPadicPowOfMixedChar (a : ℤ_[p])
    (x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1) :
    CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1

theorem

principalUnitPadicPowOfMixedChar_natCast

L42 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitPadicPowOfMixedChar_natCast

Documentation

Natural p-adic exponents agree with the original group powers.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u
variable {K : Type u} [Field K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
variable (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]

Lean source · statement

theorem principalUnitPadicPowOfMixedChar_natCast (n : ℕ)
    (x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1) :
    principalUnitPadicPowOfMixedChar v p (n : ℤ_[p]) x = x ^ n

Module documentation

P-adic powers of actual principal units

Declarations

principalUnitPadicModuleOfMixedChar

principalUnitPadicPowOfMixedChar

principalUnitPadicPowOfMixedChar_natCast