Tagged Frobenius fibres in a cyclotomic compositum

Let L / K be Galois and let M = L(μ_m). When m is coprime to the discriminant of L, the joint restriction isomorphism

Gal(M/K) ≃ Gal(L/K) × (ZMod m)ˣ

allows a Frobenius condition over M / K to carry both a prescribed element σ : Gal(L/K) and a cyclotomic tag τ : (ZMod m)ˣ. This file packages the resulting prime fibre and proves that distinct tags give disjoint fibres, whatever the base elements.

The point is slightly stronger than injectivity of the product equivalence. Equality of Frobenius fibres is indexed by conjugacy classes, so one must show that two elements whose cyclotomic coordinates differ cannot be conjugate. Applying the cyclotomic character reduces conjugacy to equality because (ZMod m)ˣ is commutative.

Main definitions

• NumberField.Chebotarev.taggedFrobeniusPrimeSet: the primes whose Artin class over M / K is represented by the tag (σ, τ).

Main results

• NumberField.Chebotarev.disjoint_taggedFrobeniusPrimeSet: the fibres of (σ₁, τ) and (σ₂, υ) are disjoint whenever τ ≠ υ.
• NumberField.Chebotarev.pairwise_disjoint_taggedFrobeniusPrimeSet: the tagged fibres for a fixed σ are pairwise disjoint as τ varies.

References

The tagged fibres and their disjointness for distinct τ belong to the cyclotomic-crossing step of the proof of the Chebotarev density theorem in Sharifi, Algebraic Number Theory, Theorem 7.2.2, Step 2. The Birkbeck--Brasca development CBirkbeck/chebotarev-density (Apache-2.0), at commit 55a89985d47a3befcf6069aca1da250ff088b5c7, records the same disjointness inside the private exists_cyclotomicCrossing_fibres in CebotarevDensity/Abelian.lean, where it follows from a global tag recording the cyclotomic component of each prime's Frobenius; here it is proved instead by passing conjugacy through the cyclotomic character.

noncomputable def NumberField.Chebotarev.taggedFrobeniusPrimeSet (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))

The Frobenius fibre carrying a fixed base element and cyclotomic tag. Under the joint restriction isomorphism Gal(M/K) ≃ Gal(L/K) × (ZMod m)ˣ, this is the prime fibre of the conjugacy class represented by the inverse image of (σ, τ).

The number-field and Galois structures on M are consequences of the cyclotomic tower, so they are installed internally rather than required from callers.

@[simp]

theorem NumberField.Chebotarev.taggedFrobeniusPrimeSet_def (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [NumberField M] [IsGalois K M] (hcop : (discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) : taggedFrobeniusPrimeSet K L M m hcop hζ σ τ = frobeniusPrimeSet K M (ConjClasses.mk ((IsCyclotomicExtension.galEquivProd K L M m hcop hζ).symm (σ, τ)))

The tagged fibre is the ordinary Frobenius fibre of the conjugacy class represented by the corresponding element of Gal(M/K). This is the unfolding interface for applying results about frobeniusPrimeSet; the instances on M are precisely those that its right-hand side requires.

@[simp]

theorem NumberField.Chebotarev.mem_taggedFrobeniusPrimeSet_iff (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) {𝔭 : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)} : 𝔭 ∈ taggedFrobeniusPrimeSet K L M m hcop hζ σ τ ↔ ∃ (hur : ∀ (Q : Ideal (RingOfIntegers M)) [inst : Q.IsPrime] [Q.LiesOver 𝔭.asIdeal], Algebra.IsUnramifiedAt (RingOfIntegers K) Q), artinSymbol 𝔭.asIdeal hur = ConjClasses.mk ((IsCyclotomicExtension.galEquivProd K L M m hcop hζ).symm (σ, τ))

Membership in a tagged fibre, unfolded into the corresponding Artin-class condition.

theorem NumberField.Chebotarev.disjoint_taggedFrobeniusPrimeSet (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ₁ σ₂ : Gal(L/K)) {τ υ : (ZMod m)ˣ} (hτυ : τ ≠ υ) : Disjoint (taggedFrobeniusPrimeSet K L M m hcop hζ σ₁ τ) (taggedFrobeniusPrimeSet K L M m hcop hζ σ₂ υ)

Distinct cyclotomic tags give disjoint Frobenius fibres. The fibres indexed by (σ₁, τ) and (σ₂, υ) are disjoint whenever τ ≠ υ, whatever σ₁ σ₂ : Gal(L/K).

Disjointness is what allows the densities of the separate tagged fibres to be added, so this is the form consumed by lower-bound density estimates over the compositum.

theorem NumberField.Chebotarev.pairwise_disjoint_taggedFrobeniusPrimeSet (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) : Pairwise (Function.onFun Disjoint (taggedFrobeniusPrimeSet K L M m hcop hζ σ))

Tagged fibres over a fixed base element are pairwise disjoint. For a fixed σ : Gal(L/K), the fibres indexed by (σ, τ) are pairwise disjoint as τ : (ZMod m)ˣ varies.