The singular chains of a contractible free G-space as a projective resolution

Let a monoid G act on a space E by continuous maps. Pushing singular chains forward along the translations g • · makes each group of singular n-chains of E with coefficients in a commutative ring k a representation of G (TauCeti.singularChainsRepresentation), and the singular boundary is equivariant, so the singular chains form a chain complex of representations (TauCeti.singularChainsRep). Forgetting the action gives back the singular chain complex (TauCeti.singularChainsRepForget₂Iso), and the sum of the coefficients of a 0-chain is an augmentation onto the trivial representation (TauCeti.singularChainsRepAugmentation).

The n-chains are the permutation representation of G on the singular n-simplices (TauCeti.singularChainsEquivOfMulAction). If G is a group acting freely on E, it acts freely on singular simplices, since a simplex is moved off itself already at one point; so each term is a free representation, in particular a projective one (TauCeti.projective_singularChainsRep_X). If E is moreover contractible, the augmented singular chain complex is exact (TauCeti.quasiIso_singularChainsAugmentation), and the singular chains of E are a projective resolution of the trivial representation (TauCeti.singularChainsResolution). For the total space of a free cover with contractible total space, such as the universal cover of a K(G, 1) CW complex, this resolution computes the group homology of G.

Main definitions

• TauCeti.singularChainsRepresentation: the action of G on singular n-chains.
• TauCeti.singularChainsRep: the singular chain complex of E, as a chain complex of representations of G.
• TauCeti.singularChainsRepAugmentation: its augmentation onto the trivial representation.
• TauCeti.singularChainsEquivOfMulAction: the n-chains are the permutation representation on singular n-simplices.
• TauCeti.singularChainsResolution: for a free action on a contractible space, the projective resolution of the trivial representation by the singular chains.

Main results

• TauCeti.projective_singularChainsRep_X: for a free action, the terms are projective.
• TauCeti.quasiIso_singularChainsRepAugmentation: for contractible E, the augmentation is a quasi-isomorphism.

References

• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Section I.4 and Section II.4.

noncomputable def TauCeti.singularChainsRepresentation (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : Representation k G ↑(((singularChains k).obj E).X n)

The action of G on the singular n-chains of a G-space E: g acts by pushing chains forward along the translation g • ·.

theorem TauCeti.singularChainsRepresentation_apply {k : Type u} [CommRing k] {E : TopCat} {G : Type u} [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) (g : G) : (singularChainsRepresentation k E G n) g = ModuleCat.Hom.hom (((singularChains k).map (TopCat.ofHom { toFun := fun (x : ↑E) => g • x, continuous_toFun := ⋯ })).f n)

An element g acts on singular n-chains by the chain map of the translation g • ·.

@[simp]

theorem TauCeti.singularChainsRepresentation_simplexChain {k : Type u} [CommRing k] {E : TopCat} {G : Type u} [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] {n : ℕ} (g : G) (σ : (TopCat.toSSet.obj E).obj (Opposite.op { len := n })) (a : k) : ((singularChainsRepresentation k E G n) g) (simplexChain σ a) = simplexChain (g • σ) a

An element g sends the chain of a simplex σ to the chain of the translated simplex g • σ.

noncomputable def TauCeti.singularChainsRepDifferential (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : Rep.of (singularChainsRepresentation k E G (n + 1)) ⟶ Rep.of (singularChainsRepresentation k E G n)

The singular boundary is G-equivariant, so it is a morphism of representations.

@[simp]

theorem TauCeti.singularChainsRepDifferential_hom_apply (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) (c : ↑(((singularChains k).obj E).X (n + 1))) : (Rep.Hom.hom (singularChainsRepDifferential k E G n)) c = (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj E).d (n + 1) n)) c

The equivariant singular boundary is the singular boundary.

