Euler's theorem gives compatible finite powers of (p + 1) ^ (p - 1). Their inverse limit is a continuous character of the additive p-adic integers, with infinite image and trivial reduction modulo p.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]def principalUnitResidue (n : ℕ) : (ZMod (p ^ n))ˣSurrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]theorem principalUnitResidue_pow (n : ℕ) :
principalUnitResidue p n ^ (p ^ n) = 1Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]def principalUnitPowerResidue (n : ℕ) :
ZMod (p ^ n) →+ Additive (ZMod (p ^ n))ˣSurrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]theorem principalUnitPowerResidue_intCast (n : ℕ) (a : ℤ) :
(principalUnitPowerResidue p n (a : ZMod (p ^ n))).toMul =
principalUnitResidue p n ^ aSurrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]theorem principalUnitPowerResidue_compatible (n : ℕ)
(a : ZMod (p ^ (n + 1))) :
Units.map (ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n))).toMonoidHom
(principalUnitPowerResidue p (n + 1) a).toMul =
(principalUnitPowerResidue p n
(ZMod.castHom (pow_dvd_pow p (Nat.le_succ n)) (ZMod (p ^ n)) a)).toMulThe powers of (p + 1) ^ (p - 1) extend continuously to p-adic exponents.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]theorem exists_continuous_principal_unit_powers :
∃ φ : Multiplicative (PadicInt p) →ₜ* (PadicInt p)ˣ,
((φ (Multiplicative.ofAdd 1) : (PadicInt p)ˣ) : PadicInt p) =
((p + 1 : ℕ) : PadicInt p) ^ (p - 1) ∧
∀ x, toZModPow 1 (φ x : PadicInt p) = 1The additive p-adic integers admit a continuous infinite principal-unit character.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable (p : ℕ) [Fact p.Prime]theorem exists_infinite_principal_unit_character :
∃ φ : Multiplicative (PadicInt p) →ₜ* (PadicInt p)ˣ,
Set.Infinite (Set.range φ) ∧ ∀ x, toZModPow 1 (φ x : PadicInt p) = 1