Equivariant maps on coinvariant singular chains

A continuous map equivariant along a group homomorphism induces a map on the coinvariants of singular chains. No injectivity or surjectivity of the homomorphism is required. These are the maps on the geometric resolutions used to compare the homology of quotient covers with group homology.

The map sends the class of a ⊗ c to the class of a ⊗ f_* c. It respects identities and composition, and is defined for arbitrary continuous actions, without freeness or contractibility assumptions. The descent uses Mathlib's Representation.Coinvariants.lift.

Before passing to coinvariants, pushing chains forward along f is a chain map TauCeti.singularChainsRepResMap from the equivariant singular chains of E to the restriction along φ of those of F, and it preserves the augmentations (TauCeti.singularChainsRepResMap_f_zero_comp_augmentation). The map on coinvariants is the change-of-groups map MonoidHom.coinvariantsTensorChainMap induced by it (TauCeti.singularChainsCoinvariantsMap_eq_coinvariantsTensorChainMap), which is how the group-homology naturality of MonoidHom.groupHomologyIso_hom_naturality applies to singular chains.

Main definitions

• TauCeti.singularChainsRepResMap: the equivariant pushforward of singular chains, as a chain map into the restricted complex.
• TauCeti.singularChainsCoinvariantsMap: the induced chain map on coinvariants.

References

• K. S. Brown, Cohomology of Groups, Springer GTM 87, Chapters II.4 and III.1.

theorem TauCeti.singularChains_map_f_representation (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (n : ℕ) (g : G) (c : ↑(((singularChains k).obj E).X n)) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) (((singularChainsRepresentation k E G n) g) c) = ((singularChainsRepresentation k F H n) (φ g)) ((CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) c)

Pushing singular chains forward along an equivariant map intertwines the actions, including when the acting monoids differ.

noncomputable def TauCeti.singularChainsRepResMap (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) : singularChainsRep k E G ⟶ ((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).obj (singularChainsRep k F H)

Pushing singular chains forward along an equivariant map is a chain map from the equivariant singular chains of E to the restriction along φ of the equivariant singular chains of F.

@[simp]

theorem TauCeti.singularChainsRepResMap_f_hom_apply (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (n : ℕ) (c : ↑(((singularChains k).obj E).X n)) : (Rep.Hom.hom ((singularChainsRepResMap k f hf).f n)) c = (CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) c

The equivariant chain map pushes chains forward along f.

theorem TauCeti.singularChainsRepResMap_f_zero_comp_augmentation (k : Type u) [CommRing k] {G H : Type u} [Monoid G] [Monoid H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) : CategoryTheory.CategoryStruct.comp ((singularChainsRepResMap k f hf).f 0) ((Rep.resFunctor φ).map ((singularChainsRepAugmentation k F H).f 0)) = (singularChainsRepAugmentation k E G).f 0

The equivariant pushforward of singular chains preserves the augmentations.

noncomputable def TauCeti.singularChainsCoinvariantsMap (k : Type u) [CommRing k] {G H : Type u} [Group G] [Group H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) : HomologicalComplex.coinvariantsTensorObj (Rep.trivial k G k) (singularChainsRep k E G) ⟶ HomologicalComplex.coinvariantsTensorObj (Rep.trivial k H k) (singularChainsRep k F H)

The chain map on coinvariants induced by a continuous map equivariant along φ. The coefficient representation is the trivial representation on k.

@[simp]

theorem TauCeti.singularChainsCoinvariantsMap_f_mk (k : Type u) [CommRing k] {G H : Type u} [Group G] [Group H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) (n : ℕ) (a : k) (c : ↑(((singularChains k).obj E).X n)) : (CategoryTheory.ConcreteCategory.hom ((singularChainsCoinvariantsMap k f hf).f n)) ((((Rep.trivial k G k).coinvariantsTensorMk (Rep.of (singularChainsRepresentation k E G n))) a) c) = (((Rep.trivial k H k).coinvariantsTensorMk (Rep.of (singularChainsRepresentation k F H n))) a) ((CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) c)

The map on coinvariants pushes forward the chain in a pure tensor.

@[simp]

theorem TauCeti.singularChainsCoinvariantsMap_id (k : Type u) [CommRing k] {G : Type u} [Group G] {E : TopCat} [MulAction G ↑E] [ContinuousConstSMul G ↑E] : singularChainsCoinvariantsMap k (CategoryTheory.CategoryStruct.id E) ⋯ = CategoryTheory.CategoryStruct.id (HomologicalComplex.coinvariantsTensorObj (Rep.trivial k G k) (singularChainsRep k E G))

The identity of a space induces the identity on coinvariant singular chains.

@[simp]

theorem TauCeti.singularChainsCoinvariantsMap_comp (k : Type u) [CommRing k] {G H K : Type u} [Group G] [Group H] [Group K] {E F D : TopCat} [MulAction G ↑E] [MulAction H ↑F] [MulAction K ↑D] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] [ContinuousConstSMul K ↑D] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) {ψ : H →* K} (q : F ⟶ D) (hq : ∀ (h : H) (x : ↑F), (CategoryTheory.ConcreteCategory.hom q) (h • x) = ψ h • (CategoryTheory.ConcreteCategory.hom q) x) : singularChainsCoinvariantsMap k (CategoryTheory.CategoryStruct.comp f q) ⋯ = CategoryTheory.CategoryStruct.comp (singularChainsCoinvariantsMap k f hf) (singularChainsCoinvariantsMap k q hq)

Equivariant continuous maps induce maps on coinvariant chains respecting composition.

theorem TauCeti.singularChainsCoinvariantsMap_eq_coinvariantsTensorChainMap (k : Type u) [CommRing k] {G H : Type u} [Group G] [Group H] {E F : TopCat} [MulAction G ↑E] [MulAction H ↑F] [ContinuousConstSMul G ↑E] [ContinuousConstSMul H ↑F] {φ : G →* H} (f : E ⟶ F) (hf : ∀ (g : G) (x : ↑E), (CategoryTheory.ConcreteCategory.hom f) (g • x) = φ g • (CategoryTheory.ConcreteCategory.hom f) x) : singularChainsCoinvariantsMap k f hf = φ.coinvariantsTensorChainMap (CategoryTheory.CategoryStruct.id (Rep.trivial k G k)) (singularChainsRepResMap k f hf)

The map on coinvariant singular chains is the change-of-groups map on tensor coinvariants induced by the equivariant pushforward of chains, with the identity on the trivial coefficients k.