Aspherical spaces and Eilenberg--Mac Lane spaces of type K(G, 1)

A based space is aspherical when it is path-connected and all of its homotopy groups in dimensions at least two are trivial. An Eilenberg--Mac Lane space of type K(G, 1) is an aspherical space whose fundamental group is isomorphic to G.

The definitions are properties rather than structures carrying chosen isomorphisms. Thus they are invariant under changing an exhibited fundamental-group isomorphism, and do not retain noncanonical data. This file records independence of the base point, invariance under isomorphism of the target group, as well as closure under binary and indexed products. Invariance under homotopy equivalence, and so in particular under homeomorphism, is in TauCeti.AlgebraicTopology.EilenbergMacLane.HomotopyEquiv.

The product results reuse the existing product isomorphisms for fundamental and higher homotopy groups.

This implements the general API for TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, "K(G, 1) spaces". Concrete circle and torus examples are respectively in TauCeti.AlgebraicTopology.UniversalCover.Circle.EilenbergMacLane and TauCeti.AlgebraicTopology.UniversalCover.Torus.EilenbergMacLane.

Main declarations

• TauCeti.IsAspherical: path-connectedness together with vanishing homotopy groups in dimensions at least two.
• TauCeti.IsEilenbergMacLaneSpaceOne: the property of being an Eilenberg--Mac Lane space of type K(G, 1).
• TauCeti.IsAspherical.of_basepoint, TauCeti.IsEilenbergMacLaneSpaceOne.of_basepoint: neither property depends on the base point.
• TauCeti.IsAspherical.prod, TauCeti.IsAspherical.pi, TauCeti.IsEilenbergMacLaneSpaceOne.prod, TauCeti.IsEilenbergMacLaneSpaceOne.pi: closure under products.

def TauCeti.IsAspherical (X : Type u) [TopologicalSpace X] (x : X) : Prop

A based space is aspherical when it is path-connected and every homotopy group in dimension at least two is trivial.

Equations

• TauCeti.IsAspherical X x = (PathConnectedSpace X ∧ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x))

theorem TauCeti.isAspherical_iff {X : Type u} [TopologicalSpace X] {x : X} : IsAspherical X x ↔ PathConnectedSpace X ∧ ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)

Characteristic restatement of asphericity.

theorem TauCeti.IsAspherical.mk {X : Type u} [TopologicalSpace X] {x : X} (hX : PathConnectedSpace X) (hπ : ∀ (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) X x)) : IsAspherical X x

Construct asphericity from path-connectedness and the vanishing of all homotopy groups in dimensions at least two.

theorem TauCeti.IsAspherical.pathConnectedSpace {X : Type u} [TopologicalSpace X] {x : X} (h : IsAspherical X x) : PathConnectedSpace X

An aspherical space is path-connected.

theorem TauCeti.IsAspherical.subsingleton_homotopyGroup {X : Type u} [TopologicalSpace X] {x : X} (h : IsAspherical X x) (n : ℕ) : Subsingleton (HomotopyGroup.Pi (n + 2) X x)

Every homotopy group of an aspherical space in dimension at least two is trivial.

theorem TauCeti.IsAspherical.of_basepoint {X : Type u} [TopologicalSpace X] {x : X} (h : IsAspherical X x) (x' : X) : IsAspherical X x'

Asphericity does not depend on the base point. An aspherical space is path connected, so its homotopy groups at any two points are isomorphic.

theorem TauCeti.IsAspherical.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} (hX : IsAspherical X x) (hY : IsAspherical Y y) : IsAspherical (X × Y) (x, y)

The product of two aspherical spaces is aspherical.

theorem TauCeti.IsAspherical.pi {ι : Type w} {Z : ι → Type u} [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (h : ∀ (i : ι), IsAspherical (Z i) (z i)) : IsAspherical ((i : ι) → Z i) z

An indexed product of aspherical spaces is aspherical.

def TauCeti.IsEilenbergMacLaneSpaceOne (G : Type u) [Group G] (X : Type v) [TopologicalSpace X] (x : X) : Prop

A based space is an Eilenberg--Mac Lane space of type K(G, 1) when it is aspherical and its fundamental group is isomorphic to G.

Equations

• TauCeti.IsEilenbergMacLaneSpaceOne G X x = (TauCeti.IsAspherical X x ∧ Nonempty (FundamentalGroup X x ≃* G))

theorem TauCeti.isEilenbergMacLaneSpaceOne_iff {G : Type u} [Group G] {X : Type v} [TopologicalSpace X] {x : X} : IsEilenbergMacLaneSpaceOne G X x ↔ IsAspherical X x ∧ Nonempty (FundamentalGroup X x ≃* G)

Characteristic restatement of the K(G, 1) property.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.mk {G : Type u} [Group G] {X : Type w} [TopologicalSpace X] {x : X} (hX : IsAspherical X x) (hπ : Nonempty (FundamentalGroup X x ≃* G)) : IsEilenbergMacLaneSpaceOne G X x

Construct the K(G, 1) property from asphericity and an isomorphism between the fundamental group and G.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.isAspherical {G : Type u} [Group G] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpaceOne G X x) : IsAspherical X x

A K(G, 1) space is aspherical.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.nonempty_fundamentalGroupMulEquiv {G : Type u} [Group G] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpaceOne G X x) : Nonempty (FundamentalGroup X x ≃* G)

The fundamental group of a K(G, 1) space is isomorphic to G.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.of_basepoint {G : Type u} [Group G] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpaceOne G X x) (x' : X) : IsEilenbergMacLaneSpaceOne G X x'

The K(G, 1) property does not depend on the base point.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.of_mulEquiv {G : Type u} {H : Type v} [Group G] [Group H] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpaceOne G X x) (e : G ≃* H) : IsEilenbergMacLaneSpaceOne H X x

Transporting the target group along an isomorphism preserves the K(G, 1) property.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.prod {G₁ : Type u} {G₂ : Type v} [Group G₁] [Group G₂] {X₁ : Type w} {X₂ : Type w'} [TopologicalSpace X₁] [TopologicalSpace X₂] {x₁ : X₁} {x₂ : X₂} (h₁ : IsEilenbergMacLaneSpaceOne G₁ X₁ x₁) (h₂ : IsEilenbergMacLaneSpaceOne G₂ X₂ x₂) : IsEilenbergMacLaneSpaceOne (G₁ × G₂) (X₁ × X₂) (x₁, x₂)

The product of a K(G₁, 1) space and a K(G₂, 1) space is a K(G₁ × G₂, 1) space.

theorem TauCeti.IsEilenbergMacLaneSpaceOne.pi {ι : Type w} {G' : ι → Type u} {Z : ι → Type v} [(i : ι) → Group (G' i)] [(i : ι) → TopologicalSpace (Z i)] {z : (i : ι) → Z i} (h : ∀ (i : ι), IsEilenbergMacLaneSpaceOne (G' i) (Z i) (z i)) : IsEilenbergMacLaneSpaceOne ((i : ι) → G' i) ((i : ι) → Z i) z

An indexed product of K(Gᵢ, 1) spaces is a K(Π i, Gᵢ, 1) space.