Change of groups for group homology computed by resolutions #
Let f : G →* H be a group homomorphism and φ : A ⟶ Res(f)(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 chain map
MonoidHom.coinvariantsTensorChainMap f φ α : (A ⊗ P)_G ⟶ (B ⊗ Q)_H, which sends the class of
a ⊗ c to the class of φ a ⊗ α c. In each degree it is the map
MonoidHom.coinvariantsTensorMap on tensor coinvariants of representations.
When P and Q are projective resolutions of the trivial representations and α lies over the
identity of k, Mathlib's identifications groupHomologyIso of group homology with the homology
of (A ⊗ P)_G and (B ⊗ Q)_H carry Mathlib's change-of-group map groupHomology.map f φ n to the
map induced by coinvariantsTensorChainMap f φ α (MonoidHom.groupHomologyIso_hom_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 groupHomologyIso through comparison maps from the bar resolutions
(Rep.groupHomologyIso_hom_eq_homologyMap), uses that the two composites from the bar
resolution of G to Res(f)(Q) are homotopic (MonoidHom.barResolutionComparisonHomotopy), and
that on bar coinvariants the change-of-group map is groupHomology.map
(MonoidHom.inhomogeneousChainsIso_homologyMap_barCoinvariantsMap).
Main definitions #
MonoidHom.coinvariantsTensorChainMap: the chain map(A ⊗ P)_G ⟶ (B ⊗ Q)_Hinduced byf,φandα.
Main results #
MonoidHom.groupHomologyIso_hom_naturality,MonoidHom.groupHomologyIso_inv_naturality: group homology computed by projective resolutions is natural in the group.MonoidHom.barCoinvariantsMap_eq_coinvariantsTensorChainMap: on bar resolutions the chain map is the existing change of groups on bar coinvariants.MonoidHom.homologyMap_coinvariantsTensorChainMap_eq_of_homotopy: homotopic chain maps induce the same map on homology.
References #
- K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Chapter III, §8, and Chapter I, §7.
The group homology comparisons and change-of-group maps used here are Mathlib's constructions by Amelia Livingston; no alternative group homology is introduced.
Change of groups on tensor coinvariants of complexes. For f : G →* H, a compatible
coefficient map φ : A ⟶ Res(f)(B) and a chain map α : P ⟶ Res(f)(Q), this is the chain map
(A ⊗ P)_G ⟶ (B ⊗ Q)_H sending the class of a ⊗ c to the class of φ a ⊗ α c.
Instances For
The component in degree n is the change-of-group map on tensor coinvariants.
The chain map sends the class of a ⊗ c to the class of φ a ⊗ α c.
Precomposing with the map induced by a chain map β : P' ⟶ P amounts to precomposing α
with β.
Precomposing with the map induced by a chain map β : P' ⟶ P amounts to precomposing α
with β.
Postcomposing with the map induced by a chain map γ : Q ⟶ Q' amounts to postcomposing α
with the restriction of γ.
Postcomposing 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 homology of tensor coinvariants.
Change of groups on bar coinvariants is the coinvariant map of the relabelling chain map
TauCeti.Rep.barComplex.resChainMap of the bar resolutions.
Group homology computed by resolutions is natural in the group. For f : G →* H, a
compatible coefficient map φ : A ⟶ Res(f)(B), projective resolutions P and Q of the trivial
representations and an augmentation-preserving chain map α : P ⟶ Res(f)(Q), the identifications
groupHomologyIso carry Mathlib's change-of-group map groupHomology.map f φ n to the map induced
on the homology of tensor coinvariants by ⟦a ⊗ c⟧ ↦ ⟦φ a ⊗ α c⟧. No hypothesis on f is
needed: restriction along f need not preserve projective representations.
Group homology computed by resolutions is natural in the group. For f : G →* H, a
compatible coefficient map φ : A ⟶ Res(f)(B), projective resolutions P and Q of the trivial
representations and an augmentation-preserving chain map α : P ⟶ Res(f)(Q), the identifications
groupHomologyIso carry Mathlib's change-of-group map groupHomology.map f φ n to the map induced
on the homology of tensor coinvariants by ⟦a ⊗ c⟧ ↦ ⟦φ a ⊗ α c⟧. No hypothesis on f is
needed: restriction along f need not preserve projective representations.
The inverse identifications are also natural in the group.
The inverse identifications are also natural in the group.