Frobenius power criteria for local units

Let M/K be a Galois extension of number fields containing a primitive n-th root of unity in K. An n-th root α ∈ M of a ∈ K is fixed by an arithmetic Frobenius above a finite place v exactly when a is an n-th power in K_v, provided n avoids v and a is a v-unit. Neither a nor α needs to be integral.

Consequently, if Gal(M/L) is generated by a family of these Frobenius elements, then α lies in L exactly when a is a power in all their base-field completions. This applies to S-units at places outside S, including S-units with denominators, and supplies the criterion needed to identify the kernel of their map to the local power classes.

The argument clears a denominator separately at each place and uses the integral power residue criterion IsArithFrobAt.smul_eq_self_iff and the Hensel comparison HeightOneSpectrum.exists_pow_eq_adicCompletion_iff. Comparing different roots uses TauCeti.exists_eq_algebraMap_mul_of_pow_eq.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, Lemma 6.3 and proof of Lemma 6.9.

theorem IsArithFrobAt.apply_eq_self_iff_exists_pow_eq_adicCompletion {K : Type u_1} {M : Type u_2} [Field K] [NumberField K] [Field M] [Algebra K M] {σ : Gal(M/K)} {Q : Ideal (NumberField.RingOfIntegers M)} [Q.IsPrime] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} [Q.LiesOver v.asIdeal] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q) {n : ℕ} {ζ : NumberField.RingOfIntegers K} (hζ : IsPrimitiveRoot ζ n) (hn : ↑n ∉ v.asIdeal) {a : K} {α : M} (ha : (IsDedekindDomain.HeightOneSpectrum.valuation K v) a = 1) (hα : α ^ n = (algebraMap K M) a) : σ α = α ↔ ∃ (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v), b ^ n = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) a

A Frobenius fixes a radical of a local unit exactly when its radicand is a power in the base-field completion. The radicand and its root may have denominators.

theorem TauCeti.NumberField.mem_intermediateField_iff_forall_exists_pow_eq_adicCompletion {K : Type u_1} {M : Type u_2} [Field K] [NumberField K] [Field M] [Algebra K M] [IsGalois K M] {L : IntermediateField K M} {ι : Type u_3} {σ : ι → Gal(M/K)} {Q : ι → Ideal (NumberField.RingOfIntegers M)} [∀ (i : ι), (Q i).IsPrime] {v : ι → IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} [∀ (i : ι), (Q i).LiesOver (v i).asIdeal] {n : ℕ} {ζ : NumberField.RingOfIntegers K} {a : K} {α : M} (hσ : ∀ (i : ι), IsArithFrobAt (NumberField.RingOfIntegers K) (σ i) (Q i)) (hL : L.fixingSubgroup = Subgroup.closure (Set.range σ)) (hζ : IsPrimitiveRoot ζ n) (hn : ∀ (i : ι), ↑n ∉ (v i).asIdeal) (ha : ∀ (i : ι), (IsDedekindDomain.HeightOneSpectrum.valuation K (v i)) a = 1) (hα : α ^ n = (algebraMap K M) a) : α ∈ L ↔ ∀ (i : ι), ∃ (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion K (v i)), b ^ n = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K (v i))) a

A radical of a local unit lies in the subfield cut out by Frobenius elements exactly when its radicand is a power in every corresponding completion. In particular this applies to S-unit radicands at places outside S.

theorem TauCeti.NumberField.exists_mem_intermediateField_pow_eq_iff_forall_exists_pow_eq_adicCompletion {K : Type u_1} {M : Type u_2} [Field K] [NumberField K] [Field M] [Algebra K M] [IsGalois K M] {L : IntermediateField K M} {ι : Type u_3} {σ : ι → Gal(M/K)} {Q : ι → Ideal (NumberField.RingOfIntegers M)} [∀ (i : ι), (Q i).IsPrime] {v : ι → IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} [∀ (i : ι), (Q i).LiesOver (v i).asIdeal] {n : ℕ} {ζ : NumberField.RingOfIntegers K} {a : K} {α : M} (hσ : ∀ (i : ι), IsArithFrobAt (NumberField.RingOfIntegers K) (σ i) (Q i)) (hL : L.fixingSubgroup = Subgroup.closure (Set.range σ)) (hζ : IsPrimitiveRoot ζ n) (hn : ∀ (i : ι), ↑n ∉ (v i).asIdeal) (ha : ∀ (i : ι), (IsDedekindDomain.HeightOneSpectrum.valuation K (v i)) a = 1) (hα : α ^ n = (algebraMap K M) a) : (∃ β ∈ L, β ^ n = (algebraMap K M) a) ↔ ∀ (i : ι), ∃ (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion K (v i)), b ^ n = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K (v i))) a

Power classes in an intermediate field are detected by local powers at a family of Frobenius generators, for radicands that are units at those places.