ProCGroups.exists_continuous_character_extension_divisible
A continuous discrete character on a closed subgroup of a profinite abelian group extends continuously after mapping its values to a divisible group.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
open ProC
universe u v wLean source · statement
theorem exists_continuous_character_extension_divisible
{A : Type u} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
[CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
{B : Type v} [Group B] [TopologicalSpace B] [DiscreteTopology B]
{M : Type w} [CommGroup M] [TopologicalSpace M] [DivisibleBy (Additive M) ℤ]
(D : Subgroup A) (hD : IsClosed (D : Set A)) (χ : D →ₜ* B) (ι : B →* M) :
∃ η : A →ₜ* M, ∀ d : D, η d.1 = ι (χ d)