NYLL
Module

MixedCharPrincipalUnitPadicPowMod.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicPowMod
2 declarations indexed from sourceView source ↗

Module documentation

P-adic exponents modulo prime powers

Reduction of a p-adic exponent modulo p^s changes its action on a principal unit by an actual p^s-th power. The witness is constructed in the principal unit group and then mapped into the field unit group.

Imports3
Imported by2

Declarations

theorem

exists_principalUnitPadicPow_div_natCast_eq_pow

L30 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_principalUnitPadicPow_div_natCast_eq_pow
Documentation

A p-adic exponent and its natural residue modulo p^s differ on a principal unit by an actual p^s-th power in the 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
theorem exists_principalUnitPadicPow_div_natCast_eq_pow (a : ℤ_[p])
    (x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)
    (s : ℕ) :
    ∃ y : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1,
      principalUnitPadicPowOfMixedChar v p a x /
          x ^ (PadicInt.toZModPow s a).val = y ^ (p ^ s)
theorem

exists_fieldUnit_principalUnitPadicPow_div_natCast_eq_pow

L63 ↗
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_fieldUnit_principalUnitPadicPow_div_natCast_eq_pow
Documentation

The same exponent reduction has an actual p^s-th power witness in the field unit group, obtained by mapping the principal-unit witness.

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 exists_fieldUnit_principalUnitPadicPow_div_natCast_eq_pow (a : ℤ_[p])
    (x : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)
    (s : ℕ) :
    ∃ y : Kˣ,
      CompleteDVF.valuationSubringUnitsToFieldUnits (completeDVFOfWithZeroValuation v)
          (principalUnitPadicPowOfMixedChar v p a x :
            (completeDVFOfWithZeroValuation v).valuationSubringˣ) /
        (CompleteDVF.valuationSubringUnitsToFieldUnits (completeDVFOfWithZeroValuation v)
          (x : (completeDVFOfWithZeroValuation v).valuationSubringˣ)) ^
            (PadicInt.toZModPow s a).val = y ^ (p ^ s)

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