This file connects the cyclotomic ramification-index formula over ℤ to the finite-place completions used by the global Artin map. A rational prime outside the conductor is unramified at the actual chosen extension of its normalized finite-place absolute value.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (q : Nat.Primes) : Fact q.1.PrimeThe height-one prime of 𝓞 ℚ indexed by q lies over the principal prime ideal (q) of ℤ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
⟨q.2⟩theorem rationalPrime_liesOver_integerSpan
(q : Nat.Primes) :
(RayClass.rationalPrime q).asIdeal.LiesOver
(Ideal.span {(q.1 : ℤ)})The centre of the chosen finite-place extension in a rational cyclotomic level is algebraically unramified away from the level.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
⟨q.2⟩theorem rationalCyclotomicLevel_isUnramifiedAt_chosenFinitePlaceCentre
(m : ℕ+) (q : Nat.Primes)
(hq : ¬ q.1 ∣ (m : ℕ)) :
Algebra.IsUnramifiedAt (𝓞 ℚ)
(finitePlaceExtensionCentre
(K := ℚ)
(L := KummerTheory.rationalCyclotomicLevel m)
(RayClass.rationalPrime q)
(chosenFinitePlaceExtension
(L := KummerTheory.rationalCyclotomicLevel m)
(RayClass.rationalPrime q))).asIdealA rational cyclotomic level is unramified at every chosen finite place whose underlying rational prime does not divide the level.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (q : Nat.Primes) : Fact q.1.Prime :=
⟨q.2⟩theorem rationalCyclotomicLevel_chosenFinitePlaceIsUnramified
(m : ℕ+) (q : Nat.Primes)
(hq : ¬ q.1 ∣ (m : ℕ)) :
ChosenFinitePlaceIsUnramified
(K := ℚ)
(L := KummerTheory.rationalCyclotomicLevel m)
(RayClass.rationalPrime q)