Eilenberg--Mac Lane spaces of type K(G, n)

For a positive integer n and a group G, a based space (X, x) is an Eilenberg--Mac Lane space of type K(G, n) when it is path-connected, its homotopy groups πₖ(X, x) vanish for every positive k ≠ n, and πₙ(X, x) is isomorphic to G (TauCeti.IsEilenbergMacLaneSpace). For n ≥ 2 the group πₙ(X, x) is abelian, so then G is abelian; for n = 1 this is the existing notion TauCeti.IsEilenbergMacLaneSpaceOne (TauCeti.isEilenbergMacLaneSpace_one_iff).

As for K(G, 1) spaces, the definition is a property rather than a structure carrying a chosen isomorphism. It does not depend on the base point or on the target group up to isomorphism, and it is closed under binary and indexed products. Homotopy invariance (TauCeti.IsEilenbergMacLaneSpace.of_homotopyEquiv) is in TauCeti.AlgebraicTopology.EilenbergMacLane.HomotopyEquiv, and the weak-equivalence criterion (TauCeti.IsEilenbergMacLaneSpace.isWeakHomotopyEquivalence_iff) is in TauCeti.AlgebraicTopology.EilenbergMacLane.WeakHomotopyEquivalence, next to their K(G, 1) and aspherical versions.

Main declarations

• TauCeti.IsEilenbergMacLaneSpace G n X x: (X, x) is a K(G, n) space.
• TauCeti.isEilenbergMacLaneSpace_one_iff: in degree one this is TauCeti.IsEilenbergMacLaneSpaceOne.
• TauCeti.IsEilenbergMacLaneSpace.of_basepoint, TauCeti.IsEilenbergMacLaneSpace.of_mulEquiv: invariance under change of base point and of the group.
• TauCeti.IsEilenbergMacLaneSpace.prod, TauCeti.IsEilenbergMacLaneSpace.pi: closure under products.

References

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Section 4.2, Eilenberg--MacLane spaces.

def TauCeti.IsEilenbergMacLaneSpace (G : Type u) [Group G] (n : ℕ) [NeZero n] (X : Type v) [TopologicalSpace X] (x : X) : Prop

A based space (X, x) is an Eilenberg--Mac Lane space of type K(G, n), for a positive integer n, when it is path-connected, its homotopy groups πₖ(X, x) vanish for every positive k ≠ n, and πₙ(X, x) is isomorphic to G.

theorem TauCeti.isEilenbergMacLaneSpace_iff {G : Type u} [Group G] {n : ℕ} [NeZero n] {X : Type v} [TopologicalSpace X] {x : X} : IsEilenbergMacLaneSpace G n X x ↔ PathConnectedSpace X ∧ (∀ (k : ℕ), k ≠ 0 → k ≠ n → Subsingleton (HomotopyGroup.Pi k X x)) ∧ Nonempty (HomotopyGroup.Pi n X x ≃* G)

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

@[simp]

theorem TauCeti.isEilenbergMacLaneSpace_homotopyGroup_iff {n : ℕ} [NeZero n] {X : Type v} [TopologicalSpace X] {x : X} : IsEilenbergMacLaneSpace (HomotopyGroup.Pi n X x) n X x ↔ PathConnectedSpace X ∧ ∀ (k : ℕ), k ≠ 0 → k ≠ n → Subsingleton (HomotopyGroup.Pi k X x)

A based space is an Eilenberg--Mac Lane space of type K(πₙ(X, x), n) if and only if it is path-connected and its other positive-dimensional homotopy groups vanish.

theorem TauCeti.IsEilenbergMacLaneSpace.mk {G : Type u} [Group G] {n : ℕ} [NeZero n] {X : Type w} [TopologicalSpace X] {x : X} (hX : PathConnectedSpace X) (hπ : ∀ (k : ℕ), k ≠ 0 → k ≠ n → Subsingleton (HomotopyGroup.Pi k X x)) (hG : Nonempty (HomotopyGroup.Pi n X x ≃* G)) : IsEilenbergMacLaneSpace G n X x

Construct the K(G, n) property from path-connectedness, the vanishing of the other positive-dimensional homotopy groups and an isomorphism between πₙ and G.

theorem TauCeti.IsEilenbergMacLaneSpace.pathConnectedSpace {G : Type u} [Group G] {n : ℕ} [NeZero n] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpace G n X x) : PathConnectedSpace X

A K(G, n) space is path-connected.

theorem TauCeti.IsEilenbergMacLaneSpace.subsingleton_homotopyGroup {G : Type u} [Group G] {n : ℕ} [NeZero n] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpace G n X x) {k : ℕ} (hk : k ≠ n) : Subsingleton (HomotopyGroup.Pi k X x)

Every homotopy group of a K(G, n) space outside dimension n is trivial, including the set π₀ of path components.

theorem TauCeti.IsEilenbergMacLaneSpace.nonempty_homotopyGroupMulEquiv {G : Type u} [Group G] {n : ℕ} [NeZero n] {X : Type w} [TopologicalSpace X] {x : X} (h : IsEilenbergMacLaneSpace G n X x) : Nonempty (HomotopyGroup.Pi n X x ≃* G)

The nth homotopy group of a K(G, n) space is isomorphic to G.

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

The K(G, n) property does not depend on the base point. A K(G, n) space is path connected, so its homotopy groups at any two points are isomorphic.

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

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

theorem TauCeti.IsEilenbergMacLaneSpace.prod {n : ℕ} [NeZero n] {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₁ : IsEilenbergMacLaneSpace G₁ n X₁ x₁) (h₂ : IsEilenbergMacLaneSpace G₂ n X₂ x₂) : IsEilenbergMacLaneSpace (G₁ × G₂) n (X₁ × X₂) (x₁, x₂)

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

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

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

theorem TauCeti.isEilenbergMacLaneSpace_one_iff {G : Type u} [Group G] {X : Type v} [TopologicalSpace X] {x : X} : IsEilenbergMacLaneSpace G 1 X x ↔ IsEilenbergMacLaneSpaceOne G X x

In degree one, the K(G, n) property is the K(G, 1) property.