Inhomogeneous coordinates on continuous homogeneous cochains

As additive groups, the first three terms of Mathlib's homogeneous cochain complex are identified with M, C1 G M, and C2 G M. The forward maps are the classical formulas g₀ • m, g₀ • c (g₀⁻¹ * g₁), and g₀ • c (g₀⁻¹ * g₁, g₁⁻¹ * g₂); the inverse maps evaluate at 1, at (1, g), and at (1, g, g * h). The differential compatibilities identify the canonical differentials with d0, d1, and d2, including the cocycle conditions in degrees one and two. All three comparisons are natural in compatible pairs of group and coefficient maps. These are additive equivalences; no identification of the pointwise and compact-open topologies is asserted.

Degrees zero and one need no local compactness. The degree-two inverse uses ContinuousMap.uncurry, so the group is locally compact. In particular the construction applies to profinite groups. Coefficients are discrete modules with a jointly continuous action; the canonical complex is always the one attached to ofDiscreteModule ℤ G M.

The formulas follow Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, 2nd ed., Chapter I §2. The pointwise homogeneous formulas are reused from Homogeneous.lean; Mathlib's TopRep.homogeneousCochains supplies the actual complex. Its terms are written as the invariant submodules of the iterated coinduced representation, the normal form needed by the simplifier for the application lemmas.

def TauCeti.ContCohomology.cochainEquiv0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : M ≃+ ↥(ofDiscreteModule ℤ G M).ρ.coind₁.invariants

Degree-zero inhomogeneous cochains as canonical homogeneous cochains.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv0_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : M) (g : G) : ↑((cochainEquiv0 G M) m) g = g • m

cochainEquiv0 sends m ∈ M to the homogeneous 0-cochain g ↦ g • m.

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv0_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 : ↥(ofDiscreteModule ℤ G M).ρ.coind₁.invariants) : (cochainEquiv0 G M).symm c = ↑c 1

The inverse of cochainEquiv0 evaluates a homogeneous 0-cochain at 1.

def TauCeti.ContCohomology.cochainEquiv1 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] : ↥(C1 G M) ≃+ ↥(ofDiscreteModule ℤ G M).ρ.coind₁.coind₁.invariants

Continuous one-cochains as canonical homogeneous cochains, by currying their homogeneous form.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv1_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(C1 G M)) (g h : G) : (↑((cochainEquiv1 G M) c) g) h = homogeneous1 (↑c) g h

cochainEquiv1 sends a continuous 1-cochain c to its homogeneous form (g, h) ↦ homogeneous1 c g h, curried.

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv1_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 : ↥(ofDiscreteModule ℤ G M).ρ.coind₁.coind₁.invariants) (g : G) : ↑((cochainEquiv1 G M).symm c) g = (↑c 1) g

The inverse of cochainEquiv1 sends a homogeneous cochain c to the 1-cochain g ↦ c 1 g.

theorem TauCeti.ContCohomology.d_cochainEquiv0 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : M) : (TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 0 1)) ((cochainEquiv0 G M) m) = (cochainEquiv1 G M) ⟨(d0 G M) m, ⋯⟩

The degree-zero comparison carries d0 to Mathlib's homogeneous differential.

theorem TauCeti.ContCohomology.cochainEquiv1_symm_d (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(ofDiscreteModule ℤ G M).ρ.coind₁.invariants) : (cochainEquiv1 G M).symm ((TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 0 1)) c) = ⟨(d0 G M) ((cochainEquiv0 G M).symm c), ⋯⟩

The inverse degree-one comparison carries the canonical differential to d0.

theorem TauCeti.ContCohomology.d_cochainEquiv1_apply (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(C1 G M)) (g h k : G) : ((↑((TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 1 2)) ((cochainEquiv1 G M) c)) g) h) k = g • (d1 G M) ↑c (g⁻¹ * h, h⁻¹ * k)

The differential of the degree-one comparison is the homogeneous form of d1.

