Naturality of the degree-two comparison

The isomorphism between explicit H² and Mathlib's continuous cohomology is natural for compatible pairs. In particular, it transports restriction to a subgroup and maps of discrete coefficient modules. These squares let calculations on continuous two-cocycles be read as statements about the canonical cohomology object, as in the restriction formula for the index-two Evens graph class.

The additive comparison and its compatible-pair naturality are in CohomologyComparison.lean. Here the equations are stated on the discrete carriers of the explicit groups and the TopModuleCat ℤ isomorphisms. For restriction the subgroup has to be compact, so the degree-two comparison exists on both sides. Read through the comparison, the triviality of inner conjugation on canonical cohomology, TauCeti.ContinuousCohomology.map_eq_id_of_inner, becomes the triviality of inner conjugation on explicit H² (explicitMap2_eq_self_of_inner).

The identification of inhomogeneous and homogeneous continuous cohomology follows J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2.

@[simp]

theorem TauCeti.ContCohomology.explicitIso_map2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [ContinuousSMul H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (x : DiscreteH2 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 2)) ((CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology H N).hom) ((discreteH2Equiv H N).symm ((explicitMap2 G M H N φ f ⋯ hf) ((discreteH2Equiv G M) x)))

The degree-two comparison in TopModuleCat ℤ commutes with pullback along a compatible pair of a continuous group homomorphism and an equivariant coefficient map.

@[simp]

theorem TauCeti.ContCohomology.explicitIso_res2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (S : Subgroup G) [CompactSpace ↥S] (x : DiscreteH2 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S (ofDiscreteModule ℤ G M) 2)) ((CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology (↥S) M).hom) ((discreteH2Equiv (↥S) M).symm ((explicitRes2 G M S) ((discreteH2Equiv G M) x)))

The degree-two comparison transports explicit restriction to canonical restriction.

@[simp]

theorem TauCeti.ContCohomology.explicitIso_coeffMap2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [ContinuousSMul G N] (f : M →+[G] N) (x : DiscreteH2 G M) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 2)) ((CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH2IsoContinuousCohomology G N).hom) ((discreteH2Equiv G N).symm ((explicitCoeff2 G M f ⋯) ((discreteH2Equiv G M) x)))

The degree-two comparison transports a continuous equivariant coefficient map to the canonical map induced by the same homomorphism.

theorem TauCeti.ContCohomology.explicitMap2_eq_self_of_inner (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (g : G) (φ : G →ₜ* G) (hφ : ∀ (x : G), φ x = g⁻¹ * x * g) (f : M →+ M) (hf : ∀ (m : M), f m = g • m) (hfc : Continuous ⇑f) (hequiv : ∀ (h : G) (m : M), f (φ h • m) = h • f m) (x : H2 G M) : (explicitMap2 G M G M φ f hfc hequiv) x = x

Inner automorphisms act trivially on explicit H². For g : G, pullback along the compatible pair of the inner automorphism x ↦ g⁻¹ * x * g and the action of g on the coefficients is the identity of H²(G, M). This is TauCeti.ContinuousCohomology.map_eq_id_of_inner, read through the degree-two comparison.