For an integer-valued valuation in mixed characteristic, the positive exponent of the residue prime gives the denominator estimates for logarithm and exponential series. Neither completeness nor residue-field finiteness is needed.
The nonnegative exponent of the value of a specified residue prime.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]def residueRamificationIndex (v : Valuation K (WithZero (Multiplicative ℤ)))
(p : ℕ) : ℕA residue characteristic has value strictly less than one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem natCast_residueChar_lt_one
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ)
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
v (p : K) < 1In mixed characteristic the logarithmic value of the residue prime is negative.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem log_natCast_residueChar_neg [CharZero K]
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
WithZero.log (v (p : K)) < 0Passing to a natural exponent does not truncate the ramification index.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem residueRamificationIndex_intCast [CharZero K]
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
(v.residueRamificationIndex p : ℤ) = -WithZero.log (v (p : K))The ramification index of a residue prime in mixed characteristic is positive.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem residueRamificationIndex_pos [CharZero K]
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
0 < v.residueRamificationIndex pThe actual value of the residue prime is recovered by the constructed exponent.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem natCast_residueChar_eq_exp_neg [CharZero K]
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] :
v (p : K) = WithZero.exp (-(v.residueRamificationIndex p : ℤ))The denominator valuation formula, with its scale constructed from the valuation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Valuation
universe u
variable {K : Type u} [Field K]theorem natCast_eq_exp_neg_ramificationIndex_mul_padicValNat [CharZero K]
(v : Valuation K (WithZero (Multiplicative ℤ))) (p : ℕ) [Fact p.Prime]
[CharP (IsLocalRing.ResidueField v.valuationSubring) p] (n : ℕ) (hn : n ≠ 0) :
v (n : K) =
WithZero.exp (-((v.residueRamificationIndex p : ℤ) * (padicValNat p n : ℤ)))