Local primary data after pseudo-unit normalization #
This file transports an actual p-th root in the cyclotomic-prime
completion across a change of Kummer radicand by a p-th power. For an
integral normalized radicand coprime to the cyclotomic prime, the transported
root supplies the finite-primary congruence used by one-sided reciprocity.
theorem
NumberTheory.CyclotomicCharacter.InverseExtension.KummerPresentation.isFinitePrimaryAtCyclotomicPrime_of_localRoot_normalization
{p : ℕ}
[Fact (Nat.Prime p)]
{L : Type u}
[Field L]
[NumberField L]
[Algebra (PrimeCyclotomicField p) L]
[IsScalarTower ℚ (PrimeCyclotomicField p) L]
(E : InverseExtension p L)
(P : E.KummerPresentation)
(hlocal :
∃ (y : IsDedekindDomain.HeightOneSpectrum.adicCompletion (PrimeCyclotomicField p) (cyclotomicPrime p)),
y ^ p = (algebraMap (PrimeCyclotomicField p)
(IsDedekindDomain.HeightOneSpectrum.adicCompletion (PrimeCyclotomicField p) (cyclotomicPrime p)))
P.radicand)
(η : NumberField.RingOfIntegers (PrimeCyclotomicField p))
(c : (PrimeCyclotomicField p)ˣ)
(hη :
(algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (PrimeCyclotomicField p)) η = P.radicand * ↑c ^ p)
(hηPrime : η ∉ (cyclotomicPrime p).asIdeal)
:
A local p-th root of a Kummer radicand remains a local p-th root
after multiplying the radicand by the p-th power used in an integral
normalization. Consequently, a normalized numerator avoiding the
cyclotomic prime is finite-primary.