Invariant coefficients for continuous cohomology

For a normal subgroup H of G acting distributively on an additive group M, the invariants M ^ H carry a distributive action of G ⧸ H. Over a profinite G with H open normal, these are the coefficients of the finite-quotient system computing continuous cohomology. Shrinking H enlarges M ^ H along transition inclusions. For arbitrary normal H, the quotient action also supplies the coefficients of inflation.

The invariant subgroup is Mathlib's FixedPoints.addSubgroup H M. Its algebraic actions, inclusions and pairings are supplied by TauCeti/GroupTheory/GroupAction/FixedPoints.lean, and their topology by TauCeti/Topology/Algebra/GroupAction/FixedPoints.lean. This file provides the compatibility with the continuous finite-quotient maps and the discrete-module dictionary.

Main results

• TauCeti.ContCohomology.fixedPointsInclusion_continuousFiniteQuotientMap_smul: for open normal subgroups V ≤ U, the inclusion M^U → M^V is equivariant along the continuous quotient map G ⧸ V → G ⧸ U. This holds for additive monoids with distributive action.
• TauCeti.ofDiscreteModuleQuotient: the coefficient dictionary identifies the explicit fixed-point module with TopRep.quotientToInvariants, preserving the underlying coefficients.

@[simp]

theorem TauCeti.ContCohomology.fixedPointsInclusion_continuousFiniteQuotientMap_smul (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u_2) [AddMonoid M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) (q : G ⧸ ↑V.toOpenSubgroup) (m : ↥(FixedPoints.addSubmonoid (↥↑U.toOpenSubgroup) M)) : (fixedPointsInclusion hVU) ((continuousFiniteQuotientMap G hVU) q • m) = q • (fixedPointsInclusion hVU) m

The coefficient inclusion M^U → M^V is equivariant after restriction along the quotient homomorphism G ⧸ V → G ⧸ U.

def TauCeti.ofDiscreteModuleQuotient (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (H : Subgroup G) [H.Normal] : ofDiscreteModule ℤ (G ⧸ H) ↥(FixedPoints.addSubgroup (↥H) M) ⟶ (ofDiscreteModule ℤ G M).quotientToInvariants H

The coefficient dictionary commutes with quotient invariants. The explicit fixed-point module M^H, regarded as a discrete module over G ⧸ H, maps canonically to the invariants of the restricted canonical object. Its underlying function preserves the coefficient in M; only the two equivalent proofs of invariance differ.

This is the coefficient morphism used to compare explicit and canonical inflation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ofDiscreteModuleQuotient_apply (G : Type u_1) [Group G] (M : Type u_2) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] (H : Subgroup G) [H.Normal] (m : ↥(FixedPoints.addSubgroup (↥H) M)) : ↑((CategoryTheory.ConcreteCategory.hom (ofDiscreteModuleQuotient G M H)) m) = ↑m

The quotient-invariants dictionary morphism preserves the underlying coefficient.