Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Density-lift through the fixed-field subextension

Abstract

Density-lift through the fixed-field subextension.

Theorem 1.1 (Density-lift through the fixed-field subextension).

Lean statement: D5/S3/Factorization/Galois/Chebotarev/FixedFieldDensity.density_lift_through_fixedField

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

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

Commentary.

Density-lift through the fixed-field subextension (Sharifi 7.2.2 Step 1, p. 143). Let σ ∈ Gal(L/K), E = L^⟨σ⟩ the fixed field of the cyclic subgroup ⟨σ⟩, and σ_E ∈ Gal(L/E) the corresponding element. Given the abelian-case density over E for the Frobenius-fibre of σ_E (value 1/|Gal(L/E)|), the density over K of the Frobenius class of σ is |C|/|G|.

References