ClassFieldTheory.mem_rayLocalHigherUnitGroup_iff_exists_one_add
For n ≥ 1, a local field unit belongs to the n-th higher-unit group exactly when its value is 1 + t for some t in the n-th power of the maximal ideal of the local integer ring.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheory
universe uLean source · statement
theorem mem_rayLocalHigherUnitGroup_iff_exists_one_add
{K : Type u} [Field K] [NumberField K]
(v : HeightOneSpectrum (𝓞 K)) (n : ℕ) (hn : 1 ≤ n)
(x : (v.adicCompletion K)ˣ) :
x ∈ rayLocalHigherUnitGroup v n ↔
∃ t : v.adicCompletionIntegers K,
t ∈ (IsLocalRing.maximalIdeal (v.adicCompletionIntegers K)) ^ n ∧
(x : v.adicCompletion K) =
((1 + t : v.adicCompletionIntegers K) : v.adicCompletion K)