Singular chains of a quotient covering are coinvariants

Let a group G act on a space E so that p : E ⟶ B is the quotient covering map of the action, in the sense of Mathlib's IsQuotientCoveringMap. The action is the functor E.actionFunctor G : SingleObj G ⥤ TopCat sending the unique object to E, and p is a cocone hG.cocone over it. This file shows that the singular simplicial set, and the singular chain complex with any coefficients, of B are the coinvariants of those of E:

• IsQuotientCoveringMap.isColimitMapCoconeToSSet: the singular simplicial set of B is the quotient of that of E by G: every singular simplex of B lifts to E, and any two lifts of the same simplex differ by an element of G (IsQuotientCoveringMap.toSSet_map_app_surjective and IsQuotientCoveringMap.toSSet_map_app_eq_iff).
• IsQuotientCoveringMap.isColimitMapCoconeSingularChainComplex: hence C(B; R) is the colimit C(E; R)_G of the action of G on C(E; R) by the chain maps g_*, for coefficients R in any preadditive category with coproducts, since the simplicial chain complex preserves colimits.

Neither statement needs G to be finite. Taking coinvariants is not exact, so the corresponding statement for homology fails in general. It holds when G is finite and multiplication by |G| is invertible on R: the transfer t of the finite covering p satisfies t ≫ p_* = |G| • 𝟙 and p_* ≫ t = ∑_{g ∈ G} g_*, so the colimit is preserved by every additive functor (CategoryTheory.Limits.SingleObj.isColimitMapCoconeOfTransfer) and in particular survives homology:

• IsQuotientCoveringMap.isColimitMapCoconeSingularHomology: Hₙ(B; R) ≅ Hₙ(E; R)_G through p_* when |G| is invertible on R.

References

• A. Hatcher, Algebraic Topology, Section 3.G (Proposition 3G.1), for the transfer and the averaging argument, stated there for cohomology with field coefficients and invariants; the homology and coinvariant form here is its dual.
• K. S. Brown, Cohomology of Groups, Springer GTM 87, Chapter VII, for the Cartan–Leray spectral sequence, which starts from the identification C(E)_G = C(B).

def IsQuotientCoveringMap.cocone {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) : CategoryTheory.Limits.Cocone (E.actionFunctor G)

The quotient covering map p : E ⟶ B, as a cocone over the action of G on E.

@[simp]

theorem IsQuotientCoveringMap.cocone_pt {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) : hG.cocone.pt = B

@[simp]

theorem IsQuotientCoveringMap.cocone_ι_app {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (x✝ : CategoryTheory.SingleObj G) : hG.cocone.ι.app x✝ = p

noncomputable def IsQuotientCoveringMap.isColimitMapCoconeToSSet {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) : CategoryTheory.Limits.IsColimit (TopCat.toSSet.mapCocone hG.cocone)

The singular simplicial set of the base of a quotient covering is the quotient of that of the total space. For the quotient covering map p : E ⟶ B of an action of a group G, the singular simplicial set of B is the colimit of the action of G on the singular simplicial set of E, with legs p_*.

theorem IsQuotientCoveringMap.toSSet_map_app_surjective {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) (n : SimplexCategoryᵒᵖ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n))

Every singular simplex of the base of a quotient covering lifts to the total space.

theorem IsQuotientCoveringMap.toSSet_map_app_eq_iff {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) {n : SimplexCategoryᵒᵖ} (σ σ' : (TopCat.toSSet.obj E).obj n) : (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) σ = (CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map p).app n)) σ' ↔ ∃ (g : G), g • σ' = σ

Two lifts of a singular simplex of the base of a quotient covering differ by an element of G: two singular simplices of the total space have the same image in the base exactly when one is a translate of the other.

noncomputable def IsQuotientCoveringMap.isColimitMapCoconeSingularChainComplex {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) : CategoryTheory.Limits.IsColimit (((AlgebraicTopology.singularChainComplexFunctor C).obj R).mapCocone hG.cocone)

The singular chains of the base of a quotient covering are coinvariants. For the quotient covering map p : E ⟶ B of an action of a group G, the singular chain complex C(B; R) is the colimit C(E; R)_G of the action of G on C(E; R) by the chain maps g_*, with legs p_*.

noncomputable def IsQuotientCoveringMap.isColimitMapCoconeSingularHomology {E B : TopCat} {p : E ⟶ B} {G : Type u_1} [Group G] [MulAction G ↑E] (hG : IsQuotientCoveringMap (⇑(CategoryTheory.ConcreteCategory.hom p)) G) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) [Fintype G] [CategoryTheory.CategoryWithHomology C] (n : ℕ) [CategoryTheory.IsIso (Fintype.card G • CategoryTheory.CategoryStruct.id R)] : CategoryTheory.Limits.IsColimit (((AlgebraicTopology.singularHomologyFunctor C n).obj R).mapCocone hG.cocone)

The singular homology of the base of a finite quotient covering is coinvariants. For the quotient covering map p : E ⟶ B of an action of a finite group G, and coefficients R on which multiplication by |G| is invertible, Hₙ(B; R) is the colimit Hₙ(E; R)_G of the action of G on Hₙ(E; R), with legs p_*.