Finite congruences from local cyclotomic primary data

This file converts a power in an adic completion into congruences of global integers. The approximation statement is stronger than the depth needed in the cyclotomic application: if an integral element is a q-th power in the completion at v, then it is congruent to a q-th power modulo every power of v.

For the cyclotomic prime, depth p + 1 gives the finite hyperprimary condition used in one-sided Kummer reciprocity.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.exists_integral_pow_congr_mod_prime_pow_of_adic_pow {K : Type u} [Field K] [NumberField K] (v : FinitePrime K) (q n : ℕ) (hq : q ≠ 0) (η : NumberField.RingOfIntegers K) (hroot : ∃ (y : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), y ^ q = (algebraMap (NumberField.RingOfIntegers K) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) η) : ∃ (b : NumberField.RingOfIntegers K), η - b ^ q ∈ v.asIdeal ^ n

If an integral element is a nontrivial power in the completion at v, then it is congruent to the same power of a global integer modulo every prescribed power of v.

def NumberTheory.CyclotomicCharacter.InverseExtension.IsFinitePrimaryAtCyclotomicPrime {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) : Prop

The finite hyperprimary condition at the cyclotomic prime: the numerator is a cyclotomic-prime unit and is a p-th power modulo λ^(p+1).

Equations

• One or more equations did not get rendered due to their size.

theorem NumberTheory.CyclotomicCharacter.InverseExtension.isFinitePrimaryAtCyclotomicPrime_of_adic_pthPower {p : ℕ} [Fact (Nat.Prime p)] (η : NumberField.RingOfIntegers (PrimeCyclotomicField p)) (hηPrime : η ∉ (cyclotomicPrime p).asIdeal) (hroot : ∃ (y : IsDedekindDomain.HeightOneSpectrum.adicCompletion (PrimeCyclotomicField p) (cyclotomicPrime p)), y ^ p = (algebraMap (NumberField.RingOfIntegers (PrimeCyclotomicField p)) (IsDedekindDomain.HeightOneSpectrum.adicCompletion (PrimeCyclotomicField p) (cyclotomicPrime p))) η) : IsFinitePrimaryAtCyclotomicPrime η

An integral cyclotomic-prime unit with a p-th root in the completion is finite-primary.