Documentation

TauCeti.NumberTheory.LocalField.NatCastValuation

The normalized valuation of a natural number in a local field #

Let K be a nonarchimedean local field. The image of a natural number n under the canonical map β„• β†’ K lies in the ring of integers π’ͺ[K], so its normalized valuation is a natural number as soon as it is defined, that is as soon as (n : K) β‰  0. This file introduces that natural number,

natCastValuation K n hn : β„•,

and its basic API.

It is the quantity that measures how far n is from being invertible in π’ͺ[K]: it vanishes exactly when (n : π’ͺ[K]) is a unit, equivalently when the residue characteristic of K does not divide n. In particular it vanishes identically when K has positive characteristic, so it carries information only in mixed characteristic; there its value at the residue characteristic is the absolute ramification index of K.

Main definitions #

Main results #

References #

source
theorem TauCeti.natCast_ne_zero_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] {n : β„•} (hn : IsUnit ↑n) :
↑n β‰  0

A natural number that is a unit in the integer ring is nonzero in the field.

source
theorem TauCeti.natCast_ne_zero_of_coprime_ringChar {K : Type u_1} [Field K] [ValuativeRel K] {n : β„•} (hn : n.Coprime (ringChar (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer))) :
↑n β‰  0

A natural number prime to the residue characteristic is nonzero in the field.

source
theorem TauCeti.two_ne_zero_of_isUnit_two {K : Type u_1} [Field K] [ValuativeRel K] (h2 : IsUnit 2) :
2 β‰  0

If 2 is a unit in the integer ring, it is nonzero in the field.

