The finite-quotient system of a group cohomology tower

For a normal subgroup U of a group G and a G-representation A, Mathlib's Rep.quotientToInvariants makes the invariants A^U a representation of G ⧸ U, so that Hⁿ(G ⧸ U, A^U) is defined. As U shrinks these groups form a directed system: for V ≤ U the quotient homomorphism G ⧸ V →* G ⧸ U and the coefficient inclusion A^U ↪ A^V are a compatible pair in the sense of groupCohomology.map, and so induce

Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ V, A^V).

The transition maps therefore run opposite to the quotient homomorphisms, and the system is a functor on the opposite of the index poset. This file builds it over the open normal subgroups of a topological group, which is the index poset the profinite colimit theorem uses. That theorem — that the colimit of this system computes the continuous cohomology of G — needs G profinite and the coefficients discrete, and is not stated here: no construction or law below assumes either hypothesis, and no comparison map to continuous cohomology is constructed.

The finite-level tower built here is the one the standard accounts of profinite cohomology describe; the references below state the colimit theorem this system is the source of.

Main definitions

• TauCeti.ContCohomology.continuousFiniteQuotientMap G hVU: the quotient homomorphism TauCeti.QuotientGroup.mapOfLE, bundled as a continuous homomorphism when U and V are open normal subgroups.
• TauCeti.invariantsInclusion A hVU: the inclusion A^U ↪ A^V for V ≤ U.
• TauCeti.transitionPair A hVU: the compatible pair assembled from the two.
• TauCeti.finiteLevelTransition A hVU n: the induced map Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ V, A^V).
• TauCeti.finiteLevelFunctor k U n: the U-level A ↦ Hⁿ(G ⧸ U, A^U) as a functor of the coefficient representation.
• TauCeti.finiteQuotientSystem A n: the system as a functor (OpenNormalSubgroup G)ᵒᵖ ⥤ ModuleCat k.
• TauCeti.finiteQuotientSystemFunctor k G n: the same system, as a functor of the coefficient representation.

Main statements

• TauCeti.toFiniteQuotientFunctor_map_hom_hom: the group half of the system is exactly the tower of Mathlib's ProfiniteGrp.toFiniteQuotientFunctor.
• TauCeti.invariantsInclusion_equivariant: the coefficient inclusion is equivariant after restriction along QuotientGroup.mapOfLE, which is what makes transitionPair a compatible pair.
• TauCeti.finiteLevelTransition_refl and TauCeti.finiteLevelTransition_comp: the two functor laws, which are what make the transition maps a system on the opposite poset.
• TauCeti.transitionPair_naturality and TauCeti.finiteLevelTransition_naturality: a morphism of coefficients commutes with the transition pairs, and hence with the transition maps.

Implementation notes

Everything except the continuous quotient map, the two OpenNormalSubgroup-indexed functors, and the comparison theorem is stated for arbitrary normal subgroups V ≤ U of an arbitrary group, since that is all the proofs use. Openness makes the source of the continuous quotient map discrete and supplies the index poset OpenNormalSubgroup G. Profiniteness enters only in TauCeti.toFiniteQuotientFunctor_map_hom_hom, which quantifies over an object of ProfiniteGrp because it compares with a functor Mathlib defines on that category; it is a hypothesis of no construction and of no transition law here. What the later colimit theorem adds, over this same index poset, is profiniteness of G as an unbundled hypothesis together with discreteness of the coefficients, in order to identify the colimit with continuous cohomology.

The group half of the transition pairs is TauCeti.QuotientGroup.mapOfLE, which is generic quotient-group infrastructure and lives in TauCeti.GroupTheory.QuotientGroup.Map: it is the canonical transition map of the system of quotient groups of G, and of the systems built from those quotients, not of this one only, and this file consumes it together with its _mk, _refl and _comp lemmas.