noncomputable def TauCeti.singularChainsRep (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : ChainComplex (Rep k G) ℕ

The singular chains of a G-space as a chain complex of representations of G: in degree n it is the representation TauCeti.singularChainsRepresentation on the singular n-chains, and its differential is the singular boundary.

@[simp]

theorem TauCeti.singularChainsRep_X (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : (singularChainsRep k E G).X n = Rep.of (singularChainsRepresentation k E G n)

The terms of the equivariant singular chain complex are the representations TauCeti.singularChainsRepresentation.

@[simp]

theorem TauCeti.singularChainsRep_d (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : (singularChainsRep k E G).d (n + 1) n = singularChainsRepDifferential k E G n

The differentials of the equivariant singular chain complex are the singular boundaries.

noncomputable def TauCeti.singularChainsRepForget₂Iso (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).obj (singularChainsRep k E G) ≅ (singularChains k).obj E

Forgetting the action of G, the equivariant singular chain complex is the singular chain complex of E: the components of this isomorphism are identities.

@[simp]

theorem TauCeti.singularChainsRepForget₂Iso_hom_f (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : (singularChainsRepForget₂Iso k E G).hom.f n = CategoryTheory.CategoryStruct.id ((((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).obj (singularChainsRep k E G)).X n)

The components of TauCeti.singularChainsRepForget₂Iso are identities.

noncomputable def TauCeti.singularAugmentRep (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : Rep.of (singularChainsRepresentation k E G 0) ⟶ Rep.trivial k G k

The augmentation of the singular 0-chains of E, the sum of the coefficients, as a morphism to the trivial representation: pushing chains forward preserves the augmentation.

@[simp]

theorem TauCeti.singularAugmentRep_hom_toLinearMap (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : (Rep.Hom.hom (singularAugmentRep k E G)).toLinearMap = singularAugment k E

The underlying linear map of TauCeti.singularAugmentRep is the augmentation.

noncomputable def TauCeti.singularChainsRepAugmentation (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : singularChainsRep k E G ⟶ (ChainComplex.single₀ (Rep k G)).obj (Rep.trivial k G k)

The augmentation of the equivariant singular chains: the chain map to the trivial representation, placed in degree 0, that sums the coefficients of a 0-chain.

@[simp]

theorem TauCeti.singularChainsRepAugmentation_f_zero (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] : (singularChainsRepAugmentation k E G).f 0 = singularAugmentRep k E G

In degree 0 the equivariant augmentation is TauCeti.singularAugmentRep.

instance TauCeti.quasiIso_singularChainsRepAugmentation (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] [ContractibleSpace ↑E] : QuasiIso (singularChainsRepAugmentation k E G)

The augmented singular chain complex of a contractible G-space is exact: forgetting the action, the augmentation is that of the singular chains of E.

noncomputable def TauCeti.singularChainsEquivOfMulAction (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Monoid G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] (n : ℕ) : (singularChainsRepresentation k E G n).Equiv (Representation.ofMulAction k G ((TopCat.toSSet.obj E).obj (Opposite.op { len := n })))

The singular n-chains are the permutation representation on singular n-simplices: the chain of a simplex σ with coefficient a corresponds to a times the basis vector of σ, and G acts on simplices by translation (TauCeti.TopCat.mulActionToSSetObj).

instance TauCeti.projective_singularChainsRep_X (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Group G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] [IsCancelSMul G ↑E] (n : ℕ) : CategoryTheory.Projective ((singularChainsRep k E G).X n)

The singular chains of a free G-space are free representations: each term of the equivariant singular chain complex is the permutation representation of a free action, on the singular simplices (TauCeti.TopCat.isCancelSMul_toSSetObj), and so it is projective.

noncomputable def TauCeti.singularChainsResolution (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Group G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] [IsCancelSMul G ↑E] [ContractibleSpace ↑E] : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)

The singular chains of a contractible free G-space are a projective resolution of the trivial representation of G over k: G acts freely on singular simplices, so the terms are free over the group ring, and the augmented singular chain complex of a contractible space is exact.

@[simp]

theorem TauCeti.singularChainsResolution_complex (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Group G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] [IsCancelSMul G ↑E] [ContractibleSpace ↑E] : (singularChainsResolution k E G).complex = singularChainsRep k E G

The complex of TauCeti.singularChainsResolution is the equivariant singular chain complex.

@[simp]

theorem TauCeti.singularChainsResolution_π (k : Type u) [CommRing k] (E : TopCat) (G : Type u) [Group G] [MulAction G ↑E] [ContinuousConstSMul G ↑E] [IsCancelSMul G ↑E] [ContractibleSpace ↑E] : (singularChainsResolution k E G).π = singularChainsRepAugmentation k E G

The augmentation of TauCeti.singularChainsResolution is that of the equivariant singular chains.