The crossing constant of an auxiliary cyclic group

The cyclotomic crossing bounds the density of a Frobenius fibre from below by a quantity built from one auxiliary prime: the proportion of the auxiliary cyclic group H taken up by the tags — the elements whose order is divisible by the residue degree f — divided in addition by the order of Aut_K(L). Equivalently it is the proportion of Aut_K(L) × H represented by one automorphism paired with the tags. This file defines that quantity, crossingConstant, and bounds it below.

What the bound provides is uniformity: it depends on f only through the number of primes dividing f, and on the auxiliary group only through the level r in f ^ r ∣ #H. Raising r therefore pushes the crossing constant of every cyclic group of that level towards 1 / #Aut_K(L), uniformly in the group; the file closes with this limit, in the form a consumer choosing one auxiliary group per target value needs.

Main definitions

• TauCeti.NumberField.Chebotarev.crossingConstant: the tag proportion in H, divided by the order of Aut_K(L).

Main results

• TauCeti.NumberField.Chebotarev.crossingConstant_nonneg: the constant is nonnegative.
• TauCeti.NumberField.Chebotarev.le_crossingConstant: once f ^ r divides #H, the crossing constant is at least (1 - 2 ^ (-r)) ^ #f.primeFactors divided by the order of Aut_K(L).
• TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant: as the level r grows, that bound tends to 1 / #Aut_K(L), so every δ < 1 / #Aut_K(L) lies below the crossing constant of every cyclic group whose order is divisible by f ^ r, for a single r.
• TauCeti.NumberField.Chebotarev.exists_prime_coprime_lt_crossingConstant: that level is realised by (ZMod q)ˣ for a prime q coprime to any given nonzero N; the cyclotomic crossing takes N to be the discriminant of L.

References

The crossing construction follows R. Sharifi, Algebraic Number Theory, Theorem 7.2.2.

noncomputable def TauCeti.NumberField.Chebotarev.crossingConstant (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] {H : Type u_3} [Group H] [Fintype H] (f : ℕ) : ℝ

The crossing constant. The number of tagged elements of the auxiliary cyclic group H — those whose order is divisible by f — divided by #Aut_K(L) * #H.

That is the tag proportion within H, divided in addition by the order of Aut_K(L), which enters only through its order: the denominator that turns a count of tags into the density contributed by one auxiliary prime.

theorem TauCeti.NumberField.Chebotarev.crossingConstant_def (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] {H : Type u_3} [Group H] [Fintype H] (f : ℕ) : crossingConstant K L f = ↑(taggedElements f).card / (↑(Nat.card (L ≃ₐ[K] L)) * ↑(Nat.card H))

The crossing constant, written out. The characteristic rewrite: a consumer uses this rather than unfolding the definition.

Deliberately not a simp lemma. crossingConstant is itself the normal form — the bound le_crossingConstant is stated in terms of it, so unfolding it on sight would dissolve the conclusion a consumer is trying to apply.

theorem TauCeti.NumberField.Chebotarev.crossingConstant_nonneg (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] {H : Type u_3} [Group H] [Fintype H] (f : ℕ) : 0 ≤ crossingConstant K L f

The crossing constant is nonnegative. It is a ratio of cardinalities, so a consumer squeezing a density between bounds gets this without unfolding the definition.

theorem TauCeti.NumberField.Chebotarev.le_crossingConstant (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] {H : Type u_3} [Group H] [Fintype H] [IsCyclic H] (f r : ℕ) (hrpos : 0 < r) (hf : f ^ r ∣ Nat.card H) : (1 - 2 ^ (-↑r)) ^ f.primeFactors.card / ↑(Nat.card (L ≃ₐ[K] L)) ≤ crossingConstant K L f

The lower bound for the crossing constant. When f ^ r divides the order of the cyclic auxiliary group H, the crossing constant is at least (1 - 2 ^ (-r)) ^ #f.primeFactors divided by the order of Aut_K(L). The bound no longer mentions #H: the auxiliary group enters only through the level r.

Aut_K(L) is not assumed finite; when it is infinite both sides are 0.

theorem TauCeti.NumberField.Chebotarev.exists_forall_lt_crossingConstant (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] (f : ℕ) {δ : ℝ} (hδ : δ < 1 / ↑(Nat.card (L ≃ₐ[K] L))) : ∃ (r : ℕ), ∀ (H : Type u_4) [inst : Group H] [inst_1 : Fintype H] [IsCyclic H], f ^ r ∣ Nat.card H → δ < crossingConstant K L f

The crossing constant approaches 1 / #Aut_K(L). For every δ < 1 / #Aut_K(L) there is a level r such that the crossing constant of every cyclic group whose order is divisible by f ^ r exceeds δ.

The level depends only on δ, f and the order of Aut_K(L), not on the cyclic group, so a consumer that can choose an auxiliary group of any level pushes the crossing bound arbitrarily close to 1 / #Aut_K(L).

theorem TauCeti.NumberField.Chebotarev.exists_prime_coprime_lt_crossingConstant (K : Type u_1) (L : Type u_2) [CommSemiring K] [Semiring L] [Algebra K L] {f N : ℕ} (hf : f ≠ 0) (hN : N ≠ 0) {δ : ℝ} (hδ : δ < 1 / ↑(Nat.card (L ≃ₐ[K] L))) : ∃ (q : ℕ) (x : Fact (Nat.Prime q)), N.Coprime q ∧ δ < crossingConstant K L f

An auxiliary prime with a large crossing constant. For every δ < 1 / #Aut_K(L), every f ≠ 0 and every N ≠ 0 there is a prime q, coprime to N, such that the crossing constant of (ZMod q)ˣ at f exceeds δ.

The cyclotomic crossing takes N to be the absolute discriminant of L: coprimality to it is what the joint restriction IsCyclotomicExtension.galEquivProd needs to split the Galois group of L(μ_q) / K as Aut_K(L) × (ZMod q)ˣ.