Auxiliary places for the Kummer second inequality

Let K be a number field containing the p-th roots of unity, let S be a finite set of finite places containing the places above the prime p, and put M = K(U_S^{1/p}). For every intermediate field L, this file chooses a finite set T of auxiliary places with the four properties needed in the counting step of the Kummer proof of the second fundamental inequality:

• S and T are disjoint;
• p ^ #T = [M : L];
• the S-units surject onto the product of the local unit p-th power classes at T;
• every place in T has a place of L above it of local degree one.

The Frobenius elements outside S generate Gal(M/L) by the first fundamental inequality. The Frobenius-basis theorem extracts T; its cardinality identity then makes the Kummer-theoretic counting bound for local power classes an equality.

Main result

• TauCeti.ClassFieldTheory.exists_auxiliaryPlaces_unitLocalPowerClassMap_surjective: the auxiliary set T, including its cardinality, local-power-class and local-degree properties.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §6, especially Lemma 6.9 and the proof of the second inequality.

theorem TauCeti.ClassFieldTheory.exists_auxiliaryPlaces_unitLocalPowerClassMap_surjective {K E : Type} [Field K] [NumberField K] [Field E] [Algebra K E] {p : ℕ} (hp : Nat.Prime p) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hpS : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), ↑p ∈ v.asIdeal → v ∈ S) {ζ : NumberField.RingOfIntegers K} (hζ : IsPrimitiveRoot ζ p) (hroots : ∀ a ∈ (↑S).unit K, ∃ (x : E), x ^ p = (algebraMap K E) ↑a) (L : IntermediateField K ↥(kummerField E p ((↑S).unit K))) [NumberField ↥L] : ∃ (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hST : Disjoint ↑S ↑T), p ^ T.card = Module.finrank ↥L ↥(kummerField E p ((↑S).unit K)) ∧ Function.Surjective ⇑((↑S).unitLocalPowerClassMap (↑T) hST p) ∧ ∀ v ∈ T, ∃ (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥L) // w.asIdeal.LiesOver v.asIdeal }), Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion ↥L ↑w) = 1

Auxiliary places for the Kummer second inequality. Let p be prime, let S contain all finite places above p, and let M = K(U_S^{1/p}) in an ambient field containing the required radicals. For every intermediate field L/K in M, there is a finite set T, disjoint from S, such that p ^ #T = [M : L], the S-units surject onto the local unit p-th power classes at T, and every place in T has a place of L above it of local degree one.