Frobenius elements for a group acting on a ring extension

This file supplements Mathlib's IsArithFrobAt API with facts about a monoid or group acting on a commutative ring extension S/R. All of them are stated at ring level, so they are available independently of any number-field or Legendre-symbol specialization.

Two are properties of a single Frobenius element. The defining congruence has #(R ⧸ Q ∩ R) as its exponent, so it makes that residue ring finite and therefore forces Q ≠ ⊥ over an infinite base. Iterating it n times replaces the exponent by its n-th power, which is what a Frobenius over an intermediate ring of residue degree n is required to satisfy.

For an ideal p of R, an element σ of the acting group cuts out the set of primes of S above p that admit σ as an arithmetic Frobenius. These sets need not be disjoint: at a ramified prime several elements are a Frobenius at once, so this is a family of fibers rather than a partition. Disjointness at a prime Q is what IsArithFrobAt.eq_of_isUnramifiedAt below supplies, under hypotheses of its own: a faithful action, S Noetherian, Q.primeCompl ≤ S⁰, and Algebra.IsUnramifiedAt R Q. Exhaustion of the primes above p needs a Frobenius to exist at each of them, which again carries hypotheses of its own, such as those of IsArithFrobAt.exists_of_isInvariant.

Main results

• IsArithFrobAt.eq_of_isUnramifiedAt — a Frobenius element is unique for a faithful action at an unramified prime of a Noetherian ring whose prime complement consists of non-zero-divisors.
• IsArithFrobAt.ne_bot — a prime carrying a Frobenius element over an infinite base ring is nonzero.
• IsArithFrobAt.mk_pow_smul — the n-th power of a Frobenius element acts on the residue ring by the q ^ n-th power map.
• Ideal.nonempty_frobenius_fiber_equiv_of_isConj — conjugate elements have equipotent fibers above a fixed ideal of the base, as a bijection between them.
• Ideal.frobenius_fiber_card_eq_of_isConj — the Nat.card form of that equipotence.

The equipotence is the "distributed evenly" step of Chebotarev's density theorem: where the fibers do partition the primes above p, it is what lets a count over a whole conjugacy class be recovered from the count at a single representative. Because S is an arbitrary commutative ring the fibers may be infinite, and Nat.card is 0 on an infinite type; the bijection is therefore the primary statement and the Nat.card identity is derived from it.

Implementation notes

The bijection realizing the equipotence is not conjugation itself but the pointwise action P ↦ c • P of a witnessing element c; Mathlib's IsArithFrobAt.conj is what transports the Frobenius condition along it, sending a Frobenius σ at P to the Frobenius c * σ * c⁻¹ at c • P.

The source states the equipotence for the rings of integers of a Galois extension of number fields and under an unramifiedness hypothesis on p that it never uses. Both restrictions are dropped here: the transport argument uses only the generic Frobenius group-action API, and it is available at every prime.

References

• Sharifi, Algebraic Number Theory, Theorem 7.2.2 (p. 143).
• Stevenhagen–Lenstra, Chebotarëv and his density theorem, Appendix.
• Birkbeck–Brasca, chebotarev-density (Apache-2.0), commit 8575c9df1ae0a61120ab5c964c7911414254bec7, file CebotarevDensity/FixedFieldDensity.lean, declaration frobeniusFibre_card_eq_of_isConj (source line 54). The transport argument of nonempty_frobenius_fiber_equiv_of_isConj below, and the statement of the frobenius_fiber_card_eq_of_isConj derived from it, are adapted from that declaration; the source states only the Nat.card form.

theorem IsArithFrobAt.eq_of_isUnramifiedAt {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] [FaithfulSMul G S] {Q : Ideal S} [Q.IsPrime] (hQ : Q.primeCompl ≤ nonZeroDivisors S) [Algebra.IsUnramifiedAt R Q] [IsNoetherianRing S] {σ τ : G} (hσ : IsArithFrobAt R σ Q) (hτ : IsArithFrobAt R τ Q) : σ = τ

Suppose S is Noetherian and Q is a prime of S containing all zero-divisors. If the action of G on S is faithful and the extension is unramified at Q, then a Frobenius element of G at Q is unique.

theorem IsArithFrobAt.ne_bot {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [FaithfulSMul R S] [Infinite R] [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] {Q : Ideal S} {σ : G} (H : IsArithFrobAt R σ Q) : Q ≠ ⊥

A prime carrying an arithmetic Frobenius over an infinite base is nonzero. The defining congruence has the cardinality of R ⧸ Q ∩ R as its exponent, so it forces that residue ring to be finite; over an infinite R this rules out Q = ⊥.

theorem IsArithFrobAt.mk_pow_smul {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Monoid G] [MulSemiringAction G S] [SMulCommClass G R S] {Q : Ideal S} {σ : G} (H : IsArithFrobAt R σ Q) (n : ℕ) (x : S) : (Ideal.Quotient.mk Q) (σ ^ n • x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q) ^ n

Powers of an arithmetic Frobenius raise the exponent. If σ is an arithmetic Frobenius at Q, then σ ^ n acts on the residue ring S ⧸ Q as the q ^ n-th power map, where q = #(R ⧸ Q ∩ R).

This is the congruence a tower formula rests on: over an intermediate ring whose prime below Q has residue ring of cardinality q ^ n, the n-th power of a Frobenius over the base satisfies the defining congruence of a Frobenius over that intermediate ring.

theorem Ideal.nonempty_frobenius_fiber_equiv_of_isConj {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (p : Ideal R) (σ σ' : G) (hc : IsConj σ σ') : Nonempty ({ P : Ideal S // ∃ (_ : P.IsPrime) (_ : P.LiesOver p) (_ : P ≠ ⊥), IsArithFrobAt R σ P } ≃ { P : Ideal S // ∃ (_ : P.IsPrime) (_ : P.LiesOver p) (_ : P ≠ ⊥), IsArithFrobAt R σ' P })

Equipotent Frobenius fibers. For IsConj σ σ', the action of a witnessing conjugator is a bijection from the nonzero primes of S above p with arithmetic Frobenius σ onto those with arithmetic Frobenius σ'. The bijection depends on the choice of conjugator, so it is stated as Nonempty.

theorem Ideal.frobenius_fiber_card_eq_of_isConj {R : Type u_1} {S : Type u_2} {G : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Group G] [MulSemiringAction G S] [SMulCommClass G R S] (p : Ideal R) (σ σ' : G) (hc : IsConj σ σ') : Nat.card { P : Ideal S // ∃ (_ : P.IsPrime) (_ : P.LiesOver p) (_ : P ≠ ⊥), IsArithFrobAt R σ P } = Nat.card { P : Ideal S // ∃ (_ : P.IsPrime) (_ : P.LiesOver p) (_ : P ≠ ⊥), IsArithFrobAt R σ' P }

Conjugate elements have fibers of the same Nat.card above a fixed ideal of the base. This is the cardinality shadow of nonempty_frobenius_fiber_equiv_of_isConj: when the fibers are infinite both sides are 0, so it is the bijection there that carries the content.