Surjectivity of the cyclotomic Artin map #
Let F = K(μ_m) be an m-th cyclotomic extension of a number field K. This file proves that
the Artin map cyclotomicArtin K F m from the ray class group of cyclotomicModulus K m to
Gal(F/K) is surjective.
Main results #
NumberField.Chebotarev.cyclotomicArtin_surjective: the cyclotomic Artin map is surjective.
References #
- J. Neukirch, Algebraic Number Theory, Chapter VII, §13.
theorem
NumberField.Chebotarev.cyclotomicArtin_surjective
(K : Type u_1)
[Field K]
[NumberField K]
(F : Type u_2)
[Field F]
[NumberField F]
[Algebra K F]
(m : ℕ)
[NeZero m]
[IsCyclotomicExtension {m} K F]
[IsGalois K F]
:
Function.Surjective ⇑(cyclotomicArtin K F m)
The cyclotomic Artin map is surjective. For F = K(μ_m), every automorphism of F / K is
the Artin automorphism of a ray class of cyclotomicModulus K m.