Local power classes of S-units

For disjoint sets of finite places S and T, an S-unit determines a unit power class at each place of T. The resulting homomorphism has kernel consisting of the S-units that are powers in all these completions.

If a Galois extension contains the radicals of the S-units and the Frobenius elements at T generate the subgroup fixing L, this kernel is exactly the S-units that are powers in L. This identifies the source quotient in the counting proof of local power-class surjectivity with the quotient used by Kummer theory.

That counting proof is Milne's Lemma 6.9. Suppose K contains the n-th roots of unity, S and T are finite, n is a unit at the places of T, the extension is generated by the radicals of the S-units, and n ^ #T ≤ [M : L]. Then the map is surjective. By Kummer theory the image has at least [M : L] elements, while each place of T contributes #μ_n(K_v) = n unit power classes. This surjectivity is the hypothesis on the auxiliary set T in the Kummer-theoretic proof of the second fundamental inequality.

The local target uses the depth-zero unit filtration, so it retains only unit classes; the valuation classes of the completion are excluded.

Main results

• Set.ker_unitLocalPowerClassMap: the kernel is the set of S-units that are n-th powers in L.
• Set.unitLocalPowerClassMap_surjective: the map is surjective when n ^ #T ≤ [M : L].

References

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

@[reducible, inline]

abbrev Set.UnitLocalPowerClasses {K : Type u_1} [Field K] [NumberField K] (T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (n : ℕ) : Type u_1

The product of the local unit n-th power-class groups at the places of T.

noncomputable def Set.unitLocalPowerClassMap {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) (n : ℕ) : ↥(S.unit K) →* T.UnitLocalPowerClasses n

The homomorphism taking an S-unit to its unit n-th power classes at the places of T. Disjointness ensures that every coordinate is a local unit.

@[simp]

theorem Set.unitLocalPowerClassMap_apply {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) (n : ℕ) (u : ↥(S.unit K)) (v : ↑T) : (S.unitLocalPowerClassMap T hST n) u v = ↑⟨(Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v))) ↑u, ⋯⟩

A coordinate of the local power-class map is the class of the corresponding local unit.

theorem Set.exists_mem_unit_of_unitLocalPowerClassMap_surjective {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) {n : ℕ} (hsurj : Function.Surjective ⇑(S.unitLocalPowerClassMap T hST n)) (y : (v : ↑T) → (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)ˣ) (hy : ∀ (v : ↑T), Valued.v ↑(y v) = 1) : ∃ u ∈ S.unit K, ∀ (v : ↑T), ((Units.map ↑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v))) u)⁻¹ * y v ∈ (powMonoidHom n).range

If the S-units surject onto the local unit n-th power classes at T, then every family of local units at the places of T agrees with a single S-unit up to n-th powers.

theorem Set.unitLocalPowerClassMap_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) {n : ℕ} (hn : n ≠ 0) (u : ↥(S.unit K)) : (S.unitLocalPowerClassMap T hST n) u = 1 ↔ ∀ (v : ↑T), ∃ (b : IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v), b ^ n = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K ↑v)) ↑↑u

An S-unit has trivial local power classes exactly when it has an n-th root in every completion indexed by T.

theorem Set.ker_unitLocalPowerClassMap {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) {M : Type u_2} [Field M] [Algebra K M] [IsGalois K M] {n : ℕ} (hn : n ≠ 0) (L : IntermediateField K M) (σ : ↑T → Gal(M/K)) (Q : ↑T → Ideal (NumberField.RingOfIntegers M)) [∀ (v : ↑T), (Q v).IsPrime] [∀ (v : ↑T), (Q v).LiesOver (↑v).asIdeal] (hσ : ∀ (v : ↑T), IsArithFrobAt (NumberField.RingOfIntegers K) (σ v) (Q v)) (hL : L.fixingSubgroup = Subgroup.closure (range σ)) {ζ : NumberField.RingOfIntegers K} (hζ : IsPrimitiveRoot ζ n) (havoid : ∀ (v : ↑T), ↑n ∉ (↑v).asIdeal) (hroots : ∀ a ∈ S.unit K, ∃ (α : M), α ^ n = (algebraMap K M) ↑a) : (S.unitLocalPowerClassMap T hST n).ker = (Subgroup.comap (Units.map ↑(algebraMap K ↥L)) (powMonoidHom n).range).subgroupOf (S.unit K)

The kernel of the S-unit local power-class map. Suppose M contains an n-th root of every S-unit, and Frobenius elements at the places of T generate Gal(M/L). Then an S-unit lies in the kernel precisely when its image in L is an n-th power. Neither set of places is required to be finite.

theorem Set.unitLocalPowerClassMap_surjective {K : Type u_1} [Field K] [NumberField K] (S T : Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint S T) {M : Type u_2} [Field M] [Algebra K M] [IsGalois K M] {n : ℕ} (hn : n ≠ 0) [Finite ↑S] [Finite ↑T] (L : IntermediateField K M) (σ : ↑T → Gal(M/K)) (Q : ↑T → Ideal (NumberField.RingOfIntegers M)) [∀ (v : ↑T), (Q v).IsPrime] [∀ (v : ↑T), (Q v).LiesOver (↑v).asIdeal] (hσ : ∀ (v : ↑T), IsArithFrobAt (NumberField.RingOfIntegers K) (σ v) (Q v)) (hL : L.fixingSubgroup = Subgroup.closure (range σ)) {ζ : NumberField.RingOfIntegers K} (hζ : IsPrimitiveRoot ζ n) (havoid : ∀ (v : ↑T), ↑n ∉ (↑v).asIdeal) (hroots : ∀ a ∈ S.unit K, ∃ (α : M), α ^ n = (algebraMap K M) ↑a) (hM : TauCeti.kummerField M n (S.unit K) = ⊤) (hT : n ^ Nat.card ↑T ≤ Module.finrank (↥L) M) : Function.Surjective ⇑(S.unitLocalPowerClassMap T hST n)

The S-units surject onto the local unit power classes (Milne VII, Lemma 6.9). Let K contain a primitive n-th root of unity and let S and T be disjoint finite sets of finite places, with n a unit at the places of T. Let M = K(U_S^{1/n}) be generated by the n-th roots of the S-units, and let L be an intermediate field such that Frobenius elements at the places of T generate Gal(M/L) and n ^ #T ≤ [M : L]. Then every family of unit n-th power classes at the places of T is the family of classes of a single S-unit.