The ordered chains of Milnor's countable join as a projective resolution

A group G acts on the simplices of the countable join indexedJoin fun _ : ℕ => G by translating the labels of their vertices, and this action commutes with taking faces (TauCeti.face_smul_universalGSpace). So the ordered simplicial chains of the countable join, indexed by the cells of universalGSpace G and oriented by increasing index as its CW structure is, form a chain complex of permutation representations of G (TauCeti.universalGSpaceChainComplex). Forgetting the action gives back the ordered simplicial chain complex (TauCeti.universalGSpaceChainComplexForget₂Iso).

The action on simplices is free, so each term is a free representation, with basis one simplex in each orbit (TauCeti.ofMulActionIsoFree), and in particular projective. The sum of the coefficients of a 0-chain is an augmentation onto the trivial representation (TauCeti.universalGSpaceAugmentation), and it is a quasi-isomorphism because the augmented ordered chain complex of the countable join is exact (TauCeti.quasiIso_orderedSimplicialChainComplexAugmentation_indexedJoin). Together these make the ordered chains of the countable join a projective resolution of the trivial representation (TauCeti.universalGSpaceResolution). It is the topological counterpart of Mathlib's standard resolution Rep.standardResolution; on underlying complexes of modules, TauCeti.universalGSpaceToStandardComplex maps the former to the latter.

Main definitions

• TauCeti.universalGSpaceChainComplex: the ordered chain complex of the countable join, as a chain complex of permutation representations of G.
• TauCeti.universalGSpaceAugmentation: its augmentation onto the trivial representation.
• TauCeti.universalGSpaceResolution: the resulting projective resolution of the trivial representation.

Main results

• TauCeti.universalGSpaceChainComplexForget₂Iso: forgetting the action gives the ordered simplicial chain complex of the countable join.
• TauCeti.quasiIso_universalGSpaceAugmentation: the augmentation is a quasi-isomorphism.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• K. S. Brown, Cohomology of Groups, GTM 87, Springer, 1982, Chapter I, Sections 4 and 5.

noncomputable def TauCeti.universalGSpaceBoundary (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : Rep.ofMulAction k G ((indexedJoin fun (x : ℕ) => G).RealizationCell (n + 1)) ⟶ Rep.ofMulAction k G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

The ordered simplicial boundary of the countable join, as a morphism between the permutation representations of G on its simplices of consecutive dimensions.

@[simp]

theorem TauCeti.universalGSpaceBoundary_hom_single (k : Type u) [Ring k] (G : Type u) [Group G] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell (n + 1)) (a : k) : (Rep.Hom.hom (universalGSpaceBoundary k G n)) (MonoidAlgebra.single c a) = ∑ j : Fin (n + 2), (-1) ^ ↑j • MonoidAlgebra.single (c.face j) a

The boundary of a simplex is the alternating sum of its faces.

theorem TauCeti.universalGSpaceBoundary_comp_coeff (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (universalGSpaceBoundary k G n)) (MonoidAlgebra.coeffLinearEquiv k).toModuleIso.hom = CategoryTheory.CategoryStruct.comp (MonoidAlgebra.coeffLinearEquiv k).toModuleIso.hom (ModuleCat.ofHom (OrderedSimplicialChain.boundary k n))

Read on coefficients, the equivariant boundary is the ordered simplicial boundary.

noncomputable def TauCeti.universalGSpaceChainComplex (k : Type u) [Ring k] (G : Type u) [Group G] : ChainComplex (Rep k G) ℕ

The ordered chains of the countable join as a complex of representations. In degree n it is the permutation representation of G on the n-simplices of the countable join, which are the n-cells of universalGSpace G, and its differential is the alternating simplicial boundary.

@[simp]

theorem TauCeti.universalGSpaceChainComplex_X (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : (universalGSpaceChainComplex k G).X n = Rep.ofMulAction k G ((indexedJoin fun (x : ℕ) => G).RealizationCell n)

In degree n the complex is the permutation representation on the n-simplices.

@[simp]

theorem TauCeti.universalGSpaceChainComplex_d (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : (universalGSpaceChainComplex k G).d (n + 1) n = universalGSpaceBoundary k G n

The differential of the complex is the equivariant simplicial boundary.

noncomputable def TauCeti.universalGSpaceChainComplexForget₂Iso (k : Type u) [Ring k] (G : Type u) [Group G] : ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).obj (universalGSpaceChainComplex k G) ≅ orderedSimplicialChainComplex (indexedJoin fun (x : ℕ) => G) k

Forgetting the action gives the ordered simplicial chain complex of the countable join; in each degree the isomorphism reads a vector of the permutation representation as its coefficients.

@[simp]

theorem TauCeti.universalGSpaceChainComplexForget₂Iso_hom_f (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : (universalGSpaceChainComplexForget₂Iso k G).hom.f n = CategoryTheory.CategoryStruct.comp (MonoidAlgebra.coeffLinearEquiv k).toModuleIso.hom (CategoryTheory.eqToHom ⋯)

In each degree the isomorphism reads a vector as its coefficients.

@[simp]

theorem TauCeti.universalGSpaceChainComplexForget₂Iso_inv_f (k : Type u) [Ring k] (G : Type u) [Group G] (n : ℕ) : (universalGSpaceChainComplexForget₂Iso k G).inv.f n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (MonoidAlgebra.coeffLinearEquiv k).toModuleIso.inv

In each degree the inverse comparison reconstructs a permutation vector from its coefficients.

noncomputable def TauCeti.universalGSpaceAugmentation (k : Type u) [Ring k] (G : Type u) [Group G] : universalGSpaceChainComplex k G ⟶ (ChainComplex.single₀ (Rep k G)).obj (Rep.trivial k G k)

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

@[simp]

theorem TauCeti.universalGSpaceAugmentation_f_zero (k : Type u) [Ring k] (G : Type u) [Group G] : (universalGSpaceAugmentation k G).f 0 = permutationAugmentation k G ((indexedJoin fun (x : ℕ) => G).RealizationCell 0)

In degree 0 the augmentation sums the coefficients.

instance TauCeti.quasiIso_universalGSpaceAugmentation (k : Type u) [Ring k] (G : Type u) [Group G] : QuasiIso (universalGSpaceAugmentation k G)

The augmentation of the countable join is a quasi-isomorphism: forgetting the action, it is the augmentation of the ordered simplicial chain complex.

noncomputable def TauCeti.universalGSpaceResolution (k : Type u) [CommRing k] (G : Type u) [Group G] : CategoryTheory.ProjectiveResolution (Rep.trivial k G k)

The ordered chains of Milnor's countable join are a projective resolution of the trivial representation of G: the terms are free over the group ring, because G acts freely on the simplices, and the augmentation is a quasi-isomorphism.

@[simp]

theorem TauCeti.universalGSpaceResolution_complex (k : Type u) [CommRing k] (G : Type u) [Group G] : (universalGSpaceResolution k G).complex = universalGSpaceChainComplex k G

The complex of the resolution is the ordered chain complex of the countable join.

@[simp]

theorem TauCeti.universalGSpaceResolution_π (k : Type u) [CommRing k] (G : Type u) [Group G] : (universalGSpaceResolution k G).π = universalGSpaceAugmentation k G

The augmentation of the resolution sums the coefficients of a 0-chain.