invariantsInclusion, transitionPair and finiteLevelTransition keep their bodies sealed: each is characterized by its _apply_coe, _hom_toLinearMap and functor-law lemmas, and those lemmas are proved as (rfl), so no consumer unfolds a body. The three functors are @[expose] instead, because the statement of a functor's map lemma does not elaborate with the body sealed: the left-hand side lives in F.obj A ⟶ F.obj B and the right-hand side in the type the obj field reduces to, so without the body the characteristic lemma cannot even be written down.

This implements the six milestones of the "The system" bullet of Layer 4 of the human-authored roadmap at TauCetiRoadmap/ProfiniteCohomology/README.md, together with the functoriality of the whole system in the coefficients that the same bullet asks for. The colimit theorem of that same layer is separate, and stays out: it is stated on the explicit low-degree complex and compared with the canonical object, so it consumes the roadmap's Layers 2 and 3, neither of which the system built here uses — every ingredient below is Mathlib's.

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).

The two halves of a transition pair

theorem TauCeti.invariants_le {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} (hVU : V ≤ U) : Representation.invariants (MonoidHom.comp A.ρ U.subtype) ≤ Representation.invariants (MonoidHom.comp A.ρ V.subtype)

Invariants grow as the subgroup shrinks: a vector fixed by U is fixed by every V ≤ U.

noncomputable def TauCeti.invariantsInclusion {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} (hVU : V ≤ U) : ↥(Representation.invariants (MonoidHom.comp A.ρ U.subtype)) →ₗ[k] ↥(Representation.invariants (MonoidHom.comp A.ρ V.subtype))

The coefficient half of a transition pair of the finite-quotient system: the inclusion A^U ↪ A^V for V ≤ U.

Equations

• TauCeti.invariantsInclusion A hVU = Submodule.inclusion ⋯

@[simp]

theorem TauCeti.invariantsInclusion_apply_coe {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} (hVU : V ≤ U) (m : ↥(Representation.invariants (MonoidHom.comp A.ρ U.subtype))) : ↑((invariantsInclusion A hVU) m) = ↑m

The inclusion A^U ↪ A^V moves no element of A.

@[simp]

theorem TauCeti.invariantsInclusion_refl {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U : Subgroup G} : invariantsInclusion A ⋯ = LinearMap.id

The inclusion of A^U into itself is the identity.

@[simp]

theorem TauCeti.invariantsInclusion_comp {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V W : Subgroup G} (hWV : W ≤ V) (hVU : V ≤ U) : invariantsInclusion A hWV ∘ₗ invariantsInclusion A hVU = invariantsInclusion A ⋯

Inclusions of invariants compose: A^U ↪ A^V ↪ A^W is the inclusion A^U ↪ A^W.

def TauCeti.ContCohomology.continuousFiniteQuotientMap (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) : G ⧸ ↑V.toOpenSubgroup →ₜ* G ⧸ ↑U.toOpenSubgroup

The quotient homomorphism G ⧸ V → G ⧸ U, bundled with its automatic continuity for open normal subgroups.

Equations

