The explicit model against the canonical object, in degree zero

The explicit low-degree complex presents H⁰(G, M) as the invariant subgroup M^G of a discrete G-module, while the canonical object is Mathlib's continuousCohomology 0 X for X a topological representation. This file identifies the two in degree zero, for X the image TauCeti.ofDiscreteModule ℤ G M of M under the coefficient dictionary, and transports the operations that exist in that degree across the identification.

The comparison is an isomorphism in TopModuleCat ℤ, not merely an additive one: H⁰(G, M) is a subgroup of the discrete M, so it is discrete already and needs no separate discrete synonym, and Mathlib's ContinuousCohomology.zeroIso exhibits the canonical carrier as homeomorphic to the invariant subspace of the same module. The identity on underlying elements of M is therefore already an isomorphism of topological ℤ-modules between H⁰(G, M) and those invariants, which is TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants; composing it with the inverse of zeroIso gives TauCeti.ContCohomology.explicitH0IsoContinuousCohomology, whose value at an invariant m is the degree-zero cohomology class of m in the sense of TauCeti.ContinuousCohomology.degreeZeroClass.

Degree zero needs no hypothesis beyond the ones that make the two sides exist. In particular it needs neither profiniteness of G nor continuity of the action G × M → M: a 0-cochain is a single element of M, so no continuity condition constrains it, and ContinuousCohomology.zeroIso holds for every object of TopRep ℤ G. The comparison is nevertheless stated only for objects in the image of TauCeti.ofDiscreteModule, as Layer 3 of the roadmap requires: a general object of TopRep ℤ G need not be discrete, and the explicit complex is not a description of its cohomology.

Main definitions

• TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants: the explicit H⁰(G, M) = M^G is the invariant submodule of TauCeti.ofDiscreteModule ℤ G M, as an isomorphism of topological ℤ-modules.
• TauCeti.ContCohomology.explicitH0IsoContinuousCohomology: the comparison H⁰(G, M) ≅ continuousCohomology 0 (ofDiscreteModule ℤ G M) in TopModuleCat ℤ.

Main results

• TauCeti.ContCohomology.explicitH0IsoContinuousCohomology_hom_eq_π: the comparison sends an invariant element m to the class of its homogeneous 0-cocycle TauCeti.ContCohomology.cocycle0 m, which is how the cocycle-level comparisons of the higher degrees read it.
• TauCeti.ContCohomology.finite_continuousCohomology_zero: H⁰(G, M) is finite for a finite discrete M.
• TauCeti.ContCohomology.explicitH0Iso_map: the comparison is natural in compatible pairs.
• TauCeti.ContCohomology.explicitH0Iso_res, TauCeti.ContCohomology.explicitH0Iso_coeffMap: its two named instances, carrying the explicit restriction and coefficient maps of degree zero to the canonical ones. The restriction square is typed by TauCeti.res_ofDiscreteModule, which identifies the restriction of a canonical object with the canonical object of the restriction.
• TauCeti.coeffMap_zero_injective: the coefficient map of an injective equivariant map is injective on H⁰.

Roadmap

This implements the degree-zero part of the "comparison isomorphisms" milestone of Layer 3 of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, whose Suggested.lean fixes the name explicitH0IsoContinuousCohomology, together with the degree-zero rows of the transport table in its §2. The names of the three transports carry the degree explicitly, because Suggested.lean pins the unsuffixed explicitIso_map, explicitIso_res and explicitIso_coeffMap to degree one. Degrees one and two of the comparison need the passage between the canonical homogeneous cochains C(G, C(G, …)) and functions on Gⁿ, hence the compact-open exponential law and profiniteness of G, and are not in this file.

The sibling file GroupCohomologyIso.lean compares the same explicit model with Mathlib's discrete groupCohomology; this file compares it with the continuous carrier, which is the canonical object the roadmap fixes.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the identification of the inhomogeneous description of continuous cohomology, which the explicit model here follows, with the homogeneous one computing the canonical object. The isomorphism built in this file is the degree-zero case of that identification.

The carriers are the invariants of a single element, so they need no inverses in G and no topology on it.

theorem TauCeti.ContCohomology.mem_invariants_ofDiscreteModule_iff_mem_H0 (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (m : M) : m ∈ (ofDiscreteModule ℤ G M).ρ.invariants ↔ m ∈ H0 G M

An element of a discrete G-module is invariant for the canonical object it names exactly when it lies in the explicit H⁰(G, M) = M^G.

def TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] : ↥(H0 G M) ≃L[ℤ] ↥(ofDiscreteModule ℤ G M).ρ.invariants

Degree zero, on the carriers. The explicit H⁰(G, M) = M^G is the invariant submodule of the canonical object TauCeti.ofDiscreteModule ℤ G M, by the identity on underlying elements. Both carry the subspace topology of the discrete M, so the identification is a homeomorphism as well as an isomorphism of ℤ-modules.

Equations

• TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants G M = (TauCeti.ContCohomology.H0 G M).continuousLinearEquivInvariants (TauCeti.ofDiscreteModule ℤ G M).ρ ⋯

@[simp]

