Frobenius bases at completely split places

Let M/K be an abelian extension of number fields whose Galois group has exponent a prime p, for instance the Kummer extension K(U_S^{1/p}) generated by the p-th roots of the S-units of a field containing the p-th roots of unity, and let L be an intermediate field. An unramified finite place v of K has a single Frobenius element Frob_v ∈ Gal(M/K) (NumberFieldArithmetic.artinElementAway).

Suppose that the Frobenius elements of M/L at the places of L above the places of K outside a finite set S generate Gal(M/L). This file shows that the Frobenius elements of M/K at finitely many places v ∉ S of K that have a place of local degree one in L already form a basis of Gal(M/L), viewed as a subgroup of Gal(M/K): there is a finite set T of finite places of K, disjoint from S, such that

• the elements Frob_v for v ∈ T generate Gal(M/L), and there are as few of them as possible: p ^ #T = [M : L];
• every v ∈ T has a place of L above it of local degree one.

The point is that a Frobenius element of M/L at a place w of L above v is the power Frob_v ^ f(w/v) (NumberField.restrictScalars_eq_pow_inertiaDeg), and f(w/v) divides the order of Frob_v, which divides p. So either f(w/v) = p and the Frobenius element of M/L at w is trivial, or f(w/v) = 1 and it is Frob_v itself. The Frobenius elements at places of residue degree one therefore generate Gal(M/L) on their own, and an 𝔽_p-basis of Gal(M/L) can be extracted from them (TauCeti.exists_finset_subset_closure_eq_natCard_eq_pow).

This is the choice of the auxiliary set T in Milne's Kummer-theoretic proof of the second fundamental inequality, applied with M = K(U_S^{1/p}) and L/K cyclic of degree p. The generation hypothesis is the conclusion of Milne's Proposition 4.7 for the extension M/L, that the Frobenius elements outside a finite set generate the Galois group of an abelian extension. It is proved from the first fundamental inequality in TauCeti.ClassFieldTheory.closure_isArithFrobAt_eq_top_tower.

Main results

• TauCeti.NumberField.exists_finset_closure_artinElementAway_eq_range_restrictScalarsHom: the finite set T.

References

• J. S. Milne, Class Field Theory, v4.03, Chapter VII, §6 (the choice of T in the proof of the second inequality) and Proposition 4.7.

theorem TauCeti.NumberField.exists_finset_closure_artinElementAway_eq_range_restrictScalarsHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] {p : ℕ} (hp : Nat.Prime p) (hexp : Monoid.exponent Gal(M/K) ∣ p) (hab : ∀ (σ τ : Gal(M/K)), Commute σ τ) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (hur : ∀ v ∉ S, ∀ (Q : Ideal (NumberField.RingOfIntegers M)) [inst : Q.IsPrime] [Q.LiesOver v.asIdeal], Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) Q) (hgen : Subgroup.closure {τ : Gal(M/L) | ∃ v ∉ S, ∃ (Q : { Q : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers M) // Q.asIdeal.LiesOver v.asIdeal }), IsArithFrobAt (NumberField.RingOfIntegers L) τ (↑Q).asIdeal} = ⊤) : ∃ (T : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))), Disjoint S T ∧ Subgroup.closure (NumberFieldArithmetic.artinElementAway hab S hur '' ↑T) = (AlgEquiv.restrictScalarsHom K).range ∧ p ^ T.card = Module.finrank L M ∧ ∀ 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

A basis of Frobenius elements at completely split places. Let M/K be an abelian extension of number fields whose Galois group has exponent dividing a prime p, unramified at the finite places outside a finite set S, and let L be an intermediate field. Suppose that the Frobenius elements of M/L at the primes of M above the places of K outside S generate Gal(M/L). Then there is a finite set T of finite places of K, disjoint from S, such that the Frobenius elements Frob_v ∈ Gal(M/K), v ∈ T, generate the subgroup Gal(M/L), with p ^ #T = [M : L], and every v ∈ T has a place of L above it of local degree one.

The equation p ^ #T = [M : L] says that T is as small as possible: the Frob_v with v ∈ T form a basis of Gal(M/L) as an 𝔽_p-vector space.