• TauCeti.ContCohomology.continuousFiniteQuotientMap G hVU = { toMonoidHom := TauCeti.QuotientGroup.mapOfLE hVU, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.ContCohomology.continuousFiniteQuotientMap_mk (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) (g : G) : (continuousFiniteQuotientMap G hVU) ↑g = ↑g

The map G ⧸ V → G ⧸ U sends the class of g to the class of g.

@[simp]

theorem TauCeti.ContCohomology.continuousFiniteQuotientMap_refl (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (U : OpenNormalSubgroup G) : continuousFiniteQuotientMap G ⋯ = ContinuousMonoidHom.id (G ⧸ ↑U.toOpenSubgroup)

The map G ⧸ U → G ⧸ U along U ≤ U is the identity.

@[simp]

theorem TauCeti.ContCohomology.continuousFiniteQuotientMap_comp (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V W : OpenNormalSubgroup G} (hWV : W ≤ V) (hVU : V ≤ U) : (continuousFiniteQuotientMap G hVU).comp (continuousFiniteQuotientMap G hWV) = continuousFiniteQuotientMap G ⋯

The maps between finite quotients compose: G ⧸ W → G ⧸ V → G ⧸ U is G ⧸ W → G ⧸ U.

@[simp]

theorem TauCeti.ContCohomology.continuousFiniteQuotientMap_comp_quotientMk (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {U V : OpenNormalSubgroup G} (hVU : V ≤ U) : (continuousFiniteQuotientMap G hVU).comp (ContinuousMonoidHom.quotientMk ↑V.toOpenSubgroup) = ContinuousMonoidHom.quotientMk ↑U.toOpenSubgroup

The quotient homomorphism G → G ⧸ U factors through every deeper quotient: for V ≤ U it is the transition map G ⧸ V → G ⧸ U after G → G ⧸ V.

The transition maps of the system

theorem TauCeti.invariantsInclusion_equivariant {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) (x : G ⧸ V) (m : ↥(Representation.invariants (MonoidHom.comp A.ρ U.subtype))) : (invariantsInclusion A hVU) (((A.quotientToInvariants U).ρ ((QuotientGroup.mapOfLE hVU) x)) m) = ((A.quotientToInvariants V).ρ x) ((invariantsInclusion A hVU) m)

Equivariance of the coefficient inclusion after restriction along QuotientGroup.mapOfLE: the G ⧸ U-action on A^U, pulled back along G ⧸ V →* G ⧸ U, agrees with the G ⧸ V-action on A^V. This holds because the action of g on A^U depends only on the class of g modulo any subgroup of U, and it is what makes TauCeti.transitionPair well typed.

noncomputable def TauCeti.transitionPair {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : Rep.res (QuotientGroup.mapOfLE hVU) (A.quotientToInvariants U) ⟶ A.quotientToInvariants V

A transition pair of the finite-quotient system, assembled from TauCeti.QuotientGroup.mapOfLE and TauCeti.invariantsInclusion.

Equations

• TauCeti.transitionPair A hVU = Rep.ofHom { toLinearMap := TauCeti.invariantsInclusion A hVU, isIntertwining' := ⋯ }

@[simp]

theorem TauCeti.transitionPair_hom_toLinearMap {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : (Rep.Hom.hom (transitionPair A hVU)).toLinearMap = invariantsInclusion A hVU

The underlying linear map of the transition pair is the inclusion A^U ↪ A^V.

noncomputable def TauCeti.finiteLevelTransition {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) (n : ℕ) : groupCohomology (A.quotientToInvariants U) n ⟶ groupCohomology (A.quotientToInvariants V) n

The transition map of the finite-quotient system: Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ V, A^V) for normal subgroups V ≤ U, induced by TauCeti.transitionPair.

Equations

• TauCeti.finiteLevelTransition A hVU n = groupCohomology.map (TauCeti.QuotientGroup.mapOfLE hVU) (TauCeti.transitionPair A hVU) n

@[simp]

theorem TauCeti.finiteLevelTransition_refl {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (U : Subgroup G) [U.Normal] (n : ℕ) : finiteLevelTransition A ⋯ n = CategoryTheory.CategoryStruct.id (groupCohomology (A.quotientToInvariants U) n)

The first functor law: the transition map from a level to itself is the identity.

theorem TauCeti.finiteLevelTransition_comp {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V W : Subgroup G} [U.Normal] [V.Normal] [W.Normal] (hWV : W ≤ V) (hVU : V ≤ U) (n : ℕ) : finiteLevelTransition A ⋯ n = CategoryTheory.CategoryStruct.comp (finiteLevelTransition A hVU n) (finiteLevelTransition A hWV n)

The second functor law: for W ≤ V ≤ U the transition from the U-level to the W-level is the composite through the V-level. With TauCeti.finiteLevelTransition_refl this says the finite-quotient system is a functor on the opposite of the poset of normal subgroups.

theorem TauCeti.finiteLevelTransition_comp_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) {U V W : Subgroup G} [U.Normal] [V.Normal] [W.Normal] (hWV : W ≤ V) (hVU : V ≤ U) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology (A.quotientToInvariants W) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (finiteLevelTransition A ⋯ n) h = CategoryTheory.CategoryStruct.comp (finiteLevelTransition A hVU n) (CategoryTheory.CategoryStruct.comp (finiteLevelTransition A hWV n) h)

The second functor law: for W ≤ V ≤ U the transition from the U-level to the W-level is the composite through the V-level. With TauCeti.finiteLevelTransition_refl this says the finite-quotient system is a functor on the opposite of the poset of normal subgroups.

Functoriality in the coefficients

noncomputable def TauCeti.finiteLevelFunctor (k : Type u) {G : Type u} [CommRing k] [Group G] (U : Subgroup G) [U.Normal] (n : ℕ) : CategoryTheory.Functor (Rep k G) (ModuleCat k)

The U-level of the finite-quotient system, as a functor of the coefficients: the composite of Mathlib's Rep.quotientToInvariantsFunctor with groupCohomology.functor, sending a G-representation A to Hⁿ(G ⧸ U, A^U). Its map is the coefficient half of the functoriality of the whole system, and it is the source of Mathlib's inflation natural transformation groupCohomology.infNatTrans.

Equations

• TauCeti.finiteLevelFunctor k U n = (Rep.quotientToInvariantsFunctor k U).comp (groupCohomology.functor k (G ⧸ U) n)

@[simp]

theorem TauCeti.finiteLevelFunctor_obj {k G : Type u} [CommRing k] [Group G] (U : Subgroup G) [U.Normal] (n : ℕ) (A : Rep k G) : (finiteLevelFunctor k U n).obj A = groupCohomology (A.quotientToInvariants U) n

finiteLevelFunctor k U n sends A to Hⁿ(G ⧸ U, A^U).

@[simp]

theorem TauCeti.finiteLevelFunctor_map {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} (U : Subgroup G) [U.Normal] (n : ℕ) (f : A ⟶ B) : (finiteLevelFunctor k U n).map f = groupCohomology.map (MonoidHom.id (G ⧸ U)) ((Rep.quotientToInvariantsFunctor k U).map f) n

finiteLevelFunctor k U n sends f : A ⟶ B to the map Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ U, B^U) induced by f on U-invariants.

theorem TauCeti.transitionPair_naturality {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} {U V : Subgroup G} [U.Normal] [V.Normal] (f : A ⟶ B) (hVU : V ≤ U) : (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor (MonoidHom.id (G ⧸ V))).map (transitionPair A hVU)) ((Rep.quotientToInvariantsFunctor k V).map f))).toLinearMap = (Rep.Hom.hom (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor (QuotientGroup.mapOfLE hVU)).map ((Rep.quotientToInvariantsFunctor k U).map f)) (transitionPair B hVU))).toLinearMap

