Change of groups for group cohomology computed by resolutions #
Let f : G →* H be a group homomorphism and φ : Res(f)(A) ⟶ B a compatible map of coefficient
representations. A chain map α : P ⟶ Res(f)(Q) from a complex of G-representations to the
restriction of a complex of H-representations induces the cochain map
MonoidHom.linearYonedaObjMap f φ α : Hom_H(Q, A) ⟶ Hom_G(P, B), which sends g : Q ⟶ A to
φ ∘ g ∘ α. This cochain map and its composition and homotopy lemmas only need G and H to be
monoids.
When P and Q are projective resolutions of the trivial representations and α lies over the
identity of k, Mathlib's identifications groupCohomologyIso of group cohomology with the
cohomology of Hom_H(Q, A) and Hom_G(P, B) carry Mathlib's change-of-group map
groupCohomology.map f φ n to the map induced by linearYonedaObjMap f φ α
(MonoidHom.groupCohomologyIso_inv_naturality). No hypothesis on f is needed. Restriction
along f need not preserve projective representations, so α is in general not a map of
projective resolutions in Rep k G; only the exactness of the restricted target is used. This
computes change-of-group maps with geometric resolutions, such as the singular chains of a
contractible free G-space, without passing through the bar resolution.
The proof computes groupCohomologyIso through comparison maps from the bar resolutions
(TauCeti.Rep.groupCohomologyIso_inv_eq_homologyMap), uses that the two composites from the bar
resolution of G to Res(f)(Q) are homotopic (MonoidHom.barResolutionComparisonHomotopy), and
that on the bar resolutions the cochain map is Mathlib's inhomogeneous groupCohomology.cochainsMap
(MonoidHom.inhomogeneousCochainsIso_hom_linearYonedaObjMap_resChainMap).
Main definitions #
MonoidHom.linearYonedaObjMap: the cochain mapHom_H(Q, A) ⟶ Hom_G(P, B)induced byf,φandα.
Main results #
MonoidHom.groupCohomologyIso_hom_naturality,MonoidHom.groupCohomologyIso_inv_naturality: group cohomology computed by projective resolutions is natural in the group.MonoidHom.inhomogeneousCochainsIso_hom_linearYonedaObjMap_resChainMap: on bar resolutions the cochain map is Mathlib's inhomogeneous change of groups.MonoidHom.homologyMap_linearYonedaObjMap_eq_of_homotopy: homotopic chain maps induce the same map on cohomology.
References #
- K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Chapter III, §8, and Chapter I, §7.
The group cohomology comparisons and change-of-group maps used here are Mathlib's constructions by
Amelia Livingston; no alternative group cohomology is introduced. This file is the cohomological
counterpart of TauCeti.RepresentationTheory.Homological.GroupHomology.ChangeOfGroups.
Change of groups on morphism complexes. For f : G →* H, a compatible coefficient map
φ : Res(f)(A) ⟶ B and a chain map α : P ⟶ Res(f)(Q), this is the cochain map
Hom_H(Q, A) ⟶ Hom_G(P, B) sending g : Q ⟶ A to φ ∘ g ∘ α.
Instances For
The cochain map sends g : Q ⟶ A to φ ∘ g ∘ α.
Postcomposing with the map induced by a chain map β : P' ⟶ P amounts to precomposing α
with β.
Postcomposing with the map induced by a chain map β : P' ⟶ P amounts to precomposing α
with β.
Precomposing with the map induced by a chain map γ : Q ⟶ Q' amounts to postcomposing α
with the restriction of γ.
Precomposing with the map induced by a chain map γ : Q ⟶ Q' amounts to postcomposing α
with the restriction of γ.
Homotopic chain maps induce the same map on the cohomology of morphism complexes.
On the bar resolutions, the cochain map of the relabelling chain map
TauCeti.Rep.barComplex.resChainMap is Mathlib's change of groups on inhomogeneous cochains.
On the bar resolutions, the cochain map of the relabelling chain map
TauCeti.Rep.barComplex.resChainMap is Mathlib's change of groups on inhomogeneous cochains.
The inverse form of inhomogeneousCochainsIso_hom_linearYonedaObjMap_resChainMap.
The inverse form of inhomogeneousCochainsIso_hom_linearYonedaObjMap_resChainMap.
Group cohomology computed by resolutions is natural in the group. For f : G →* H, a
compatible coefficient map φ : Res(f)(A) ⟶ B, projective resolutions P and Q of the trivial
representations and an augmentation-preserving chain map α : P ⟶ Res(f)(Q), the identifications
groupCohomologyIso carry the map induced on cohomology by g ↦ φ ∘ g ∘ α to Mathlib's
change-of-group map groupCohomology.map f φ n. No hypothesis on f is needed: restriction along
f need not preserve projective representations.
Group cohomology computed by resolutions is natural in the group. For f : G →* H, a
compatible coefficient map φ : Res(f)(A) ⟶ B, projective resolutions P and Q of the trivial
representations and an augmentation-preserving chain map α : P ⟶ Res(f)(Q), the identifications
groupCohomologyIso carry the map induced on cohomology by g ↦ φ ∘ g ∘ α to Mathlib's
change-of-group map groupCohomology.map f φ n. No hypothesis on f is needed: restriction along
f need not preserve projective representations.
The forward identifications are also natural in the group.
The forward identifications are also natural in the group.