Change of groups on bar coinvariants

For f : G →* H and a compatible coefficient map φ : A ⟶ Rep.res f B, the map on bar coinvariants sends ⟦a ⊗ c⟧ to ⟦φ(a) ⊗ f_*(c)⟧. This file constructs it by transporting Mathlib's inhomogeneous chain map across Amelia Livingston's inhomogeneousChainsIso, then proves this tensor formula. Thus the construction works for arbitrary homomorphisms, including ones for which restriction does not preserve projective representations.

The chain square and its induced homology square identify the algebraic change-of-group map in comparisons with equivariant chains of a contractible free group action. Coefficients may have nontrivial action. The bar map uses the existing TauCeti.Rep.barComplex.resChainMap, which applies the homomorphism to all group labels.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Chapters I.5 and III.8.

noncomputable def MonoidHom.barCoinvariantsMap {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) : HomologicalComplex.coinvariantsTensorObj A (Rep.barComplex k G) ⟶ HomologicalComplex.coinvariantsTensorObj B (Rep.barComplex k H)

Change of groups on bar coinvariants. On tensor classes this applies the compatible coefficient map in the first factor and relabels the bar chain in the second factor.

theorem MonoidHom.inhomogeneousChainsIso_hom_barCoinvariantsMap {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) : CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso A).hom (f.barCoinvariantsMap φ) = CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap f φ) (groupHomology.inhomogeneousChainsIso B).hom

The inhomogeneous-to-bar chain identification commutes with change of groups and compatible coefficient maps.

theorem MonoidHom.inhomogeneousChainsIso_hom_barCoinvariantsMap_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ChainComplex (ModuleCat k) ℕ} (h : HomologicalComplex.coinvariantsTensorObj B (Rep.barComplex k H) ⟶ Z) : CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso A).hom (CategoryTheory.CategoryStruct.comp (f.barCoinvariantsMap φ) h) = CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap f φ) (CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso B).hom h)

The inhomogeneous-to-bar chain identification commutes with change of groups and compatible coefficient maps.

theorem MonoidHom.barCoinvariantsMap_inhomogeneousChainsIso_inv {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) : CategoryTheory.CategoryStruct.comp (f.barCoinvariantsMap φ) (groupHomology.inhomogeneousChainsIso B).inv = CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso A).inv (groupHomology.chainsMap f φ)

The inverse chain identification also commutes with change of groups.

theorem MonoidHom.barCoinvariantsMap_inhomogeneousChainsIso_inv_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ChainComplex (ModuleCat k) ℕ} (h : groupHomology.inhomogeneousChains B ⟶ Z) : CategoryTheory.CategoryStruct.comp (f.barCoinvariantsMap φ) (CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso B).inv h) = CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChainsIso A).inv (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap f φ) h)

The inverse chain identification also commutes with change of groups.

@[simp]

theorem MonoidHom.barCoinvariantsMap_f_mk_tmul {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) (a : ↑A) (c : (Fin n → G) →₀ MonoidAlgebra k G) : (CategoryTheory.ConcreteCategory.hom ((f.barCoinvariantsMap φ).f n)) ((Representation.Coinvariants.mk (A.ρ.tprod (Representation.free k G (Fin n → G)))) (a ⊗ₜ[k] c)) = (Representation.Coinvariants.mk (B.ρ.tprod (Representation.free k H (Fin n → H)))) ((Rep.Hom.hom φ) a ⊗ₜ[k] (Rep.Hom.hom ((TauCeti.Rep.barComplex.resChainMap f).f n)) c)

On any tensor class the bar map is the tensor of the coefficient map and the existing bar-resolution map, followed by passage to the target coinvariants.

@[simp]

theorem MonoidHom.barCoinvariantsMap_id {k G : Type u} [CommRing k] [Group G] [DecidableEq G] {A : Rep.{u, u, u} k G} : (id G).barCoinvariantsMap (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (HomologicalComplex.coinvariantsTensorObj A (Rep.barComplex k G))

The identity homomorphism and identity coefficient map induce the identity on bar coinvariants.

theorem MonoidHom.barCoinvariantsMap_comp {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {K : Type u} [Group K] [DecidableEq K] {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K) (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) : (g.comp f).barCoinvariantsMap (CategoryTheory.CategoryStruct.comp φ ((Rep.resFunctor f).map ψ)) = CategoryTheory.CategoryStruct.comp (f.barCoinvariantsMap φ) (g.barCoinvariantsMap ψ)

Change of groups on bar coinvariants respects composition of both the homomorphisms and the compatible coefficient maps.

theorem MonoidHom.inhomogeneousChainsIso_homologyMap_barCoinvariantsMap {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (groupHomology.inhomogeneousChainsIso A).hom n) (HomologicalComplex.homologyMap (f.barCoinvariantsMap φ) n) = CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n) (HomologicalComplex.homologyMap (groupHomology.inhomogeneousChainsIso B).hom n)

The induced map on the homology of bar coinvariants is Mathlib's change-of-group map on group homology under the existing chain identifications.

theorem MonoidHom.inhomogeneousChainsIso_homologyMap_barCoinvariantsMap_assoc {k G H : Type u} [CommRing k] [Group G] [Group H] [DecidableEq G] [DecidableEq H] {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (n : ℕ) {Z : ModuleCat k} (h : HomologicalComplex.homology (HomologicalComplex.coinvariantsTensorObj B (Rep.barComplex k H)) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (groupHomology.inhomogeneousChainsIso A).hom n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (f.barCoinvariantsMap φ) n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (groupHomology.map f φ n) (HomologicalComplex.homologyMap (groupHomology.inhomogeneousChainsIso B).hom n)) h

The induced map on the homology of bar coinvariants is Mathlib's change-of-group map on group homology under the existing chain identifications.