Power residues and powers in an adic completion #
For a height-one prime v of a Dedekind domain R with fraction field K, an element
a ∈ R outside v is an n-th power in K_v exactly when its residue is an n-th power,
provided n is outside v. No finiteness assumption on the residue field is needed.
This compares the power residue conditions in Kummer theory with local power conditions.
The residue-field identification is residueFieldEquivAdicCompletionIntegers, and lifting
uses TauCeti.HenselianLocalRing.exists_pow_eq_of_residue_pow_eq.
References #
- J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 6.3.
- J. Neukirch, Algebraic Number Theory, Chapter II, §4 (Hensel's lemma).
theorem
IsDedekindDomain.HeightOneSpectrum.exists_pow_eq_adicCompletion_iff
{R : Type u_1}
{K : Type u_2}
[CommRing R]
[IsDedekindDomain R]
[Field K]
[Algebra R K]
[IsFractionRing R K]
(v : HeightOneSpectrum R)
{n : ℕ}
{a : R}
(hn : ↑n ∉ v.asIdeal)
(ha : a ∉ v.asIdeal)
:
(∃ (x : adicCompletion K v), x ^ n = (algebraMap R (adicCompletion K v)) a) ↔ ∃ (b : R ⧸ v.asIdeal), b ^ n = (Ideal.Quotient.mk v.asIdeal) a
An element outside v is an n-th power in the adic completion exactly when its residue
is an n-th power, for n outside v.