For a nonzero integer, the additive DVR valuation in ℤ_(p) is its integer p-adic valuation. The comparison uses the inverse images of powers of the localized maximal ideal: membership in its nth power is exactly divisibility by p^n in ℤ. Thus it does not require a choice of a unit factor of the integer.
This is the arithmetic comparison needed for the local intersection number in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.
The principal ideal of the integers generated by a natural number.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ShimizuYamaguchi26BranchedCoveringsabbrev IntegerPrimeIdeal (p : ℕ) : Ideal ℤThe localization of the integers at the ideal generated by the prime p.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ShimizuYamaguchi26BranchedCoveringsabbrev IntegerPrimeLocalization (p : ℕ) [Fact p.Prime] : TypeSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ShimizuYamaguchi26BranchedCoveringsinstance (p : ℕ) [hp : Fact p.Prime] :
IsDiscreteValuationRing (IntegerPrimeLocalization p)The normalized additive valuation of a nonzero integer in ℤ_(p) is padicValInt.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ShimizuYamaguchi26BranchedCoveringstheorem integerLocalization_addVal_eq_padicValInt
(p : ℕ) [hp : Fact p.Prime] (z : ℤ) (hz : z ≠ 0) :
IsDiscreteValuationRing.addVal (IntegerPrimeLocalization p)
(algebraMap ℤ (IntegerPrimeLocalization p) z) =
(padicValInt p z : ℕ∞)