Classifying spaces of discrete groups

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremUniqueness of aspherical spaces of CW type#

Two aspherical spaces of CW type are homotopy equivalent by a homotopy equivalence realizing any prescribed isomorphism φ of their fundamental groups: there is a homotopy equivalence e and a path γ from e x to y such that the map induced by e on fundamental groups, followed by basepoint change along γ, is φ.

The hypothesis of CW type on both spaces cannot be dropped: a point and the Warsaw circle are aspherical with trivial fundamental groups, but they are not homotopy equivalent.

TauCeti.IsAspherical.exists_homotopyEquiv.{u} {X Y : Type u} [TopologicalSpace X]
  [TopologicalSpace Y] [TauCeti.CWType X] [TauCeti.CWType Y] {x : X} {y : Y}
  (hX : TauCeti.IsAspherical X x) (hY : TauCeti.IsAspherical Y y)
  (φ : FundamentalGroup X x ≃* FundamentalGroup Y y) :
  ∃ e γ,
    ∀ (a : FundamentalGroup X x),
      (FundamentalGroup.fundamentalGroupMulEquivOfPath γ) ((FundamentalGroup.map e.toFun x) a) = φ a

Lean

Formalized in Tau Ceti as TauCeti.IsAspherical.exists_homotopyEquiv.

Sources

• Tau Ceti documentation: TauCeti.IsAspherical.exists_homotopyEquiv
• Source of TauCeti.IsAspherical.exists_homotopyEquiv in TauCeti/AlgebraicTopology/ClassifyingSpace/Uniqueness.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.IsAspherical.exists_homotopyEquiv

Uses 5

Proof usesThe cellular and the simplicial classifying spaces agree · The cellular classifying space is a CW complex · The isomorphism π₁(S¹) ≃* ℤ is the degree · The Seifert--van Kampen theorem for a family with a common pairwise intersection · Whitehead's theorem (Hatcher, Theorem 4.5)

DefinitionThe cellular and the simplicial classifying spaces agree#

For a presentation e : PresentedGroup R ≃* G of G, this is a homotopy equivalence from the cellular classifying space cellularClassifyingSpace R to Milnor's classifying space classifyingSpace G. Its forward map is pointed, induces e under the identifications of both fundamental groups (TauCeti.classifyingSpaceFundamentalGroupMulEquiv_mapOfEq_cellularHomotopyEquivClassifyingSpace), and is unique up to pointed homotopy (TauCeti.homotopicRel_cellularHomotopyEquivClassifyingSpace_toFun). Its homotopy inverse induces e⁻¹ up to a change of base point (TauCeti.exists_path_map_cellularHomotopyEquivClassifyingSpace_invFun).

TauCeti.cellularHomotopyEquivClassifyingSpace.{u} {S : Type u} (R : Set (FreeGroup S)) {G : Type u}
  [Group G] (e : PresentedGroup R ≃* G) :
  ContinuousMap.HomotopyEquiv (↑(TauCeti.cellularClassifyingSpace R)) (TauCeti.classifyingSpace G)

Lean

Formalized in Tau Ceti as TauCeti.cellularHomotopyEquivClassifyingSpace.

Sources

• Tau Ceti documentation: TauCeti.cellularHomotopyEquivClassifyingSpace
• Source of TauCeti.cellularHomotopyEquivClassifyingSpace in TauCeti/AlgebraicTopology/ClassifyingSpace/Comparison.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.cellularHomotopyEquivClassifyingSpace

Uses 6 · Used by 1

Statement usesWhitehead's theorem (Hatcher, Theorem 4.5)

Proof usesThe cellular classifying space is a CW complex · The fundamental group at x acts on every homotopy group based at x · The isomorphism π₁(S¹) ≃* ℤ is the degree · The orbit space of a free cellular action is a CW complex · The Seifert--van Kampen theorem for a family with a common pairwise intersection

Used byUniqueness of aspherical spaces of CW type

TheoremEvery group has a K(G, 1)#

Every group has a K(G, 1), in its own universe, satisfying the standing hypotheses of covering-space theory: local path-connectedness and semilocal simple connectivity. No hypothesis on the group is needed.

TauCeti.exists_isEilenbergMacLaneSpaceOne.{u} (G : Type u) [Group G] :
  ∃ X x x_1,
    LocallyPathConnectedSpace X ∧
      TauCeti.SemilocallySimplyConnectedSpace X ∧ TauCeti.IsEilenbergMacLaneSpaceOne G X x_1

Lean

Formalized in Tau Ceti as TauCeti.exists_isEilenbergMacLaneSpaceOne.

Sources

• Tau Ceti documentation: TauCeti.exists_isEilenbergMacLaneSpaceOne
• Source of TauCeti.exists_isEilenbergMacLaneSpaceOne in TauCeti/AlgebraicTopology/ClassifyingSpace/EilenbergMacLane.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.exists_isEilenbergMacLaneSpaceOne

Uses 1

Proof usesThe fundamental group at x acts on every homotopy group based at x

DefinitionThe singular homology of the classifying space is group homology#

