Surjectivity of a local cyclotomic character #
This file gives a criterion for the local p-adic cyclotomic character to be surjective: every
p-power cyclotomic polynomial must be irreducible over the base field. It is intended for local
Galois-theory applications where those finite-layer irreducibility results are available; see
Serre, Local Fields, Chapter IV, §4.
theorem
TauCeti.localCyclotomicCharacter_surjective_of_irreducible
{p : ℕ}
[Fact (Nat.Prime p)]
{K : Type u_1}
[Field K]
[CharZero K]
(hirr : ∀ (n : ℕ), Irreducible (Polynomial.cyclotomic (p ^ n) K))
:
The local p-adic cyclotomic character is surjective if all p-power cyclotomic
polynomials are irreducible over the base field.