The coefficient square of the finite-quotient system: a transition pair is natural in the coefficients. Applying a morphism f : A ⟶ B on V-invariants after the inclusion A^U ↪ A^V is applying it on U-invariants and then including B^U ↪ B^V; both composites send m : A^U to f m. It is stated on the underlying linear maps because that is the form in which groupCohomology.map_congr compares two compatible pairs, and it is the substance of TauCeti.finiteLevelTransition_naturality.

theorem TauCeti.finiteLevelTransition_naturality {k G : Type u} [CommRing k] [Group G] {A B : Rep k G} {U V : Subgroup G} [U.Normal] [V.Normal] (f : A ⟶ B) (hVU : V ≤ U) (n : ℕ) : CategoryTheory.CategoryStruct.comp (finiteLevelTransition A hVU n) ((finiteLevelFunctor k V n).map f) = CategoryTheory.CategoryStruct.comp ((finiteLevelFunctor k U n).map f) (finiteLevelTransition B hVU n)

A morphism of coefficients commutes with the transition maps of the finite-quotient system. This is the naturality of TauCeti.finiteQuotientSystem in the coefficient representation.

The system over the open normal subgroups

theorem TauCeti.toFiniteQuotientFunctor_map_hom_hom (P : ProfiniteGrp.{u}) {U V : OpenNormalSubgroup ↑P.toProfinite.toTop} (f : V ⟶ U) : GrpCat.Hom.hom (P.toFiniteQuotientFunctor.map f).hom = QuotientGroup.mapOfLE ⋯

