Frobenius fibres in a cyclotomic compositum

Let L / K be a Galois extension of number fields and let M = L(μ_m), with M / K Galois. An automorphism ρ of M / K is determined by two coordinates: its restriction to L, and its cyclotomic character IsPrimitiveRoot.autToPow, which records how it moves the m-th roots of unity. This file computes both coordinates of the Artin class of a prime 𝔭 of 𝓞 K that is unramified in M and does not divide m: the first is the Artin class of 𝔭 in L / K, with no power taken, and the second is 𝔑𝔭 mod m.

So the fibre of [ρ] over M is cut out of the fibre of [ρ|_L] over L by the congruence 𝔑𝔭 ≡ autToPow ρ (mod m). Since the character lands in the commutative group (ZMod m)ˣ, its value is a single residue even though the Artin class is only a conjugacy class. In the joint coordinates Gal(M/K) ≃ Gal(L/K) × (ZMod m)ˣ of IsCyclotomicExtension.galEquivProd, the fibre of the class of (σ, τ) consists of the primes in the fibre of [σ] over L with 𝔑𝔭 ≡ τ.

This is the Frobenius compatibility on which the cyclotomic crossing argument for the Chebotarev density theorem rests: it identifies which primes of K a Frobenius fibre of the compositum counts.

Unramifiedness in M and 𝔭 ∤ m are hypotheses. The second cannot be dropped: for m = 2 the field M is L, a prime above 2 may be unramified, and 𝔑𝔭 is then not a unit modulo m.

Main results

• NumberField.Chebotarev.mem_frobeniusPrimeSet_mk_iff_restrictNormal_autToPow: for 𝔭 unramified in M with 𝔭 ∤ m, the prime lies in the fibre of [ρ] over M exactly when it lies in the fibre of [ρ|_L] over L and autToPow ρ = 𝔑𝔭 in ZMod m.
• NumberField.Chebotarev.mem_frobeniusPrimeSet_galEquivProd_symm_iff: the same statement in the coordinates of IsCyclotomicExtension.galEquivProd.

References

• J. Neukirch, Algebraic Number Theory, Chapter I, §9, for Frobenius elements in towers.
• R. Sharifi, Algebraic Number Theory, Proposition 7.2.1 and the proof of Theorem 7.2.2, where the Frobenius of a cyclotomic compositum is read off from its restriction and its action on roots of unity.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_mk_iff_restrictNormal_autToPow {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 L] [IsGalois K M] {m : ℕ} [NeZero m] [IsCyclotomicExtension {m} L M] {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (hm : ↑m ∉ 𝔭.asIdeal) (hur : ∀ (Q : Ideal (RingOfIntegers M)) [inst : Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (ρ : Gal(M/K)) : 𝔭 ∈ frobeniusPrimeSet K M (ConjClasses.mk ρ) ↔ 𝔭 ∈ frobeniusPrimeSet K L (ConjClasses.mk (ρ.restrictNormal L)) ∧ ↑((IsPrimitiveRoot.autToPow K hζ) ρ) = ↑(Ideal.absNorm 𝔭.asIdeal)

The Frobenius fibre of the cyclotomic compositum. Let M = L(μ_m) for a Galois extension L / K, let ζ be a primitive m-th root of unity in M, and let 𝔭 be a prime of 𝓞 K that is unramified in M and does not divide m. Then 𝔭 lies in the fibre of the class of ρ : Gal(M/K) exactly when it lies in the fibre of the class of ρ|_L over L and the cyclotomic character of ρ is 𝔑𝔭 mod m.

The class of ρ is recovered from those two coordinates although only the first is a conjugacy class: the second lives in a commutative group, and an automorphism of M is determined by its restriction to L together with its cyclotomic character.

theorem NumberField.Chebotarev.mem_frobeniusPrimeSet_galEquivProd_symm_iff {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 L] [IsGalois K M] {m : ℕ} [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (discr L).natAbs.Coprime m) {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} (hm : ↑m ∉ 𝔭.asIdeal) (hur : ∀ (Q : Ideal (RingOfIntegers M)) [inst : Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) : 𝔭 ∈ frobeniusPrimeSet K M (ConjClasses.mk ((IsCyclotomicExtension.galEquivProd K L M m hcop hζ).symm (σ, τ))) ↔ 𝔭 ∈ frobeniusPrimeSet K L (ConjClasses.mk σ) ∧ ↑τ = ↑(Ideal.absNorm 𝔭.asIdeal)

The tagged Frobenius fibre of the cyclotomic compositum. In the coordinates Gal(M/K) ≃ Gal(L/K) × (ZMod m)ˣ of IsCyclotomicExtension.galEquivProd, a prime 𝔭 of 𝓞 K unramified in M and not dividing m lies in the fibre of the class of (σ, τ) exactly when it lies in the fibre of [σ] over L and 𝔑𝔭 ≡ τ (mod m).