Integral radicals of local units #
An n-th root of a local unit in a number field can be multiplied by an integer outside
the chosen prime to obtain an integral radical whose radicand is still a local unit.
This allows ramification and Frobenius criteria for integral radicals to apply to radicals
with denominators. The denominator is supplied by
HeightOneSpectrum.exists_primeCompl_mul_eq_of_integer.
References #
- J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 6.3 and Appendix, Proposition A.5.
theorem
IsDedekindDomain.HeightOneSpectrum.exists_integral_pow_eq_of_valuation_eq_one
{K : Type u_1}
{M : Type u_2}
[Field K]
[NumberField K]
[Field M]
[Algebra K M]
(v : HeightOneSpectrum (NumberField.RingOfIntegers K))
{n : ℕ}
(hn : n ≠ 0)
{a : K}
{α : M}
(ha : (valuation K v) a = 1)
(hα : α ^ n = (algebraMap K M) a)
:
∃ (d : NumberField.RingOfIntegers K) (c : NumberField.RingOfIntegers K) (β : NumberField.RingOfIntegers M),
d ∉ v.asIdeal ∧ c ∉ v.asIdeal ∧ (algebraMap (NumberField.RingOfIntegers K) K) c = (algebraMap (NumberField.RingOfIntegers K) K) d ^ n * a ∧ ↑β = (algebraMap (NumberField.RingOfIntegers K) M) d * α ∧ β ^ n = (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers M)) c
A radical of a local unit becomes integral after multiplication by an integer outside the chosen prime, and its new radicand remains outside that prime.