Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

𝔓 is the unique prime of 𝓞 L above 𝔓 ∩ 𝓞 E

Abstract

𝔓 is the unique prime of 𝓞 L above 𝔓 ∩ 𝓞 E.

Theorem 1.1 (𝔓 is the unique prime of 𝓞 L above 𝔓 ∩ 𝓞 E).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/FixedFieldFrobeniusCounting.eq_of_liesOver_under_E_of_frobenius

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/Chebotarev/FixedFieldFrobeniusCounting.eq_of_liesOver_under_E_of_frobenius (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

Let E = L^⟨σ⟩. If 𝔓 is a prime of L above an unramified prime of K, its arithmetic K-Frobenius is σ, and ord(σ) = |Gal(L/E)|, then 𝔓 is the unique prime of L above 𝔓 ∩ 𝓞 E. The hypotheses make the stabilizer of 𝔓 in Gal(L/E) the whole group; transitivity on primes above 𝔓 ∩ 𝓞 E gives uniqueness.

References