for every group G, the singular homology Hₙ(BG; k) of Milnor's classifying space with coefficients in a commutative ring k is Mathlib's group homology Hₙ(G, k) of the trivial representation. It comes from the free resolution of k by the singular chains of universalGSpace G.

TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology.{u} (k : Type u) [CommRing k] (G : Type u)
  [Group G] (n : ℕ) :
  HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧(TauCeti.classifyingSpace G)) n ≅
    groupHomology (Rep.trivial k G k) n

Lean

Formalized in Tau Ceti as TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology.

Sources

• Tau Ceti documentation: TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology
• Source of TauCeti.classifyingSpaceSingularHomologyIsoGroupHomology in TauCeti/AlgebraicTopology/ClassifyingSpace/Homology.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.classifyingSpaceSingularHomologyIsoGroupHomology

Uses 3

Statement usesThe singular chains of a contractible free G-space are a projective resolution of the trivial representation of G over k

Proof usesThe fundamental group at x acts on every homotopy group based at x · Whitehead's theorem (Hatcher, Theorem 4.5)

DefinitionThe singular cohomology of the classifying space is group cohomology#

for every group G, the singular cohomology Hⁿ(BG; M) of Milnor's classifying space with coefficients in a module M over a commutative ring k is Mathlib's group cohomology Hⁿ(G, M) of the trivial representation M. It comes from the free resolution of k by the singular chains of universalGSpace G.

TauCeti.classifyingSpaceSingularCohomologyIsoGroupCohomology.{u} (k : Type u) [CommRing k]
  (G : Type u) [Group G] (M : Type u) [AddCommGroup M] [_root_.Module k M] (n : ℕ) :
  TopCat.singularCohomology (↧k) k (↧M) (↧(TauCeti.classifyingSpace G)) n ≅
    groupCohomology (Rep.trivial k G M) n

Lean

Formalized in Tau Ceti as TauCeti.classifyingSpaceSingularCohomologyIsoGroupCohomology.

Sources

• Tau Ceti documentation: TauCeti.classifyingSpaceSingularCohomologyIsoGroupCohomology
• Source of TauCeti.classifyingSpaceSingularCohomologyIsoGroupCohomology in TauCeti/AlgebraicTopology/ClassifyingSpace/Cohomology.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.classifyingSpaceSingularCohomologyIsoGroupCohomology

Uses 3

Statement usesThe singular chains of a contractible free G-space are a projective resolution of the trivial representation of G over k

Proof usesThe fundamental group at x acts on every homotopy group based at x · Whitehead's theorem (Hatcher, Theorem 4.5)

DefinitionMilnor's join resolution is homotopy equivalent to the standard resolution#

Milnor's join resolution is homotopy equivalent to the standard resolution, by a homotopy equivalence whose forward map is the explicit join-to-standard chain map. Its homotopy inverse is the lift of the identity of the trivial representation from the standard resolution to the join resolution.

TauCeti.universalGSpaceStandardHomotopyEquiv.{u} (k : Type u) [CommRing k] (G : Type u) [Group G] :
  HomotopyEquiv (TauCeti.universalGSpaceChainComplex k G) (Rep.standardComplex k G)

Lean

Formalized in Tau Ceti as TauCeti.universalGSpaceStandardHomotopyEquiv.

Sources

• Tau Ceti documentation: TauCeti.universalGSpaceStandardHomotopyEquiv
• Source of TauCeti.universalGSpaceStandardHomotopyEquiv in TauCeti/AlgebraicTopology/ClassifyingSpace/StandardResolution.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.universalGSpaceStandardHomotopyEquiv

TheoremThe join-to-standard comparison is natural in the group#

Relabelling simplices before forgetting their indices agrees with first forgetting indices and then relabelling the tuples. This is an equality of chain maps in Rep k G, with target actions restricted along φ.

MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality.{u} {k G H : Type u} [Group G]
  [Group H] [CommRing k] (φ : G →* H) :
  CategoryTheory.CategoryStruct.comp φ.universalGSpaceChainMap
      (((Rep.resFunctor φ).mapHomologicalComplex (ComplexShape.down ℕ)).map
        (TauCeti.universalGSpaceChainComplexToStandardComplex k H)) =
    CategoryTheory.CategoryStruct.comp (TauCeti.universalGSpaceChainComplexToStandardComplex k G)
      φ.standardComplexMap

Lean

Formalized in Tau Ceti as MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality.

Sources

• Tau Ceti documentation: MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality
• Source of MonoidHom.universalGSpaceChainComplexToStandardComplex_naturality in TauCeti/AlgebraicTopology/ClassifyingSpace/Naturality.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanMonoidHom.universalGSpaceChainComplexToStandardComplex_naturality

InstanceThe cellular classifying space is a CW complex#

Its cells are those of the presentation complex, one 0-cell, one 1-cell for each generator and one 2-cell for each relator, together with the cells of dimension at least 3 attached to kill the higher homotopy groups (TauCeti.killHomotopyGroupsCWComplexCellEquiv).

