The zero locus of a continuous 1-cocycle

For a 1-cocycle f : G → M in the sense of Mathlib's unbundled groupCohomology.IsCocycle₁, groupCohomology.zeroLocus is the subgroup {g | f g = 0} of G. This file records its topological properties:

• groupCohomology.isClosed_zeroLocus: the zero locus of a continuous 1-cocycle with values in a T1 space is closed.
• groupCohomology.eq_zero_of_eqOn_zero_of_topologicalClosure_closure_eq_top: a continuous 1-cocycle with values in a T1 space that vanishes on a set whose generated subgroup is dense vanishes everywhere.
• TauCeti.continuous_groupNormHom: the norm of a finite normal subgroup is continuous when the ambient group acts by continuous maps.

theorem groupCohomology.isClosed_zeroLocus {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [T1Space M] {f : G → M} (hf : IsCocycle₁ f) (hc : Continuous f) : IsClosed ↑(zeroLocus hf)

The zero locus of a continuous 1-cocycle with values in a T1 space is closed.

theorem groupCohomology.eq_zero_of_eqOn_zero_of_topologicalClosure_closure_eq_top {G : Type u_1} {M : Type u_2} [Group G] [AddCommGroup M] [MulAction G M] [TopologicalSpace G] [TopologicalSpace M] [T1Space M] [IsTopologicalGroup G] {f : G → M} (hf : IsCocycle₁ f) (hc : Continuous f) {s : Set G} (hs : (Subgroup.closure s).topologicalClosure = ⊤) (h : Set.EqOn f 0 s) : f = 0

A continuous 1-cocycle vanishing on a topological generating set vanishes. A continuous 1-cocycle with values in a T1 space that vanishes on a set s whose generated subgroup is dense vanishes everywhere.

theorem TauCeti.continuous_groupNormHom {G : Type u_1} [Group G] (N : Subgroup G) [N.Normal] [Fintype ↥N] (M : Type u_2) [AddCommMonoid M] [DistribMulAction G M] [TopologicalSpace M] [ContinuousAdd M] [ContinuousConstSMul G M] : Continuous ⇑(groupNormHom N M)

The norm of a finite normal subgroup N of G is continuous on a module on which every element of G acts continuously.