ZHat-Artin mapPrime-power reductions of the genuine cyclotomic character detect the full rational cyclotomic automorphism. Restricting that automorphism through actual finite cyclotomic levels then detects every finite coordinate of the rational cyclotomic ZHat-extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField IsMulCommutative
open NumberField ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (p : Nat.Primes) : Fact p.1.PrimeIf all prime-power character reductions of the full cyclotomic global Artin symbol have square one, then the corresponding Artin symbol in the actual rational ZHat-extension has square one.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField IsMulCommutative
open NumberField ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem
rationalCyclotomicZHatGlobalArtin_sq_eq_one_of_character_reductions
(a : IdeleGroup ℚ)
(h :
∀ (p : Nat.Primes) (k : ℕ),
Units.map (PadicInt.toZModPow k).toMonoidHom
(KummerTheory.rationalCyclotomicCharacterPrimeProduct
(infiniteGlobalArtinMonoidHom
ℚ KummerTheory.rationalCyclotomicField a) p) ^ 2 =
1) :
rationalCyclotomicZHatGlobalArtin a ^ 2 = 1Prime-power square-one identities force the rational cyclotomic idele value itself to be trivial. Torsion-freeness of ZHat removes the residual order-two ambiguity.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField IsMulCommutative
open NumberField ClassFormation
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem
rationalCyclotomicZHatIdeleValue_eq_one_of_character_reductions
(a : IdeleGroup ℚ)
(h :
∀ (p : Nat.Primes) (k : ℕ),
Units.map (PadicInt.toZModPow k).toMonoidHom
(KummerTheory.rationalCyclotomicCharacterPrimeProduct
(infiniteGlobalArtinMonoidHom
ℚ KummerTheory.rationalCyclotomicField a) p) ^ 2 =
1) :
rationalCyclotomicZHatIdeleValue a = 1