TauCeti.instCWComplexCellularClassifyingSpace.{u} {S : Type u} (R : Set (FreeGroup S)) :
  Topology.CWComplex Set.univ

Lean

Formalized in Tau Ceti as TauCeti.instCWComplexCellularClassifyingSpace.

Sources

• Tau Ceti documentation: TauCeti.instCWComplexCellularClassifyingSpace
• Source of TauCeti.instCWComplexCellularClassifyingSpace in TauCeti/AlgebraicTopology/ClassifyingSpace/Cellular.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.instCWComplexCellularClassifyingSpace

Uses 1 · Used by 2

Proof usesThe Seifert--van Kampen theorem for a family with a common pairwise intersection

Used byThe cellular and the simplicial classifying spaces agree · Uniqueness of aspherical spaces of CW type

DefinitionA CW structure lifts along a covering map#

If C is a CW complex in the Hausdorff space B and p : E → B is a covering map, then p ⁻¹' C is a CW complex in E. Its n-cells are the pairs of an n-cell of C and a point of E over the centre of that cell (TauCeti.cellPreimageEquiv); the characteristic map of such a pair is the lift of the characteristic map of the cell through p sending the centre to the chosen point.

TauCeti.cwComplexPreimage.{u} {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B)
  [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) :
  Topology.CWComplex (p ⁻¹' C)

Lean

Formalized in Tau Ceti as TauCeti.cwComplexPreimage.

Sources

• Tau Ceti documentation: TauCeti.cwComplexPreimage
• Source of TauCeti.cwComplexPreimage in TauCeti/Topology/CWComplex/Classical/Covering.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.cwComplexPreimage

Used by 1

Used byThe cellular chains of a contractible free cover are a projective resolution of the trivial representation of G over R

DefinitionThe orbit space of a free cellular action is a CW complex#

Let p : E → B be the quotient covering map of an action of G on the Hausdorff CW complex E that carries every open n-cell onto an open n-cell, and carries an open cell onto itself only by 1. Then B is a CW complex whose n-cells are the G-orbits of n-cells of E (IsQuotientCoveringMap.cellQuotientEquiv). The characteristic map of an orbit is p ∘ φ, for φ the characteristic map of the chosen representative of the orbit (IsQuotientCoveringMap.map_cellQuotientEquiv_symm).

IsQuotientCoveringMap.cwComplexQuotient.{u, u_1} {E : Type u} [TopologicalSpace E] {G : Type u_1}
  {B : Type u} [TopologicalSpace B] [Topology.CWComplex Set.univ] [Group G] [MulAction G E]
  [T2Space E] {p : E → B} (hp : IsQuotientCoveringMap p G)
  (hcell :
    ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n),
      ∃ j, g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n j)
  (hfree :
    ∀ (g : G) (n : ℕ) (i : Topology.RelCWComplex.cell Set.univ n),
      g • Topology.RelCWComplex.openCell n i = Topology.RelCWComplex.openCell n i → g = 1) :
  Topology.CWComplex Set.univ

Lean

Formalized in Tau Ceti as IsQuotientCoveringMap.cwComplexQuotient.

Sources

• Tau Ceti documentation: IsQuotientCoveringMap.cwComplexQuotient
• Source of IsQuotientCoveringMap.cwComplexQuotient in TauCeti/Topology/CWComplex/Classical/OrbitSpace.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanIsQuotientCoveringMap.cwComplexQuotient

Used by 1

Used byThe cellular and the simplicial classifying spaces agree

DefinitionThe cellular chains of a contractible free cover are a projective resolution of the trivial representation of G over R#

if the lift p ⁻¹' C of the CW complex C is contractible, its cellular chain complex, on which G acts through translation of the lifted cells, is a complex of free representations whose augmentation is a quasi-isomorphism.

TauCeti.cellularResolution.{w} {E B : Type w} [TopologicalSpace E] [TopologicalSpace B] {p : E → B}
  (C : Set B) {G : Type w} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [T2Space B]
  [Topology.CWComplex C] (R : Type w) [CommRing R] [ContractibleSpace ↑(p ⁻¹' C)] :
  CategoryTheory.ProjectiveResolution (Rep.trivial R G R)

Lean

Formalized in Tau Ceti as TauCeti.cellularResolution.

Sources

• Tau Ceti documentation: TauCeti.cellularResolution
• Source of TauCeti.cellularResolution in TauCeti/AlgebraicTopology/Cellular/Resolution.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.cellularResolution

Uses 3

Statement usesA CW structure lifts along a covering map

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem

DefinitionThe 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.

TauCeti.singularChainsResolution.{u} (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)

Lean

Formalized in Tau Ceti as TauCeti.singularChainsResolution.

Sources

• Tau Ceti documentation: TauCeti.singularChainsResolution
• Source of TauCeti.singularChainsResolution in TauCeti/AlgebraicTopology/Singular/ModuleChains/Resolution.lean
• Tau Ceti roadmap status: Classifying spaces of discrete groups

LeanTauCeti.singularChainsResolution

Used by 2

Used byThe singular cohomology of the classifying space is group cohomology · The singular homology of the classifying space is group homology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.