theorem TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants_val (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (m : ↥(H0 G M)) : ↑((H0ContinuousLinearEquivInvariants G M) m) = ↑m

H0ContinuousLinearEquivInvariants is the identity on underlying elements.

@[simp]

theorem TauCeti.ContCohomology.H0ContinuousLinearEquivInvariants_symm_val (G : Type u) [Monoid G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (m : ↥(ofDiscreteModule ℤ G M).ρ.invariants) : ↑((H0ContinuousLinearEquivInvariants G M).symm m) = ↑m

The inverse of H0ContinuousLinearEquivInvariants is the identity on underlying elements.

noncomputable def TauCeti.ContCohomology.explicitH0IsoContinuousCohomology (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] : ↧↥(H0 G M) ≅ continuousCohomology 0 (ofDiscreteModule ℤ G M)

Layer 3, degree zero against the canonical object. The explicit H⁰(G, M) is Mathlib's continuousCohomology 0 of the canonical object attached to M, as an isomorphism in TopModuleCat ℤ.

Unlike the comparisons in degrees one and two this needs no profiniteness: it is ContinuousCohomology.zeroIso, which holds over an arbitrary topological group, composed with the identification of the invariants above.

Equations

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

theorem TauCeti.ContCohomology.explicitH0IsoContinuousCohomology_hom_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (m : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) m = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso (ofDiscreteModule ℤ G M)).inv) ((H0ContinuousLinearEquivInvariants G M) m)

The defining formula of the comparison: it is the inverse of ContinuousCohomology.zeroIso applied to the invariant element itself.

theorem TauCeti.ContCohomology.explicitH0IsoContinuousCohomology_hom_eq_degreeZeroClass (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (m : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) m = ContinuousCohomology.degreeZeroClass (ofDiscreteModule ℤ G M) ↑m ⋯

The comparison sends an invariant element to its degree-zero class, in the sense of TauCeti.ContinuousCohomology.degreeZeroClass.

@[simp]

theorem TauCeti.ContCohomology.coe_explicitH0IsoContinuousCohomology_inv_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (y : ↑(continuousCohomology 0 (ofDiscreteModule ℤ G M)).toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).inv) y) = ↑((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso (ofDiscreteModule ℤ G M)).hom) y)

The inverse of the comparison reads off the invariant element that ContinuousCohomology.zeroIso assigns to a degree-zero class.

theorem TauCeti.ContCohomology.finite_continuousCohomology_zero {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] [Finite M] : Finite ↑(continuousCohomology 0 (ofDiscreteModule ℤ G M)).toModuleCat

H⁰ of a finite discrete module is finite: it is the subgroup of invariants.

Reading the comparison on the homogeneous complex needs the homogeneous 0-cocycle TauCeti.ContCohomology.cocycle0, hence the smoothness hypothesis ContinuousSMul G M that the cocycle comparisons carry.

theorem TauCeti.ContCohomology.explicitH0IsoContinuousCohomology_hom_eq_π (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [ContinuousSMul G M] (m : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) m = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (ofDiscreteModule ℤ G M) 0)) (cocycle0 G M m)

The degree-zero comparison sends an invariant element to the class of its homogeneous 0-cocycle.

theorem TauCeti.ContCohomology.explicitH0Iso_map (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DiscreteTopology N] [DistribMulAction H N] (φ : H →ₜ* G) (f : M →+ N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (x : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.map φ (ofDiscreteModulePair (↑φ) f.toIntLinearMap ⋯) 0)) ((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology H N).hom) ((explicitMap0 G M (↑φ) f hf) x)

Layer 3, transport of the compatible-pair pullback in degree zero. The comparison carries the explicit pullback TauCeti.ContCohomology.explicitMap0 along a compatible pair to Mathlib's ContinuousCohomology.map along the same pair. The two transports below are its instances at the inclusion of a subgroup and at the identity of the group.

theorem TauCeti.ContCohomology.explicitH0Iso_res (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (S : Subgroup G) (x : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.res S (ofDiscreteModule ℤ G M) 0)) ((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology (↥S) M).hom) ((explicitRes0 G M S) x)

Layer 3, transport of restriction in degree zero. The comparison carries the explicit inclusion M^G ⊆ M^S to the canonical restriction. The two sides land in the same object because TauCeti.res_ofDiscreteModule identifies the restriction of the canonical object of M with the canonical object of M over the subgroup.

theorem TauCeti.ContCohomology.explicitH0Iso_coeffMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (N : Type u) [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DiscreteTopology N] [DistribMulAction G N] (f : M →+[G] N) (x : ↥(H0 G M)) : (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 0)) ((CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G M).hom) x) = (CategoryTheory.ConcreteCategory.hom (explicitH0IsoContinuousCohomology G N).hom) ((explicitCoeff0 G M f) x)

Layer 3, transport of coefficient maps in degree zero. The comparison carries the explicit coefficient map to the canonical one attached to the same equivariant homomorphism; the canonical coefficient morphism is the compatible pair at the identity, by TauCeti.ofDiscreteModulePair_id.

theorem TauCeti.exists_coeffMap_ker_nsmul_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type u) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] {k : ℕ} (hK : ∀ (g : G), ∀ m ∈ (nsmulAddMonoidHom k).ker, g • m ∈ (nsmulAddMonoidHom k).ker) {x : ↑(continuousCohomology 0 (ofDiscreteModule ℤ G M)).toModuleCat} (hx : k • x = 0) : ∃ (z : ↑(continuousCohomology 0 (ofDiscreteModule ℤ G ↥(nsmulAddMonoidHom k).ker)).toModuleCat), (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap (nsmulAddMonoidHom k).ker.subtype.toIntLinearMap ⋯) 0)) z = x

In degree zero, a class of H⁰(G, M) killed by k is the image of a class of H⁰(G, M[k]), where M[k] is the G-submodule killed by k.

theorem TauCeti.coeffMap_zero_injective {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M N : Type u} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] (f : M →+[G] N) (hf : Function.Injective ⇑f) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.coeffMap (ofDiscreteModuleMap f.toAddMonoidHom.toIntLinearMap ⋯) 0))

Degree-zero cohomology is left exact: the coefficient map of an injective equivariant map is injective on H⁰, which is the invariants (TauCeti.ContCohomology.explicitH0Iso_coeffMap).