Descent of continuous functions to finite quotients #
A continuous function from a profinite group to a discrete module factors through a sufficiently deep finite quotient, with values in the fixed points at that level. The quotient may be chosen below any prescribed open normal subgroup.
Main statement #
TauCeti.ContCohomology.exists_openNormalSubgroup_descendContinuous: continuous functions descend to fixed-point-valued functions on sufficiently deep finite quotients.
theorem
TauCeti.ContCohomology.exists_openNormalSubgroup_descendContinuous
{G : Type u}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
{M : Type v}
[AddGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction G M]
[ContinuousSMul G M]
[CompactSpace G]
[TotallyDisconnectedSpace G]
(U : OpenNormalSubgroup G)
(b : G → M)
(hb : Continuous b)
:
∃ (V : OpenNormalSubgroup G) (_ : V ≤ U) (bV :
G ⧸ ↑V.toOpenSubgroup → ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)), Continuous bV ∧ ∀ (g : G), ↑(bV ↑g) = b g
A continuous function from a profinite group to a discrete module descends below any prescribed open normal subgroup to a continuous function on a finite quotient, with values fixed by that subgroup.