The explicit low-degree finite-quotient systems

For a topological group G acting on a discrete additive group M, the explicit cohomology groups in degrees zero, one, and two

Hⁱ(G ⧸ U, M^U),  i = 0, 1, 2,

form a directed system as the open normal subgroup U shrinks. If V ≤ U, its transition map is the compatible-pair pullback along the quotient homomorphism G ⧸ V → G ⧸ U and the coefficient inclusion M^U → M^V. When G is compact these discrete quotient groups are finite; the construction itself requires neither compactness nor continuity of the action of G on M.

TauCeti.finiteQuotientSystem already packages the corresponding system in Mathlib's discrete groupCohomology. The systems here are instead constructed directly with TauCeti.ContCohomology.explicitMap0, explicitMap1, and explicitMap2. In particular they are universe-polymorphic and do not transport their arrows through the universe-restricted comparison with discrete group cohomology. They are the source diagrams for the explicit finite-quotient colimit theorems in degrees zero, one, and two.

Main definitions

• TauCeti.ContCohomology.explicitFiniteQuotientTransition0: the transition H⁰(G ⧸ U, M^U) → H⁰(G ⧸ V, M^V) for V ≤ U.
• TauCeti.ContCohomology.explicitFiniteQuotientSystem0: the resulting functor on (OpenNormalSubgroup G)ᵒᵖ.
• TauCeti.ContCohomology.explicitFiniteQuotientTransition1: the transition H¹(G ⧸ U, M^U) → H¹(G ⧸ V, M^V) for V ≤ U.
• TauCeti.ContCohomology.explicitFiniteQuotientSystem1: the resulting functor on (OpenNormalSubgroup G)ᵒᵖ.
• TauCeti.ContCohomology.explicitFiniteQuotientTransition2 and explicitFiniteQuotientSystem2: the corresponding transition and functor in degree two.

Main statements

• explicitFiniteQuotientTransition0_eq_explicitMap0 identifies the degree-zero transition with compatible-pair pullback; its identity, composition, object, and arrow lemmas give the same characteristic API as the positive-degree systems.
• explicitFiniteQuotientTransition1_eq_explicitMap1 identifies a transition map with the compatible-pair pullback it is built from.
• explicitFiniteQuotientTransition1_id and explicitFiniteQuotientTransition1_comp are the identity and composition laws for the transition maps.
• explicitFiniteQuotientSystem1_obj and explicitFiniteQuotientSystem1_map identify the objects and arrows of the packaged functor.
• The corresponding declarations ending in 2 give the same characteristic API in degree two.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (1.2.5).
• L. Ribes and P. Zalesskii, Profinite Groups, Cor. 6.5.6(a).

Degree zero

def TauCeti.ContCohomology.explicitFiniteQuotientTransition0 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U V : OpenNormalSubgroup G) (hVU : V ≤ U) : ↥(H0 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) →+ ↥(H0 (G ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M))

The explicit degree-zero transition from the U-level to the V-level, for V ≤ U.

It is compatible-pair pullback along G ⧸ V → G ⧸ U and the inclusion M^U → M^V. On underlying coefficients it is just that inclusion.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.coe_explicitFiniteQuotientTransition0 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) (m : ↥(H0 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))) : ↑↑((explicitFiniteQuotientTransition0 G M U V hVU) m) = ↑↑m

A degree-zero finite-quotient transition does not change the underlying coefficient.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition0_eq_explicitMap0 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) : explicitFiniteQuotientTransition0 G M U V hVU = explicitMap0 (G ⧸ ↑U.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) (↑(continuousFiniteQuotientMap G hVU)) (fixedPointsInclusion hVU) ⋯