The tower of quotient homomorphisms of the finite-quotient system is Mathlib's ProfiniteGrp.toFiniteQuotientFunctor. Its arrows run from the smaller subgroup to the larger one, which is why the cohomological system below is indexed by the opposite category.

noncomputable def TauCeti.finiteQuotientSystem {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [TopologicalSpace G] (n : ℕ) : CategoryTheory.Functor (OpenNormalSubgroup G)ᵒᵖ (ModuleCat k)

The finite-quotient system of a G-representation A: the functor sending an open normal subgroup U of G to Hⁿ(G ⧸ U, A^U), with TauCeti.finiteLevelTransition for its arrows.

The index category is the opposite of OpenNormalSubgroup G because the transition maps run from the U-level to the V-level for V ≤ U, opposite to the quotient homomorphisms G ⧸ V → G ⧸ U of ProfiniteGrp.toFiniteQuotientFunctor.

Equations

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

@[simp]

theorem TauCeti.finiteQuotientSystem_obj {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [TopologicalSpace G] (n : ℕ) (U : (OpenNormalSubgroup G)ᵒᵖ) : (finiteQuotientSystem A n).obj U = groupCohomology (A.quotientToInvariants ↑(Opposite.unop U).toOpenSubgroup) n

The finite-quotient system of A sends U to Hⁿ(G ⧸ U, A^U).

@[simp]

theorem TauCeti.finiteQuotientSystem_map {k G : Type u} [CommRing k] [Group G] (A : Rep k G) [TopologicalSpace G] (n : ℕ) {U V : (OpenNormalSubgroup G)ᵒᵖ} (f : U ⟶ V) : (finiteQuotientSystem A n).map f = finiteLevelTransition A ⋯ n

The finite-quotient system of A sends an inclusion V ≤ U to the transition map Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ V, A^V).

noncomputable def TauCeti.finiteQuotientSystemFunctor (k G : Type u) [CommRing k] [Group G] [TopologicalSpace G] (n : ℕ) : CategoryTheory.Functor (Rep k G) (CategoryTheory.Functor (OpenNormalSubgroup G)ᵒᵖ (ModuleCat k))

The finite-quotient system as a functor of the coefficient representation: this packages TauCeti.finiteQuotientSystem together with the naturality of its transition maps in the coefficients.

Equations

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

@[simp]

theorem TauCeti.finiteQuotientSystemFunctor_obj {k G : Type u} [CommRing k] [Group G] [TopologicalSpace G] (n : ℕ) (A : Rep k G) : (finiteQuotientSystemFunctor k G n).obj A = finiteQuotientSystem A n

finiteQuotientSystemFunctor k G n sends A to its finite-quotient system.

@[simp]

theorem TauCeti.finiteQuotientSystemFunctor_map_app {k G : Type u} [CommRing k] [Group G] [TopologicalSpace G] (n : ℕ) {A B : Rep k G} (f : A ⟶ B) (U : (OpenNormalSubgroup G)ᵒᵖ) : ((finiteQuotientSystemFunctor k G n).map f).app U = (finiteLevelFunctor k (↑(Opposite.unop U).toOpenSubgroup) n).map f

At U, the finite-quotient system of f : A ⟶ B is the map Hⁿ(G ⧸ U, A^U) ⟶ Hⁿ(G ⧸ U, B^U) induced by f.