Explicit and canonical continuous cocycles in degrees one and two

cocycleEquiv1 and cocycleEquiv2 identify continuous inhomogeneous cocycles with the cycles of Mathlib's homogeneous complex. Their forward formulas are g • c (g⁻¹ * h) and g • c (g⁻¹ * h, h⁻¹ * k); their inverses evaluate at (1, g) and (1, g, g * h). Each comparison identifies the explicit coboundaries with canonical boundaries, providing the cycle-level input to the comparison of cohomology classes. In degree zero every element of H⁰(G, M) = M^G is a cocycle already, and cocycle0 is its homogeneous form g ↦ g • m, a cycle of the homogeneous complex.

This is an additive equivalence, with no assertion about the pointwise topology on explicit cocycles. Degree one holds for every topological group, while degree two assumes local compactness because its inverse cochain comparison uses Mathlib's ContinuousMap.uncurry. Coefficients are discrete with a jointly continuous action.

The formulas follow Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, second edition, Chapter I §2. The passage from the concrete kernel to canonical cycles uses Mathlib's TopModuleCat.isLimitKer and HomologicalComplex.cyclesIsKernel.

Degree zero

noncomputable def TauCeti.ContCohomology.cocycle0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : ↥(H0 G M)) : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 0).toModuleCat

The homogeneous 0-cocycle of an invariant element: g ↦ g • m, which is the constant cochain m since m is invariant.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.sc_iCycles_cocycle0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : ↥(H0 G M)) : (TopModuleCat.Hom.hom (HomologicalComplex.sc (ofDiscreteModule ℤ G M).homogeneousCochains 0).iCycles) (cocycle0 G M m) = (cochainEquiv0 G M) ↑m

The inclusion of the homogeneous 0-cocycle cocycle0 m is the cochain g ↦ g • m, read through the short complex in degree zero as iCycles_cocycleEquiv1 and iCycles_cocycleEquiv2 do in degrees one and two.

theorem TauCeti.ContCohomology.iCycles_cocycle0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G M).homogeneousCochains 0)) (cocycle0 G M m) = (cochainEquiv0 G M) ↑m

The underlying homogeneous cochain of cocycle0 m is g ↦ g • m, stated on the inclusion of the homogeneous complex itself.

Degree one

noncomputable def TauCeti.ContCohomology.cocycleEquiv1 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : ↥(Z1 G M) ≃+ ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 1).toModuleCat

Continuous one-cocycles in inhomogeneous coordinates are the cycles of the canonical homogeneous cochain complex. The forward formula is g • c (g⁻¹ * h); the inverse evaluates at (1, g).

Unlike the degree-two comparison, this needs no local compactness: the degree-one cochain comparison is a plain currying, whose inverse is evaluation.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.iCycles_cocycleEquiv1 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(Z1 G M)) : (TopModuleCat.Hom.hom (HomologicalComplex.sc (ofDiscreteModule ℤ G M).homogeneousCochains 1).iCycles) ((cocycleEquiv1 G M) c) = (cochainEquiv1 G M) ⟨↑c, ⋯⟩

The inclusion of a compared one-cocycle is the existing cochain comparison.

@[simp]

theorem TauCeti.ContCohomology.cocycleEquiv1_symm_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 1).toModuleCat) (g : G) : ↑((cocycleEquiv1 G M).symm c) g = (↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G M).homogeneousCochains 1)) c) 1) g

The inverse one-cocycle comparison reads the canonical cocycle at (1, g).

theorem TauCeti.ContCohomology.cocycleEquiv1_d0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : M) : (cocycleEquiv1 G M) ⟨(d0 G M) m, ⋯⟩ = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (ofDiscreteModule ℤ G M).homogeneousCochains 0 1)) ((cochainEquiv0 G M) m)

The comparison sends the explicit coboundary of an element of M to its canonical boundary, with the same primitive under the degree-zero cochain comparison.

theorem TauCeti.ContCohomology.mem_B1_iff_cocycleEquiv1_mem_range (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(Z1 G M)) : ↑c ∈ B1 G M ↔ (cocycleEquiv1 G M) c ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (ofDiscreteModule ℤ G M).homogeneousCochains 0 1))

A continuous one-cocycle is an explicit coboundary exactly when its canonical image is a boundary.

theorem TauCeti.ContCohomology.cocycleEquiv1_naturality (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup 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) (c : ↥(Z1 G M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 1)) ((cocycleEquiv1 G M) c) = (cocycleEquiv1 H N) ((cocyclesMap1 G M H N φ f ⋯ hf) c)

The one-cocycle comparison is natural in compatible pairs of group and coefficient maps.

Degree two

noncomputable def TauCeti.ContCohomology.cocycleEquiv2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] : ↥(Z2 G M) ≃+ ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat

Continuous two-cocycles in inhomogeneous coordinates are the cycles of the canonical homogeneous cochain complex.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.iCycles_cocycleEquiv2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↥(Z2 G M)) : (TopModuleCat.Hom.hom (HomologicalComplex.sc (ofDiscreteModule ℤ G M).homogeneousCochains 2).iCycles) ((cocycleEquiv2 G M) c) = (cochainEquiv2 G M) ⟨↑c, ⋯⟩

The inclusion of a compared cocycle is the existing cochain comparison.

@[simp]

theorem TauCeti.ContCohomology.cocycleEquiv2_symm_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G M) 2).toModuleCat) (g h : G) : ↑((cocycleEquiv2 G M).symm c) (g, h) = ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G M).homogeneousCochains 2)) c) 1) g) (g * h)

The inverse cocycle comparison reads the canonical cocycle at (1, g, g * h).

theorem TauCeti.ContCohomology.cocycleEquiv2_d1 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↥(C1 G M)) : (cocycleEquiv2 G M) ⟨(d1 G M) ↑c, ⋯⟩ = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (ofDiscreteModule ℤ G M).homogeneousCochains 1 2)) ((cochainEquiv1 G M) c)

The comparison sends the explicit coboundary of a continuous one-cochain to its canonical boundary, with the same primitive under the degree-one cochain comparison.

theorem TauCeti.ContCohomology.mem_B2_iff_cocycleEquiv2_mem_range (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (c : ↥(Z2 G M)) : ↑c ∈ B2 G M ↔ (cocycleEquiv2 G M) c ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (HomologicalComplex.toCycles (ofDiscreteModule ℤ G M).homogeneousCochains 1 2))

A continuous two-cocycle is an explicit coboundary exactly when its canonical image is a boundary.

theorem TauCeti.ContCohomology.cocycleEquiv2_naturality (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] (H N : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [LocallyCompactSpace 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) (c : ↥(Z2 G M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.cocyclesMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 2)) ((cocycleEquiv2 G M) c) = (cocycleEquiv2 H N) ((cocyclesMap2 G M H N φ f ⋯ hf) c)

The two-cocycle comparison is natural in compatible pairs of group and coefficient maps.