A degree-zero transition is the compatible-pair pullback along the quotient map and the inclusion of invariant coefficients.

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition0_id (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : explicitFiniteQuotientTransition0 G M U U ⋯ = AddMonoidHom.id ↥(H0 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The degree-zero transition from a level to itself is the identity.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition0_comp (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U V W : OpenNormalSubgroup G) (hVU : V ≤ U) (hWV : W ≤ V) : explicitFiniteQuotientTransition0 G M U W ⋯ = (explicitFiniteQuotientTransition0 G M V W hWV).comp (explicitFiniteQuotientTransition0 G M U V hVU)

For W ≤ V ≤ U, the degree-zero transition from the U-level to the W-level is the composite through the V-level.

Degree one

noncomputable def TauCeti.ContCohomology.explicitFiniteQuotientTransition1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U V : OpenNormalSubgroup G) (hVU : V ≤ U) : H1 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M) →+ H1 (G ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)

The explicit degree-one transition from the U-level to the V-level, for V ≤ U.

It is defined directly by compatible-pair functoriality from the quotient homomorphism G ⧸ V → G ⧸ U and the inclusion of invariant coefficients M^U → M^V.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition1_mk (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) (c : ↥(Z1 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))) : (explicitFiniteQuotientTransition1 G M U V hVU) ↑c = (H1pi (G ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) ((cocyclesMap1 (G ⧸ ↑U.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) (G ⧸ ↑V.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) (continuousFiniteQuotientMap G hVU) (fixedPointsInclusion hVU) ⋯ ⋯) c)

A degree-one finite-quotient transition sends the class of a cocycle to its compatible-pair pullback.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition1_eq_explicitMap1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) : explicitFiniteQuotientTransition1 G M U V hVU = explicitMap1 (G ⧸ ↑U.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) (G ⧸ ↑V.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) (continuousFiniteQuotientMap G hVU) (fixedPointsInclusion hVU) ⋯ ⋯

