Naturality of the connecting map in group cohomology under change of group

Mathlib's groupCohomology.δ is the connecting map Hⁱ(G, X₃) ⟶ Hʲ(G, X₁), i + 1 = j, of the long exact sequence of a short exact sequence X of G-representations, and groupCohomology.δ_naturality states its naturality for a morphism of short exact sequences of G-representations — that is, along the identity of G. This file removes that restriction. Given f : G →* H, a short exact sequence Y of H-representations, a short exact sequence X of G-representations, and a morphism Φ : Res_f Y ⟶ X of short complexes, the square

Hⁱ(H, Y₃) ⟶ Hʲ(H, Y₁) ↓ ↓ Hⁱ(G, X₃) ⟶ Hʲ(G, X₁)

formed by the two connecting maps and the change-of-group maps groupCohomology.map f Φ.τᵢ commutes. Restriction to a subgroup and inflation from a quotient are both change-of-group maps, so this contains the compatibility of δ with each of them.

Main definitions

• TauCeti.groupCohomology.cochainsMapShortComplex: the morphism of short complexes of cochain complexes induced by a morphism Res_f Y ⟶ X along f : G →* H; its components are groupCohomology.cochainsMap f Φ.τᵢ (cochainsMapShortComplex_τ₁ and its siblings).

Main results

• TauCeti.groupCohomology.δ_naturality: the connecting map of group cohomology commutes with change-of-group maps.

References

• The restriction and inflation cases are rest_δ_naturality (ClassFieldTheory/Cohomology/Functors/Restriction.lean) and infl_δ_naturality (ClassFieldTheory/Cohomology/Functors/Inflation.lean) in kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509 (Apache-2.0), proved by the same reduction to HomologicalComplex.HomologySequence.δ_naturality; this file generalises them to an arbitrary morphism Φ : Res_f Y ⟶ X.

noncomputable def TauCeti.groupCohomology.cochainsMapShortComplex {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : Y.map (Rep.resFunctor f) ⟶ X) : Y.map (groupCohomology.cochainsFunctor k H) ⟶ X.map (groupCohomology.cochainsFunctor k G)

A morphism Φ : Res_f Y ⟶ X of short complexes of representations, along a group homomorphism f : G →* H, induces a morphism between the short complexes of inhomogeneous cochain complexes, given in each position by groupCohomology.cochainsMap f.

Equations

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

@[simp]

theorem TauCeti.groupCohomology.cochainsMapShortComplex_τ₁ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : Y.map (Rep.resFunctor f) ⟶ X) : (cochainsMapShortComplex f Φ).τ₁ = groupCohomology.cochainsMap f Φ.τ₁

The first component of cochainsMapShortComplex f Φ is the cochain map induced by the pair (f, Φ.τ₁).

@[simp]

theorem TauCeti.groupCohomology.cochainsMapShortComplex_τ₂ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : Y.map (Rep.resFunctor f) ⟶ X) : (cochainsMapShortComplex f Φ).τ₂ = groupCohomology.cochainsMap f Φ.τ₂

The second component of cochainsMapShortComplex f Φ is the cochain map induced by the pair (f, Φ.τ₂).

@[simp]

theorem TauCeti.groupCohomology.cochainsMapShortComplex_τ₃ {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (Φ : Y.map (Rep.resFunctor f) ⟶ X) : (cochainsMapShortComplex f Φ).τ₃ = groupCohomology.cochainsMap f Φ.τ₃

The third component of cochainsMapShortComplex f Φ is the cochain map induced by the pair (f, Φ.τ₃).

theorem TauCeti.groupCohomology.δ_naturality {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (hY : Y.ShortExact) (hX : X.ShortExact) (Φ : Y.map (Rep.resFunctor f) ⟶ X) (i j : ℕ) (hij : i + 1 = j) : CategoryTheory.CategoryStruct.comp (groupCohomology.δ hY i j hij) (groupCohomology.map f Φ.τ₁ j) = CategoryTheory.CategoryStruct.comp (groupCohomology.map f Φ.τ₃ i) (groupCohomology.δ hX i j hij)

The connecting map of group cohomology is natural with respect to change of group. For short exact sequences Y of H-representations and X of G-representations, and a morphism Φ : Res_f Y ⟶ X along f : G →* H, the connecting maps commute with the change-of-group maps groupCohomology.map f.

theorem TauCeti.groupCohomology.δ_naturality_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] (f : G →* H) {X : CategoryTheory.ShortComplex (Rep k G)} {Y : CategoryTheory.ShortComplex (Rep k H)} (hY : Y.ShortExact) (hX : X.ShortExact) (Φ : Y.map (Rep.resFunctor f) ⟶ X) (i j : ℕ) (hij : i + 1 = j) {Z : ModuleCat k} (h : groupCohomology X.X₁ j ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupCohomology.δ hY i j hij) (CategoryTheory.CategoryStruct.comp (groupCohomology.map f Φ.τ₁ j) h) = CategoryTheory.CategoryStruct.comp (groupCohomology.map f Φ.τ₃ i) (CategoryTheory.CategoryStruct.comp (groupCohomology.δ hX i j hij) h)

The connecting map of group cohomology is natural with respect to change of group. For short exact sequences Y of H-representations and X of G-representations, and a morphism Φ : Res_f Y ⟶ X along f : G →* H, the connecting maps commute with the change-of-group maps groupCohomology.map f.