ProCGroups.exists_openNormal_character_extension
A continuous character on a closed normal subgroup extends to an open normal supergroup inside any prescribed open normal neighborhood of that subgroup. The extension is constructed through an actual finite quotient.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ProCGroups
open ProC
universe u vLean source · statement
theorem exists_openNormal_character_extension
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
{A : Type v} [Group A] [TopologicalSpace A] [DiscreteTopology A]
(D : Subgroup G) [D.Normal] (hD : IsClosed (D : Set G))
(χ : D →ₜ* A) (V₀ : OpenNormalSubgroup G) :
∃ U : OpenNormalSubgroup G, ∃ hDU : D ≤ (U : Subgroup G),
(U : Subgroup G) ≤ D ⊔ (V₀ : Subgroup G) ∧
∃ η : U →ₜ* A, ∀ d : D, η (Subgroup.inclusion hDU d) = χ d