A degree-one finite-quotient transition is the compatible-pair pullback along the quotient homomorphism G ⧸ V → G ⧸ U and the inclusion of invariant coefficients M ^ U → M ^ V.

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition1_id (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : explicitFiniteQuotientTransition1 G M U U ⋯ = AddMonoidHom.id (H1 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The transition from an open normal subgroup to itself is the identity.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition1_comp (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U V W : OpenNormalSubgroup G) (hVU : V ≤ U) (hWV : W ≤ V) : explicitFiniteQuotientTransition1 G M U W ⋯ = (explicitFiniteQuotientTransition1 G M V W hWV).comp (explicitFiniteQuotientTransition1 G M U V hVU)

For W ≤ V ≤ U, the transition from the U-level to the W-level is the composite through the V-level.

Degree zero

def TauCeti.ContCohomology.explicitFiniteQuotientSystem0 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] : CategoryTheory.Functor (OpenNormalSubgroup G)ᵒᵖ AddCommGrpCat

The explicit degree-zero finite-quotient system. It sends an open normal subgroup U to H⁰(G ⧸ U, M^U) and an inclusion V ≤ U to compatible-pair pullback from the U-level to the V-level.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem0_obj (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : (explicitFiniteQuotientSystem0 G M).obj (Opposite.op U) = ↧↥(H0 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The object at U of the degree-zero finite-quotient system is H⁰(G ⧸ U, M^U).

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem0_map (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [DistribMulAction G M] {U V : (OpenNormalSubgroup G)ᵒᵖ} (f : U ⟶ V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((explicitFiniteQuotientSystem0 G M).map f) (CategoryTheory.eqToHom ⋯)) = AddCommGrpCat.ofHom (explicitFiniteQuotientTransition0 G M (Opposite.unop U) (Opposite.unop V) ⋯)

Every arrow of the degree-zero finite-quotient system is the direct compatible-pair transition.

Degree one

noncomputable def TauCeti.ContCohomology.explicitFiniteQuotientSystem1 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] : CategoryTheory.Functor (OpenNormalSubgroup G)ᵒᵖ AddCommGrpCat

The explicit degree-one finite-quotient system of a discrete module. It sends an open normal subgroup U to H¹(G ⧸ U, M^U) and an inclusion V ≤ U to the direct explicit transition from the U-level to the V-level.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem1_obj (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : (explicitFiniteQuotientSystem1 G M).obj (Opposite.op U) = ↧(H1 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The object at U of the explicit degree-one finite-quotient system is H¹(G ⧸ U, M^U).

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem1_map (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : (OpenNormalSubgroup G)ᵒᵖ} (f : U ⟶ V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((explicitFiniteQuotientSystem1 G M).map f) (CategoryTheory.eqToHom ⋯)) = AddCommGrpCat.ofHom (explicitFiniteQuotientTransition1 G M (Opposite.unop U) (Opposite.unop V) ⋯)

Under the object identifications above, every arrow of the explicit degree-one finite-quotient system is the direct transition built from explicitMap1.

Degree two

noncomputable def TauCeti.ContCohomology.explicitFiniteQuotientTransition2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U V : OpenNormalSubgroup G) (hVU : V ≤ U) : H2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M) →+ H2 (G ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)

The explicit degree-two transition from the U-level to the V-level, for V ≤ U.

It is defined directly by compatible-pair functoriality from the quotient homomorphism G ⧸ V → G ⧸ U and the inclusion of invariant coefficients M^U → M^V.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition2_mk (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) (c : ↥(Z2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))) : (explicitFiniteQuotientTransition2 G M U V hVU) ↑c = (H2pi (G ⧸ ↑V.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) ((cocyclesMap2 (G ⧸ ↑U.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) (G ⧸ ↑V.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) (continuousFiniteQuotientMap G hVU) (fixedPointsInclusion hVU) ⋯ ⋯) c)

A degree-two finite-quotient transition sends the class of a cocycle to its compatible-pair pullback.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition2_eq_explicitMap2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) : explicitFiniteQuotientTransition2 G M U V hVU = explicitMap2 (G ⧸ ↑U.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)) (G ⧸ ↑V.toOpenSubgroup) (↥(FixedPoints.addSubgroup (↥↑V.toOpenSubgroup) M)) (continuousFiniteQuotientMap G hVU) (fixedPointsInclusion hVU) ⋯ ⋯

A degree-two finite-quotient transition is the compatible-pair pullback along the quotient homomorphism G ⧸ V → G ⧸ U and the inclusion of invariant coefficients M^U → M^V.

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition2_id (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : explicitFiniteQuotientTransition2 G M U U ⋯ = AddMonoidHom.id (H2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The degree-two transition from an open normal subgroup to itself is the identity.

theorem TauCeti.ContCohomology.explicitFiniteQuotientTransition2_comp (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U V W : OpenNormalSubgroup G) (hVU : V ≤ U) (hWV : W ≤ V) : explicitFiniteQuotientTransition2 G M U W ⋯ = (explicitFiniteQuotientTransition2 G M V W hWV).comp (explicitFiniteQuotientTransition2 G M U V hVU)

For W ≤ V ≤ U, the degree-two transition from the U-level to the W-level is the composite through the V-level.

noncomputable def TauCeti.ContCohomology.explicitFiniteQuotientSystem2 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] : CategoryTheory.Functor (OpenNormalSubgroup G)ᵒᵖ AddCommGrpCat

The explicit degree-two finite-quotient system of a discrete module. It sends an open normal subgroup U to H²(G ⧸ U, M^U) and an inclusion V ≤ U to the direct explicit transition from the U-level to the V-level.

Equations

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

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem2_obj (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] (U : OpenNormalSubgroup G) : (explicitFiniteQuotientSystem2 G M).obj (Opposite.op U) = ↧(H2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))

The object at U of the explicit degree-two finite-quotient system is H²(G ⧸ U, M^U).

@[simp]

theorem TauCeti.ContCohomology.explicitFiniteQuotientSystem2_map (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type v) [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DiscreteTopology M] [DistribMulAction G M] {U V : (OpenNormalSubgroup G)ᵒᵖ} (f : U ⟶ V) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((explicitFiniteQuotientSystem2 G M).map f) (CategoryTheory.eqToHom ⋯)) = AddCommGrpCat.ofHom (explicitFiniteQuotientTransition2 G M (Opposite.unop U) (Opposite.unop V) ⋯)

Under the object identifications above, every arrow of the explicit degree-two finite-quotient system is the direct transition built from explicitMap2.