theorem TauCeti.ContCohomology.d_cochainEquiv1_eq_zero_iff (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (c : ↥(C1 G M)) : (TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 1 2)) ((cochainEquiv1 G M) c) = 0 ↔ ↑c ∈ Z1 G M

The degree-one comparison detects precisely the continuous inhomogeneous cocycles.

def TauCeti.ContCohomology.cochainEquiv2 (G M : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] [LocallyCompactSpace G] : ↥(C2 G M) ≃+ ↥(ofDiscreteModule ℤ G M).ρ.coind₁.coind₁.coind₁.invariants

Continuous two-cochains as canonical homogeneous cochains. Local compactness supplies uncurrying for the inverse.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv2_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 : ↥(C2 G M)) (g h k : G) : ((↑((cochainEquiv2 G M) c) g) h) k = homogeneous2 (↑c) g h k

cochainEquiv2 sends a continuous 2-cochain c to its homogeneous form (g, h, k) ↦ homogeneous2 c g h k, curried.

@[simp]

theorem TauCeti.ContCohomology.cochainEquiv2_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 : ↥(ofDiscreteModule ℤ G M).ρ.coind₁.coind₁.coind₁.invariants) (g h : G) : ↑((cochainEquiv2 G M).symm c) (g, h) = ((↑c 1) g) (g * h)

The inverse of cochainEquiv2 sends a homogeneous cochain c to the 2-cochain (g, h) ↦ c 1 g (g * h).

theorem TauCeti.ContCohomology.d_cochainEquiv1 (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)) : (TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 1 2)) ((cochainEquiv1 G M) c) = (cochainEquiv2 G M) ⟨(d1 G M) ↑c, ⋯⟩

The degree-one comparison carries d1 to Mathlib's homogeneous differential.

theorem TauCeti.ContCohomology.cochainEquiv2_symm_d (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 : ↥(ofDiscreteModule ℤ G M).ρ.coind₁.coind₁.invariants) : (cochainEquiv2 G M).symm ((TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 1 2)) c) = ⟨(d1 G M) ↑((cochainEquiv1 G M).symm c), ⋯⟩

The inverse degree-two comparison carries the canonical differential to d1.

theorem TauCeti.ContCohomology.d_cochainEquiv2_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 : ↥(C2 G M)) (g h k l : G) : (((↑((TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 2 3)) ((cochainEquiv2 G M) c)) g) h) k) l = g • (d2 G M) ↑c (g⁻¹ * h, h⁻¹ * k, k⁻¹ * l)

The differential of the degree-two comparison is the homogeneous form of d2.

theorem TauCeti.ContCohomology.d_cochainEquiv2_eq_zero_iff (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 : ↥(C2 G M)) : (TopModuleCat.Hom.hom ((ofDiscreteModule ℤ G M).homogeneousCochains.d 2 3)) ((cochainEquiv2 G M) c) = 0 ↔ ↑c ∈ Z2 G M

The degree-two comparison detects precisely the continuous inhomogeneous cocycles.

theorem TauCeti.ContCohomology.cochainEquiv0_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) (m : M) : (TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯)).f 0)) ((cochainEquiv0 G M) m) = (cochainEquiv0 H N) (f m)

The degree-zero cochain comparison is natural in compatible pairs.

theorem TauCeti.ContCohomology.cochainEquiv1_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 : ↥(C1 G M)) : (TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯)).f 1)) ((cochainEquiv1 G M) c) = (cochainEquiv1 H N) ⟨(cochainsMap1 (↑φ) f) ↑c, ⋯⟩

The degree-one cochain comparison is natural in compatible pairs.

theorem TauCeti.ContCohomology.cochainEquiv2_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] [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) [LocallyCompactSpace H] (c : ↥(C2 G M)) : (TopModuleCat.Hom.hom ((ContinuousCohomology.cochainsMap φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯)).f 2)) ((cochainEquiv2 G M) c) = (cochainEquiv2 H N) ⟨(cochainsMap2 (↑φ) f) ↑c, ⋯⟩

The degree-two cochain comparison is natural in compatible pairs.