Elements with a prescribed divisibility condition on their order

In the cyclic auxiliary group used by the Chebotarev crossing, the useful tags are the elements whose order is divisible by the order of the chosen Frobenius element. This file gives that finite carrier together with its membership and divisibility API.

Main definitions

• TauCeti.NumberField.Chebotarev.taggedElements: elements whose order is divisible by a given natural number.

Main results

• TauCeti.NumberField.Chebotarev.mem_taggedElements_iff: the defining membership condition.
• TauCeti.NumberField.Chebotarev.taggedElements_subset_of_dvd: divisibility makes the tag carrier shrink.
• TauCeti.NumberField.Chebotarev.card_taggedElements_eq_sum_totient: the exact cyclic count, expressed as a sum of Euler totients over the allowed orders.
• TauCeti.NumberField.Chebotarev.card_taggedElements_cyclic: the exact count as #H times an Euler product over the primes of f, over ℝ.
• TauCeti.NumberField.Chebotarev.le_card_taggedElements_cyclic: a uniform lower bound for that count, over ℝ.

References

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

noncomputable def TauCeti.NumberField.Chebotarev.taggedElements {H : Type u_1} [Group H] [Fintype H] (f : ℕ) : Finset H

The elements of a finite group whose order is divisible by f.

The carrier is deliberately a Finset, so the tags can be indexed by their order.

@[simp]

theorem TauCeti.NumberField.Chebotarev.mem_taggedElements_iff {H : Type u_1} [Group H] [Fintype H] {f : ℕ} {τ : H} : τ ∈ taggedElements f ↔ f ∣ orderOf τ

Membership in taggedElements, unfolded to the order divisibility condition.

theorem TauCeti.NumberField.Chebotarev.taggedElements_subset_of_dvd {H : Type u_1} [Group H] [Fintype H] {f g : ℕ} (hfg : f ∣ g) : taggedElements g ⊆ taggedElements f

A stronger divisibility requirement gives a smaller tagged carrier.

@[simp]

theorem TauCeti.NumberField.Chebotarev.taggedElements_one {H : Type u_1} [Group H] [Fintype H] : taggedElements 1 = Finset.univ

Every element is tagged for the vacuous order condition f = 1.

theorem TauCeti.NumberField.Chebotarev.card_taggedElements_eq_sum_totient {H : Type u_1} [Group H] [Fintype H] [IsCyclic H] (f : ℕ) : (taggedElements f).card = ∑ d ∈ (Fintype.card H).divisors with f ∣ d, d.totient

In a finite cyclic group, count the tagged elements by their exact orders.

theorem TauCeti.NumberField.Chebotarev.card_taggedElements_cyclic {H : Type u_1} [Group H] [Fintype H] [IsCyclic H] (f : ℕ) (hf : f ∣ Nat.card H) : ↑(taggedElements f).card = ↑(Nat.card H) * ∏ p ∈ f.primeFactors, (1 - ↑p ^ (-↑((Nat.card H).factorization p - f.factorization p + 1)))

The exact tagged count in a cyclic group. When f divides the order of H, the number of elements whose order is divisible by f is #H times a product over the primes dividing f.

This restates IsCyclic.card_filter_dvd_orderOf_eq_mul_prod_primeFactors for the taggedElements carrier and over ℝ. No positivity hypothesis on f is needed: f divides Nat.card H, which is nonzero, so f is nonzero already.

theorem TauCeti.NumberField.Chebotarev.le_card_taggedElements_cyclic {H : Type u_1} [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 H) ≤ ↑(taggedElements f).card

The tagged elements of a cyclic group make up at least a fixed proportion of it. When f ^ r divides the order of H, at least (1 - 2 ^ (-r)) ^ #f.primeFactors of the elements of H have order divisible by f. The exact proportion is card_taggedElements_cyclic.

This restates IsCyclic.le_card_filter_dvd_orderOf for the taggedElements carrier and over ℝ, which is where the density statements consuming it live. No positivity hypothesis on f is needed: f ^ r divides Nat.card H, which is nonzero, so f is nonzero already.