Finite sets of places for the S-idele sequence

For an extension L/K of number fields, there is a finite set S of finite places of K containing all ramified places such that the primes of L above S generate the class group of L. The first condition permits local computations outside S using unramified units; the second makes every idele class of L have an S-idele representative. Together they allow the exact sequence of S-units, S-ideles and idele classes to be used without an extra existence hypothesis on S.

The construction uses the finite prime generators of ClassGroup.exists_finite_closure_classGroupMk_image_eq_top and the finite ramified support TauCeti.NumberField.ramifiedSupport.

References

• J. S. Milne, Class Field Theory, Chapter VII, §4, proof of Theorem 4.3.

theorem TauCeti.GlobalNumberFields.exists_finset_primesAbove_closure_eq_top_and_isUnramified (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ∃ (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))), Subgroup.closure (IsDedekindDomain.HeightOneSpectrum.classGroupMk '' IsDedekindDomain.HeightOneSpectrum.primesAbove (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↑S) = ⊤ ∧ ∀ (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)), IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w ∉ S → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) w.asIdeal

An extension of number fields has a finite set of base places outside which it is unramified and whose primes upstairs generate the class group. No Galois hypothesis is needed.