From Milnor's join chains to the standard complex

An oriented simplex of Milnor's countable join has vertices (i₀, g₀), …, (iₙ, gₙ) with strictly increasing indices. Forgetting the indices gives the basis element (g₀, …, gₙ) of Mathlib's Rep.standardComplex. Deleting a vertex commutes with forgetting its index, so this prescription defines a chain map.

TauCeti.universalGSpaceToStandardComplex has as source the existing ordered simplicial chain complex of the countable join and as target the underlying module complex of Mathlib's standard complex. Its degreewise maps are equivariant for translation and preserve the augmentations. This is an explicit comparison of complexes of modules; its equivariant form, a homotopy equivalence of projective resolutions, is in TauCeti.AlgebraicTopology.ClassifyingSpace.StandardResolution. For a nonzero coefficient ring it is not an isomorphism: even for the trivial group, the join has countably many vertices and the standard complex has just one.

The source orientation agrees with the CW structure on universalGSpace: its characteristic maps enumerate the vertices by increasing index. The target is Mathlib's standard complex from Mathlib.RepresentationTheory.Homological.Resolution, by Amelia Livingston, not a new version of the bar resolution.

References

• J. Milnor, Construction of universal bundles, II, Ann. of Math. 63 (1956), 430--436.
• K. S. Brown, Cohomology of Groups, Springer, 1982, Chapters I and III.

noncomputable def TauCeti.universalGSpaceCellLabels {G : Type u} {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : Fin (n + 1) → G

The labels of an oriented simplex of the countable join, enumerated by increasing index.

@[simp]

theorem TauCeti.universalGSpaceCellLabels_apply {G : Type u} {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (j : Fin (n + 1)) : universalGSpaceCellLabels c j = (c.vertexEmbedding j).snd

The entry at a given position is the label of the vertex at that position.

@[simp]

theorem TauCeti.universalGSpaceCellLabels_face {G : Type u} {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell (n + 1)) (j : Fin (n + 2)) : universalGSpaceCellLabels (c.face j) = universalGSpaceCellLabels c ∘ j.succAbove

Deleting a vertex deletes the corresponding entry of the label tuple.

@[simp]

theorem TauCeti.universalGSpaceCellLabels_smul {G : Type u} [Group G] {n : ℕ} (g : G) (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) : universalGSpaceCellLabels (g • c) = g • universalGSpaceCellLabels c

Translation of a simplex translates its entire label tuple diagonally.

noncomputable def TauCeti.universalGSpaceToStandard {G : Type u} (k : Type v) [Semiring k] (n : ℕ) : OrderedSimplicialChain (indexedJoin fun (x : ℕ) => G) k n →ₗ[k] MonoidAlgebra k (Fin (n + 1) → G)

The degreewise comparison from join chains to standard chains: forget the indices of vertices, retaining their increasing-index order and the coefficient of each simplex.

@[simp]

theorem TauCeti.universalGSpaceToStandard_single {G : Type u} (k : Type v) [Semiring k] {n : ℕ} (c : (indexedJoin fun (x : ℕ) => G).RealizationCell n) (a : k) : (universalGSpaceToStandard k n) (Finsupp.single c a) = MonoidAlgebra.single (universalGSpaceCellLabels c) a

The comparison sends an individual simplex to its ordered tuple of labels.

theorem TauCeti.universalGSpaceToStandard_smul {G : Type u} (k : Type v) [Semiring k] [Group G] (n : ℕ) (g : G) (x : OrderedSimplicialChain (indexedJoin fun (x : ℕ) => G) k n) : (universalGSpaceToStandard k n) ((Finsupp.lmapDomain k k fun (x : (indexedJoin fun (x : ℕ) => G).RealizationCell n) => g • x) x) = ((Representation.ofMulAction k G (Fin (n + 1) → G)) g) ((universalGSpaceToStandard k n) x)

The comparison is equivariant: translating every simplex before forgetting its indices is the diagonal translation of the resulting standard chain. The source action is the linear extension of the action on the simplices.

theorem TauCeti.universalGSpaceToStandard_boundary {G : Type u} (k : Type u) [CommRing k] (n : ℕ) : universalGSpaceToStandard k n ∘ₗ OrderedSimplicialChain.boundary k n = Rep.standardComplex.d k G (n + 1) ∘ₗ universalGSpaceToStandard k (n + 1)

The explicit comparison commutes with the alternating boundaries.

noncomputable def TauCeti.universalGSpaceToStandardComplex {G : Type u} (k : Type u) [CommRing k] [Monoid G] : orderedSimplicialChainComplex (indexedJoin fun (x : ℕ) => G) k ⟶ Rep.standardComplex.forget₂ToModuleCat k G

The explicit join-to-standard chain map. Its source is the ordered simplicial chain complex of the countable join, and its target is the module complex underlying Mathlib's standard complex.

@[simp]

theorem TauCeti.universalGSpaceToStandardComplex_f {G : Type u} (k : Type u) [CommRing k] [Monoid G] (n : ℕ) : (universalGSpaceToStandardComplex k).f n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (universalGSpaceToStandard k n)) ((CategoryTheory.forget₂ (Rep k G) (ModuleCat k)).map (Rep.standardComplex.xIso k G n).inv))

In each degree the chain map is the explicit comparison on simplex coefficients.

theorem TauCeti.universalGSpaceToStandard_augmentation {G : Type u} (k : Type u) [CommRing k] [Monoid G] (x : OrderedSimplicialChain (indexedJoin fun (x : ℕ) => G) k 0) : (Rep.Hom.hom (Rep.standardComplex.ε k G)) ((universalGSpaceToStandard k 0) x) = (Finsupp.linearCombination k fun (x : (indexedJoin fun (x : ℕ) => G).RealizationCell 0) => 1) x

The comparison preserves the augmentations, each of which sums the coefficients of the vertices. The target augmentation is Rep.standardComplex.ε.