Continuous cohomology of a discrete representation of a compact group

Mathlib builds continuous cohomology as the homology of the homogeneous cochain complex, whose terms are the invariants of the iterated coinduced representations C(G, C(G, …, X.V)). Over a compact group G and for a representation whose underlying module is discrete, every one of those function spaces is discrete in the compact-open topology, hence so is every term of the complex and every subquotient of it. So continuousCohomology n X is a discrete topological module.

This matters because the topology is part of the statement. The low-degree explicit model presents H¹ and H² as quotients of subgroups of G → M and G × G → M; those carry the pointwise topology, whose quotient is not discrete for an infinite profinite G (with trivial ZMod 2 coefficients on an infinite product of copies of ZMod 2, no finite set of evaluations isolates the zero character). A comparison between the explicit model and the canonical one must therefore say in which category it holds, and the results here are what make the canonical side of that comparison a discrete object.

When the action on X is moreover continuous, so that X is smooth discrete (TauCeti.IsSmoothDiscrete), every term of the resolution is smooth discrete as well (TauCeti.IsSmoothDiscrete.resolutionX), since coinduction from the trivial subgroup preserves smoothness over a compact group.

The predicate TauCeti.ContinuousCohomology.ResolutionVanishesOn X T n F records that a term F of the resolution C(G, C(G, …, X)) vanishes on all n-tuples of points of a subset T ⊆ G, and TauCeti.ContinuousCohomology.ResolutionVanishesOn.exists_isOpen shows that vanishing on a compact set already holds on an open neighbourhood of it. For an arbitrary compact set that is all one gets; when the compact set is a closed subgroup of a profinite G, the neighbourhood contains an open subgroup, so the vanishing holds on an open subgroup containing the closed one (TauCeti.ContinuousCohomology.exists_openSubgroup_le_resolutionMap_subgroupSubtype_eq_zero in ClosedSubgroup.lean). This is how cohomological statements about a closed subgroup descend to the open subgroups containing it.

This implements the "category of the comparison" milestone of Layer 3 of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md.

instance TauCeti.discreteTopology_resolutionX {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : DiscreteTopology ↑(X.resolutionX n)

Every term of the coinduced resolution of a discrete representation of a compact group is discrete: it is an iterated space of continuous maps out of the compact group G.

instance TauCeti.discreteTopology_homogeneousCochains {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : DiscreteTopology ↑(X.homogeneousCochains.X n).toModuleCat

Every term of the homogeneous cochain complex of a discrete representation of a compact group is discrete.

instance TauCeti.discreteTopology_cocycles {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : DiscreteTopology ↑(ContinuousCohomology.cocycles X n).toModuleCat

The continuous cocycles of a discrete representation of a compact group are discrete.

theorem TauCeti.IsSmoothDiscrete.coind₁ {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} (hX : IsSmoothDiscrete k X) : IsSmoothDiscrete k X.coind₁

Coinduction from the trivial subgroup preserves smoothness over a compact group: if X is a smooth discrete representation of the compact group G, so is X.coind₁ = C(G, X).

theorem TauCeti.IsSmoothDiscrete.resolutionX {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} (hX : IsSmoothDiscrete k X) (n : ℕ) : IsSmoothDiscrete k (X.resolutionX n)

The coinduced resolution of a smooth discrete representation of a compact group is smooth discrete in every degree.

Vanishing on a subset

ResolutionVanishesOn X T n F says that the iterated map F : C(G, C(G, …, X)) of degree n vanishes on all n-tuples of points of T. For a subgroup S it is the vanishing of the restriction of F to S.

def TauCeti.ContinuousCohomology.ResolutionVanishesOn {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (T : Set G) (n : ℕ) : ↑(X.resolutionX n) → Prop

An element F of the n-th term C(G, C(G, …, X)) of the coinduced resolution vanishes on T when it is zero on every n-tuple of points of T.

Equations

• TauCeti.ContinuousCohomology.ResolutionVanishesOn X T 0 v = (v = 0)
• TauCeti.ContinuousCohomology.ResolutionVanishesOn X T n.succ F = ∀ g ∈ T, TauCeti.ContinuousCohomology.ResolutionVanishesOn X T n (F g)

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionVanishesOn_zero {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (T : Set G) (v : ↑(X.resolutionX 0)) : ResolutionVanishesOn X T 0 v ↔ v = 0

@[simp]

theorem TauCeti.ContinuousCohomology.resolutionVanishesOn_succ {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (T : Set G) (n : ℕ) (F : ↑(X.resolutionX (n + 1))) : ResolutionVanishesOn X T (n + 1) F ↔ ∀ g ∈ T, ResolutionVanishesOn X T n (F g)

theorem TauCeti.ContinuousCohomology.ResolutionVanishesOn.mono {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {T T' : Set G} (h : T' ⊆ T) (n : ℕ) {F : ↑(X.resolutionX n)} : ResolutionVanishesOn X T n F → ResolutionVanishesOn X T' n F

Vanishing on a set implies vanishing on every subset.

theorem TauCeti.ContinuousCohomology.ResolutionVanishesOn.exists_isOpen {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {X : TopRep k G} [DiscreteTopology ↑X] {T : Set G} (hT : IsCompact T) (n : ℕ) {F : ↑(X.resolutionX n)} : ResolutionVanishesOn X T n F → ∃ (W : Set G), IsOpen W ∧ T ⊆ W ∧ ResolutionVanishesOn X W n F

Vanishing on a compact set spreads to an open neighbourhood. An element of the coinduced resolution of a discrete representation of a compact group that vanishes on a compact set T vanishes on an open set containing T.

instance TauCeti.discreteTopology_continuousCohomology {k : Type u_1} {G : Type u_2} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : DiscreteTopology ↑(continuousCohomology n X).toModuleCat

The continuous cohomology of a discrete representation of a compact group is discrete.

This is the statement that lets a comparison with an explicit low-degree model be phrased as an isomorphism in TopModuleCat k between discrete objects rather than as an additive isomorphism after forgetting the topology.