NYLL
Module

DenominatorValuation.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.DenominatorValuation
9 declarations indexed from sourceView source ↗

Module documentation

Valuations of natural-number denominators

For a complete discrete valuation with value group WithZero (Multiplicative ℤ) and finite residue field, this file constructs the ramification index e = v_K(p) from the valuation itself. In mixed characteristic it then proves the natural-number valuation formula used in the logarithm and exponential theorems.

Imports2
Imported by4

Declarations

def

coherentWithZeroMultiplicativeIntGroup

L32 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.coherentWithZeroMultiplicativeIntGroup
Documentation

The full ordered group structure whose ordered-monoid parent is the canonical one used by Valuation on ℤᵐ⁰.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · full declaration
def coherentWithZeroMultiplicativeIntGroup :
    LinearOrderedCommGroupWithZero
      (WithZero (Multiplicative ℤ)) where
  __ :=
    (inferInstance :
      LinearOrderedCommMonoidWithZero
        (WithZero (Multiplicative ℤ)))
  __ :=
    (inferInstance :
      CommGroupWithZero
        (WithZero (Multiplicative ℤ)))
def

ofWithZeroValuation

L46 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ofWithZeroValuation
Documentation

Package a standard ℤᵐ⁰-valued complete discrete valuation with finite residue field as a local field.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · full declaration
def ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] :
    LocalField.{u, 0} K where
  toCompleteDVF :=
    { ValueGroup := WithZero (Multiplicative ℤ)
      instValueGroup := coherentWithZeroMultiplicativeIntGroup
      valuation := v
      instCompleteDiscrete := inferInstance }
  residueFinite := by
    change Finite (IsLocalRing.ResidueField v.valuationSubring)
    infer_instance
def

ramificationIndexOfWithZeroValuation

L63 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation
Documentation

The ramification index e = v_K(p) of a standard mixed-characteristic local field, obtained from the exponent of the value of its residue characteristic p.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
def ramificationIndexOfWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] : ℕ
theorem

ramificationIndexOfWithZeroValuation_intCast

L73 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation_intCast
Documentation

The natural ramification index recovers the normalized integer valuation of the residue characteristic.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ramificationIndexOfWithZeroValuation_intCast
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    (ramificationIndexOfWithZeroValuation v : ℤ) =
      -WithZero.log
        (v ((ofWithZeroValuation v).residueCharacteristic : K))
theorem

ramificationIndexOfWithZeroValuation_pos

L104 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.ramificationIndexOfWithZeroValuation_pos
Documentation

The ramification index of a mixed-characteristic local field is positive.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem ramificationIndexOfWithZeroValuation_pos
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    0 < ramificationIndexOfWithZeroValuation v
theorem

valuation_residueCharacteristic_eq_exp_neg_ramificationIndex

L134 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_residueCharacteristic_eq_exp_neg_ramificationIndex
Documentation

The value of the residue characteristic is exp (-e), where e is the ramification index constructed from the valuation.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_residueCharacteristic_eq_exp_neg_ramificationIndex
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K] :
    v ((ofWithZeroValuation v).residueCharacteristic : K) =
      WithZero.exp (-(ramificationIndexOfWithZeroValuation v : ℤ))
theorem

valuation_natCast_eq_exp_neg_ramificationIndex_mul_padicValNat

L161 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_eq_exp_neg_ramificationIndex_mul_padicValNat
Documentation

A nonzero natural number has valuation equal to the value of its residue-characteristic power. This is the denominator formula needed for the logarithm and exponential estimates in the logarithm and exponential estimates.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_eq_exp_neg_ramificationIndex_mul_padicValNat
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (m : ℕ) (hm : m ≠ 0) :
    v (m : K) =
      WithZero.exp
        (-((ramificationIndexOfWithZeroValuation v : ℤ) *
          (padicValNat (ofWithZeroValuation v).residueCharacteristic m : ℤ)))
theorem

valuation_natCast_succ_eq_exp_neg_ramificationIndex_mul_padicValNat

L219 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_succ_eq_exp_neg_ramificationIndex_mul_padicValNat
Documentation

Successor form of the natural-number valuation formula. Unlike the main formula, this needs no explicit nonzero hypothesis.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_succ_eq_exp_neg_ramificationIndex_mul_padicValNat
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (m : ℕ) :
    v ((m + 1 : ℕ) : K) =
      WithZero.exp
        (-((ramificationIndexOfWithZeroValuation v : ℤ) *
          (padicValNat
            (ofWithZeroValuation v).residueCharacteristic (m + 1) : ℤ)))
theorem

valuation_natCast_factorial_eq_exp_neg_ramificationIndex_mul_padicValNat

L234 ↗
LocalFieldTheory.DiscreteValuationField.LocalField.valuation_natCast_factorial_eq_exp_neg_ramificationIndex_mul_padicValNat
Documentation

Factorial form of the natural-number valuation formula, used by the exponential series in the deep exponential–logarithm equivalence.

Source context 5 commands

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

noncomputable section
universe u
namespace LocalFieldTheory.DiscreteValuationField
namespace LocalField
variable {K : Type u} [Field K]
Lean source · statement
theorem valuation_natCast_factorial_eq_exp_neg_ramificationIndex_mul_padicValNat
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    [Finite (IsLocalRing.ResidueField v.valuationSubring)] [CharZero K]
    (m : ℕ) :
    v ((m.factorial : ℕ) : K) =
      WithZero.exp
        (-((ramificationIndexOfWithZeroValuation v : ℤ) *
          (padicValNat
            (ofWithZeroValuation v).residueCharacteristic m.factorial : ℤ)))

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