If every finite reduction had order prime to p, each reduction would have exponent dividing p - 1. Separation by reductions would then place the entire image in the finite group of (p - 1)-st roots of unity.
Continuous reduction of p-adic units at a positive finite level.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable {p : ℕ} [Fact p.Prime]def unitsReduction (n : ℕ) :
(PadicInt p)ˣ →ₜ* (ZMod (p ^ (n + 1)))ˣAn infinite unit image has a finite reduction whose order is divisible by p.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable {p : ℕ} [Fact p.Prime]
variable {G : Type*} [Group G] [TopologicalSpace G]theorem exists_prime_dvd_card_reduction_range
(χ : G →ₜ* (PadicInt p)ˣ) (hinf : Set.Infinite (Set.range χ)) :
∃ n : ℕ, p ∣ Nat.card ((unitsReduction n).comp χ).toMonoidHom.rangeAn infinite p-adic unit image yields an actual continuous cyclic quotient of order p.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace PadicInt
variable {p : ℕ} [Fact p.Prime]
variable {G : Type*} [Group G] [TopologicalSpace G]theorem exists_surjective_prime_character_of_infinite_unit_image
(χ : G →ₜ* (PadicInt p)ˣ) (hinf : Set.Infinite (Set.range χ)) :
∃ ψ : G →ₜ* Multiplicative (ZMod p), Function.Surjective ψ