Module

MixedCharPrincipalUnitLog.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLog

3 declarations indexed from sourceView source ↗

Module documentation

The principal-unit logarithm in mixed characteristic

The logarithm is constructed on every complete mixed-characteristic discrete valuation field, including fields with infinite residue field. Its scale and the completeness of the actual valuation topology are supplied by the valuation, rather than requested as comparison hypotheses.

Imports3

Imported by8

def

principalUnitLogOfMixedChar

L27 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogOfMixedChar

Documentation

The actual logarithm series as a homomorphism on all first principal units.

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] [CharZero K]

Lean source · statement

def principalUnitLogOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
    CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1 →*
      Multiplicative K

theorem

principalUnitLogOfMixedChar_apply_toAdd

L41 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogOfMixedChar_apply_toAdd

Documentation

Evaluation agrees with the existing logarithm series.

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] [CharZero K]

Lean source · full declaration

theorem principalUnitLogOfMixedChar_apply_toAdd
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
    (u : CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1) :
    (principalUnitLogOfMixedChar v p u).toAdd =
      principalUnitLogSeriesOfWithZeroValuation v u
        (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n)) := rfl

theorem

continuous_principalUnitLogOfMixedChar

L51 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.continuous_principalUnitLogOfMixedChar

Documentation

The logarithm is continuous for the actual valuation topology.

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] [CharZero K]

Lean source · full declaration

theorem continuous_principalUnitLogOfMixedChar
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
    (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Continuous (principalUnitLogOfMixedChar v p) :=
  continuous_principalUnitLogSeriesHomOfWithZeroValuationScaled (p := p) v
    (v.residueRamificationIndex p)
    (fun n => Nat.cast_ne_zero.mpr (Nat.succ_ne_zero n))
    (fun n => v.natCast_eq_exp_neg_ramificationIndex_mul_padicValNat p
      (n + 1) (Nat.succ_ne_zero n))
    (ValuationTheory.DiscreteValuationField.Valuation.completeSpace_ofWithZeroValuation v)

Module documentation

The principal-unit logarithm in mixed characteristic

Declarations

principalUnitLogOfMixedChar

principalUnitLogOfMixedChar_apply_toAdd

continuous_principalUnitLogOfMixedChar