The actual rational cyclotomic character is detected by all of its prime-power reductions. In particular, if every reduction of every p-adic character coordinate has square one, then the underlying automorphism of the full rational cyclotomic field has square one.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocityinstance (p : Nat.Primes) : Fact p.1.PrimeAn automorphism of the full rational cyclotomic field has square one as soon as every prime-power reduction of its genuine cyclotomic character has square one.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace GlobalClassFieldTheory
namespace Reciprocity
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicAutomorphism_sq_eq_one_of_character_reductions
(σ :
KummerTheory.rationalCyclotomicField ≃ₐ[ℚ]
KummerTheory.rationalCyclotomicField)
(h :
∀ (p : Nat.Primes) (k : ℕ),
Units.map (PadicInt.toZModPow k).toMonoidHom
(KummerTheory.rationalCyclotomicCharacterPrimeProduct
σ p) ^ 2 =
1) :
σ ^ 2 = 1