ClassFieldTower.Cohomology.exists_openNormalSubgroupInClass_factor_continuousMap_finite
Every continuous map from a pro-C group to a finite discrete space factors through one open-normal quotient in C.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
namespace ClassFieldTower.Cohomology
open ProCGroups ProCGroups.ProC ProCGroups.InverseSystems
universe u w
variable {C : FiniteGroupClass.{u}}
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]Lean source · statement
theorem exists_openNormalSubgroupInClass_factor_continuousMap_finite
[CompactSpace G] [T2Space G]
(hForm : FiniteGroupClass.Formation C)
(hG : HasOpenNormalBasisInClass C G)
{Y : Type w} [TopologicalSpace Y] [Finite Y] [DiscreteTopology Y]
(rho : G → Y) (hrho : Continuous rho) :
∃ U : OpenNormalSubgroupInClass C G,
∃ rhoU : (G ⧸ (U.1 : Subgroup G)) → Y,
Continuous rhoU ∧
rho = rhoU ∘ OpenNormalSubgroupInClass.quotientProj U