source
noncomputable def TauCeti.natCastValuation (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
β„•

The normalized valuation v_K((n : K)) of the image of a natural number n in a nonarchimedean local field K, as a natural number. The proof hn that the image is nonzero is part of the input: in positive characteristic the image can vanish, and no junk value is assigned there.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.normalizedValuation_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    (normalizedValuation K) (Units.mk0 (↑n) hn) = Multiplicative.ofAdd ↑(natCastValuation K n hn)

    The characteristic equation of natCastValuation: it decodes the normalized valuation of (n : K). The right-hand side expresses the valuation as the image of a natural number, so the equation also records that the image of n lies in π’ͺ[K].

    source
    theorem TauCeti.toAdd_normalizedValuation_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    Multiplicative.toAdd ((normalizedValuation K) (Units.mk0 (↑n) hn)) = ↑(natCastValuation K n hn)

    The additive normalized valuation of a nonzero natural-number cast is its natCastValuation.

    source
    @[simp]
    theorem TauCeti.normalizedValuationWithZero_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    (normalizedValuationWithZero K) ↑n = WithZero.exp ↑(natCastValuation K n hn)

    The zero-preserving form of the characteristic equation of natCastValuation.

    source
    @[simp]
    theorem TauCeti.natCastValuation_eq_zero_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    natCastValuation K n hn = 0 ↔ IsUnit ↑n

    The vanishing criterion: the normalized valuation of n is zero exactly when n is invertible in the ring of integers.

    source
    theorem TauCeti.natCastValuation_eq_zero_of_isUnit (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} (hn : ↑n β‰  0) (hn' : IsUnit ↑n) :
    natCastValuation K n hn = 0

    If n is invertible in the ring of integers then its normalized valuation vanishes.

    source
    theorem TauCeti.natCastValuation_eq_zero_iff_not_dvd (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    natCastValuation K n hn = 0 ↔ Β¬ringChar (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer) ∣ n

    The vanishing criterion read off the residue field: the normalized valuation of n is zero exactly when the residue characteristic of K does not divide n.

    source
    theorem TauCeti.natCastValuation_ne_zero_iff_ringChar_eq (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {p : β„•} (hp : Nat.Prime p) (hn : ↑p β‰  0) :
    natCastValuation K p hn β‰  0 ↔ ringChar (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer) = p

    For a prime p, the normalized valuation of p is nonzero exactly when p is the residue characteristic of K, that is, exactly when K is p-adic.

    source
    theorem TauCeti.natCastValuation_eq_zero_of_ringChar_ne_zero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (hK : ringChar K β‰  0) (n : β„•) (hn : ↑n β‰  0) :
    natCastValuation K n hn = 0

    In equal characteristic the normalized valuation of a nonzero natural-number cast always vanishes: a natural number whose image in K is nonzero is prime to the characteristic, hence invertible in π’ͺ[K]. The invariant therefore carries information only in mixed characteristic, which is why the absolute ramification index is defined only there.

    source
    @[simp]
    theorem TauCeti.natCastValuation_one (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
    natCastValuation K 1 β‹― = 0

    The normalized valuation of 1 vanishes.

    source
    @[simp]
    theorem TauCeti.natCastValuation_mul (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {m n : β„•} (hm : ↑m β‰  0) (hn : ↑n β‰  0) :
    natCastValuation K (m * n) β‹― = natCastValuation K m hm + natCastValuation K n hn

    The normalized valuation of a natural number is additive in it.

    source
    theorem TauCeti.natCastValuation_le_of_dvd (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {m n : β„•} (hm : ↑m β‰  0) (hn : ↑n β‰  0) (h : m ∣ n) :
    natCastValuation K m hm ≀ natCastValuation K n hn

    The normalized valuation of a natural number is monotone for divisibility.

    source
    theorem TauCeti.natCastValuation_lt_sub_one_mul_of_lt_of_dvd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n i : β„•} (hn : ↑n β‰  0) (hi : natCastValuation K n hn < i) {p : β„•} (hp : Nat.Prime p) (hpK : ↑p β‰  0) (hpn : p ∣ n) :
    natCastValuation K p hpK < (p - 1) * i

    The depth condition beyond v_K(n). If v_K(n) < i, then every prime p ∣ n satisfies v_K(p) < (p - 1) * i, the depth condition of the deep-unit power lemmas map_powMonoidHom_unitFiltration and disjoint_rootsOfUnity_unitFiltration of TauCeti.NumberTheory.LocalField.UnitFiltration.Pow.

    source
    @[simp]
    theorem TauCeti.natCastValuation_pow (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} (k : β„•) (hn : ↑n β‰  0) :
    natCastValuation K (n ^ k) β‹― = k * natCastValuation K n hn

    The normalized valuation of a power of a natural number.

    source
    theorem TauCeti.span_natCast_eq_maximalIdeal_pow (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    Ideal.span {↑n} = IsLocalRing.maximalIdeal β†₯(ValuativeRel.valuation K).integer ^ natCastValuation K n hn

    The ideal generated by a nonzero natural-number cast is the corresponding power of the maximal ideal, with exponent its normalized valuation.

    source
    @[simp]
    theorem TauCeti.IsDiscreteValuationRing.addVal_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    (IsDiscreteValuationRing.addVal β†₯(ValuativeRel.valuation K).integer) ↑n = ↑(natCastValuation K n hn)

    The additive valuation of a nonzero natural-number cast in the integer ring agrees with natCastValuation of its image in the field.

    source
    theorem TauCeti.valuation_natCast_eq_pow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ο€ : β†₯(ValuativeRel.valuation K).integer} (hΟ€ : Irreducible Ο€) (n : β„•) (hn : ↑n β‰  0) :
    (ValuativeRel.valuation K) ↑n = (ValuativeRel.valuation K) ↑π ^ natCastValuation K n hn

    The multiplicative valuation of a nonzero natural-number cast is the corresponding power of the valuation of any uniformizer.

    source
    @[simp]
    theorem TauCeti.normalizedAbsoluteValue_natCast (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) (hn : ↑n β‰  0) :
    (normalizedAbsoluteValue K) ↑n = (↑(Nat.card (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer)))⁻¹ ^ natCastValuation K n hn

    The normalized absolute value of a natural number is q ^ (-natCastValuation K n hn), where q is the cardinality of the residue field.