The intrinsic local normalization agrees with the distinguished integer-valued adic valuation: the only order-preserving automorphism of the integer value group is the identity. Consequently localization of global power classes preserves their finite-valuation defects.
The two completion structures are local instances shared by the three public lemmas. Only compatibility of the distinguished valuation is introduced inside a proof; no new global instance or additional arithmetic hypothesis is needed.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevichtheorem orderMonoidIso_withZeroInt_apply
(e : ℤᵐ⁰ ≃*o ℤᵐ⁰) (x : ℤᵐ⁰) : e x = xSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevichtheorem localIntegerValuation_eq_of_surjective
(L : Type*) [Field L] [ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
(ν : Valuation L ℤᵐ⁰) [ν.Compatible] [ν.IsRankOneDiscrete]
(hν : Function.Surjective ν) : LocalFieldTheory.localIntegerValuation L = νSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
variable (v : HeightOneSpectrum (𝓞 K))instance : ValuativeRel (v.adicCompletion K)Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
variable (v : HeightOneSpectrum (𝓞 K))
local instance : ValuativeRel (v.adicCompletion K) :=
finitePlaceAdicCompletionValuativeRel K vinstance : IsNonarchimedeanLocalField (v.adicCompletion K)Intrinsic local normalization is the distinguished adic valuation.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
variable (v : HeightOneSpectrum (𝓞 K))
local instance : ValuativeRel (v.adicCompletion K) :=
finitePlaceAdicCompletionValuativeRel K v
local instance : IsNonarchimedeanLocalField (v.adicCompletion K) :=
finitePlaceAdicCompletionIsNonarchimedeanLocalField K vtheorem finitePlaceLocalIntegerValuation_eq :
LocalFieldTheory.localIntegerValuation (v.adicCompletion K) =
(Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰)The normalized valuation of a diagonal unit equals its global finite-place valuation.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
variable (v : HeightOneSpectrum (𝓞 K))
local instance : ValuativeRel (v.adicCompletion K) :=
finitePlaceAdicCompletionValuativeRel K v
local instance : IsNonarchimedeanLocalField (v.adicCompletion K) :=
finitePlaceAdicCompletionIsNonarchimedeanLocalField K vtheorem finitePlaceValuationMap_diagonal (a : Kˣ) :
LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap (v.adicCompletion K)
(Additive.ofMul (Units.map (algebraMap K (v.adicCompletion K)).toMonoidHom a)) =
(v.valuationOfNeZero a).toAddLocalization preserves the mod-p finite-valuation defect of every global power class.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel WithZero
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open IsDedekindDomain KummerTheory
variable (K : Type*) [Field K] [NumberField K]
variable (p : ℕ) [Fact p.Prime]
variable (v : HeightOneSpectrum (𝓞 K))
local instance : ValuativeRel (v.adicCompletion K) :=
finitePlaceAdicCompletionValuativeRel K v
local instance : IsNonarchimedeanLocalField (v.adicCompletion K) :=
finitePlaceAdicCompletionIsNonarchimedeanLocalField K vtheorem finitePlaceLocalPowerClassValuation_localization
(x : absolutePowerClassModP K p) :
finitePlaceLocalPowerClassValuation K p v
(finitePlacePowerClassLocalization K p v x) =
(v.valuationOfNeZeroMod p (Additive.toMul x)).toAdd