Finite cyclotomic levels are detected by their prime-power reductions, using mathlib's Chinese-remainder equivalence for ZMod. Surjectivity is obtained from the finite-intersection property for the closed fibers of the restriction maps to those levels.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormationinstance (p : Nat.Primes) : Fact p.1.PrimeThe p ^ k reduction of the cyclotomic character can be read from any finite cyclotomic level whose order is divisible by p ^ k.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicCharacterPrimeProduct_toZModPow_of_dvd
(σ : rationalCyclotomicField ≃ₐ[ℚ] rationalCyclotomicField)
(p : Nat.Primes) (k : ℕ) (n : ℕ+)
(h : p.1 ^ k ∣ (n : ℕ)) :
Units.map (PadicInt.toZModPow k).toMonoidHom
(rationalCyclotomicCharacterPrimeProduct σ p) =
ZMod.unitsMap h
(IsCyclotomicExtension.Rat.galEquivZMod
(n : ℕ) (rationalCyclotomicLevel n)
(σ.restrictNormal (rationalCyclotomicLevel n)))The product of the p-adic cyclotomic characters separates automorphisms of the actual rational cyclotomic field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicCharacterPrimeProduct_injective :
Function.Injective rationalCyclotomicCharacterPrimeProductThe canonical rational cyclotomic character is injective.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicCharacter_injective :
Function.Injective rationalCyclotomicCharacterThe canonical rational cyclotomic character is surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem rationalCyclotomicCharacter_surjective :
Function.Surjective rationalCyclotomicCharacterThe canonical topological equivalence Gal(ℚ(μ∞)/ℚ) ≃ ℤ̂ˣ.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def rationalCyclotomicCharacterContinuousMulEquiv :
(rationalCyclotomicField ≃ₐ[ℚ]
rationalCyclotomicField) ≃ₜ* ZHatˣEvaluating the actual profinite-unit cyclotomic character at a prime recovers the corresponding genuine p-adic cyclotomic character.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace KummerTheory
open ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem
zHatUnitsContinuousMulEquivPrimeProduct_rationalCyclotomicCharacter
(σ :
rationalCyclotomicField ≃ₐ[ℚ]
rationalCyclotomicField)
(p : Nat.Primes) :
zHatUnitsContinuousMulEquivPrimeProduct
(rationalCyclotomicCharacterContinuousMulEquiv σ) p =
rationalCyclotomicCharacterPrimeProduct σ p