Killing the homotopy groups of a space from a given dimension on

Let X be a Hausdorff space with a base point x, and let n ≥ 1. Attaching (n + 1)-cells along every generalized loop of dimension n at x kills πₙ without changing the lower homotopy groups (TauCeti.subsingleton_homotopyGroup_cellAttachment). Iterating, and attaching cells of dimension k + 1 along every generalized loop of dimension k at the image of x for k = n, n + 1, … in turn, gives an expanding sequence of spaces, the tower TauCeti.killingTower n X x. Its colimit TauCeti.killHomotopyGroups n X x contains X, and

• the inclusion X ⟶ killHomotopyGroups n X x induces a bijection on πₖ for k < n (TauCeti.bijective_homotopyGroupMap_killHomotopyGroupsIncl);
• πₖ of killHomotopyGroups n X x at the image of x vanishes for k ≥ n (TauCeti.subsingleton_homotopyGroup_killHomotopyGroups).

For n = 2 and a path-connected X this makes killHomotopyGroups 2 X x an Eilenberg--Mac Lane space of type K(π₁(X, x), 1) containing X (TauCeti.isEilenbergMacLaneSpaceOne_killHomotopyGroups). This is Hatcher's construction of a K(G, 1) from a presentation complex of G, carried out here for an arbitrary Hausdorff space. More generally, for n ≥ 1 and a Hausdorff, path-connected X whose homotopy groups πₖ(X, x) vanish for 0 < k < n, the space killHomotopyGroups (n + 1) X x is an Eilenberg--Mac Lane space of type K(πₙ(X, x), n) containing X (TauCeti.isEilenbergMacLaneSpace_killHomotopyGroups), the inclusion inducing the isomorphism on πₙ (TauCeti.killHomotopyGroupsHomotopyGroupMulEquiv). If the homotopy groups of a path-connected X already vanish from dimension n on, the inclusion of X is a weak homotopy equivalence (TauCeti.isWeakHomotopyEquivalence_killHomotopyGroupsIncl): the attached cells change no homotopy group.

The cells attached at step m of the tower have dimension m, so the tower is a categorical relative CW complex in Mathlib's sense, relative to X (TauCeti.killHomotopyGroupsRelativeCWComplex). This is what controls the colimit: it is Hausdorff, X and every stage are closed subspaces, the stage after step m is the classical skeleton of dimension m, and Hatcher's Corollary 4.12 identifies the homotopy groups of the colimit in each dimension with those of a finite stage (TopCat.RelativeCWComplex.surjective_homotopyGroupMap_incl_app, TopCat.RelativeCWComplex.bijective_homotopyGroupMap).

When X is itself a Hausdorff CW complex with no cells of dimension greater than n, this relative CW structure, read classically, composes with the CW structure of X (TopCat.RelativeCWComplex.cwComplexTrans): the cells of the tower have dimension greater than n, so their boundaries meet X inside its skeleton below their dimension. So killHomotopyGroups n X x is then a CW complex (TauCeti.killHomotopyGroupsCWComplex), whose cells are those of X and those of the tower, and in particular it has CW type (TauCeti.cwType_killHomotopyGroups).

Maps out of the colimit are built in the same way, stage by stage. Every cell of the tower is attached along a based map, so a map f : X ⟶ Z into a space whose homotopy groups πₖ(Z, f x) vanish for k ≥ n extends over each new cell, and these extensions form a cocone on the tower: f extends over killHomotopyGroups n X x (TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq). For n ≥ 2 the extension induces on π₁ the map induced by f (TauCeti.exists_mapOfEq_comp_killHomotopyGroupsFundamentalGroupMulEquiv). In particular, for n = 2 every map from X into a K(H, 1) space extends over killHomotopyGroups 2 X x, realizing the same homomorphism of fundamental groups; for a Hausdorff, path-connected X that space is a K(π₁(X, x), 1). In every degree n ≥ 1, a map from an (n - 1)-connected X into a K(G, n) space that is bijective on πₙ extends to a weak homotopy equivalence out of killHomotopyGroups (n + 1) X x (TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq_and_isWeakHomotopyEquivalence): this K(πₙ(X, x), n) is unique up to weak homotopy equivalence among the K(G, n) spaces receiving such a map from X.

Main definitions

• TauCeti.killingStage n X x m: the pointed space after the first m steps.
• TauCeti.killingTower n X x: the tower of stages, as a functor ℕ ⥤ TopCat.
• TauCeti.killHomotopyGroups n X x: its colimit, with the inclusion TauCeti.killHomotopyGroupsIncl n X x of X.
• TauCeti.killHomotopyGroupsRelativeCWComplex n X x: the relative CW structure.
• TauCeti.killHomotopyGroupsFundamentalGroupMulEquiv n X x: for n ≥ 2, the isomorphism of fundamental groups induced by the inclusion.
• TauCeti.killHomotopyGroupsHomotopyGroupMulEquiv n X x k: for 0 < k < n, the isomorphism of πₖ induced by the inclusion.
• TauCeti.killHomotopyGroupsCWComplex n X x hX: for a Hausdorff CW complex X without cells of dimension greater than n, the CW structure on the colimit, with its cells described by TauCeti.killHomotopyGroupsCWComplexCellEquiv.

Main results

• TauCeti.bijective_homotopyGroupMap_killHomotopyGroupsIncl: the homotopy groups below dimension n are unchanged.
• TauCeti.subsingleton_homotopyGroup_killHomotopyGroups: the homotopy groups from dimension n on vanish.
• TauCeti.isEilenbergMacLaneSpaceOne_killHomotopyGroups: for n = 2 and path-connected X, the colimit is a K(π₁(X, x), 1).
• TauCeti.isEilenbergMacLaneSpace_killHomotopyGroups: for an (n - 1)-connected X, the space killHomotopyGroups (n + 1) X x is a K(πₙ(X, x), n).
• TauCeti.isWeakHomotopyEquivalence_killHomotopyGroupsIncl: if the homotopy groups of a path-connected X already vanish from dimension n on, the inclusion is a weak homotopy equivalence.
• TauCeti.cwType_killHomotopyGroups: for a Hausdorff CW complex X without cells of dimension greater than n, the colimit has CW type.
• TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq: maps into a space whose homotopy groups vanish from dimension n on extend over the colimit.
• TauCeti.exists_mapOfEq_comp_killHomotopyGroupsFundamentalGroupMulEquiv: for n ≥ 2, the extension induces the given map on fundamental groups.
• TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq_and_isWeakHomotopyEquivalence: a map from an (n - 1)-connected X into a K(G, n) space that is bijective on πₙ extends to a weak homotopy equivalence out of killHomotopyGroups (n + 1) X x.

References

• A. Hatcher, Algebraic Topology, Section 1.B, the construction of a K(G, 1) from a presentation complex, and Section 4.1, Corollary 4.12 and Example 4.16 on killing homotopy groups by attaching cells, and Lemma 4.7 and Proposition 1B.9 on extending maps over cells into a space without higher homotopy.

noncomputable def TauCeti.killingAttachingMaps (n : ℕ) [NeZero n] (Y : TopCat) (y : ↑Y) (m : ℕ) : (ι : Type u) × (ι → (TopCat.diskBoundary m ⟶ Y))

The attaching maps of the cells attached at step m of the tower killing the homotopy groups of a pointed space (Y, y) from dimension n on. At step 0 no cell is attached. At step k + 1 one (k + 1)-cell is attached along every generalized loop of dimension k at y when n ≤ k, and no cell otherwise. The body is exposed so that the stages of the tower are cell attachments by definition.

def TauCeti.killingStage (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : ℕ → (Y : TopCat) × ↑Y

The stages of the tower killing the homotopy groups of (X, x) from dimension n on: killingStage n X x m is the pointed space obtained from (X, x) by the first m steps, each attaching cells along the maps TauCeti.killingAttachingMaps. The body is exposed so that each stage is the cell attachment to the previous one by definition.

noncomputable def TauCeti.killingStageIncl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : (killingStage n X x m).fst ⟶ (killingStage n X x (m + 1)).fst

The inclusion of each stage of the tower into the next.

theorem TauCeti.killingStageIncl_def (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : killingStageIncl n X x m = cellAttachmentIncl (killingAttachingMaps n (killingStage n X x m).fst (killingStage n X x m).snd m).snd

The inclusion of each stage of the tower into the next is the inclusion of the cell attachment.

@[simp]

theorem TauCeti.killingStageIncl_basepoint (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (killingStageIncl n X x m)) (killingStage n X x m).snd = (killingStage n X x (m + 1)).snd

The inclusion of each stage of the tower into the next preserves the base points.

noncomputable def TauCeti.killingTower (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : CategoryTheory.Functor ℕ TopCat

The tower killing the homotopy groups of (X, x) from dimension n on, as a sequence of spaces and inclusions. The body is exposed so that its objects are the stages TauCeti.killingStage n X x m by definition.

noncomputable def TauCeti.killHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : TopCat

The space obtained from X by killing its homotopy groups at x from dimension n on: the colimit of the tower TauCeti.killingTower n X x. The body is exposed so that the colimit inclusions of the stages are maps into this space by definition.

noncomputable def TauCeti.killHomotopyGroupsIncl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : X ⟶ killHomotopyGroups n X x

The inclusion of X into TauCeti.killHomotopyGroups n X x: the colimit inclusion of stage 0. The body is exposed so that the relative CW structure below is a structure on this map.

@[simp]

theorem TauCeti.killingTower_map_homOfLE_succ (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : (killingTower n X x).map (CategoryTheory.homOfLE ⋯) = killingStageIncl n X x m

The step from stage m to stage m + 1 of the tower is the inclusion of the cell attachment.

noncomputable def TauCeti.killHomotopyGroupsRelativeCWComplex (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : TopCat.RelativeCWComplex (killHomotopyGroupsIncl n X x)

The tower is a relative CW complex: the step from stage m to stage m + 1 attaches m-cells, along the maps TauCeti.killingAttachingMaps. The body is exposed so that its stages and their inclusions are those of the tower by definition, as recorded by killHomotopyGroupsRelativeCWComplex_F and killHomotopyGroupsRelativeCWComplex_incl_app.

theorem TauCeti.killHomotopyGroupsRelativeCWComplex_F (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : (killHomotopyGroupsRelativeCWComplex n X x).F = killingTower n X x

The stages of the relative CW complex are the stages of the tower.

theorem TauCeti.killHomotopyGroupsRelativeCWComplex_incl_app (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : (killHomotopyGroupsRelativeCWComplex n X x).incl.app m = CategoryTheory.Limits.colimit.ι (killingTower n X x) m

The inclusions of the stages of the relative CW complex are the colimit inclusions.

theorem TauCeti.killHomotopyGroupsRelativeCWComplex_attachCells_ι (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : ((killHomotopyGroupsRelativeCWComplex n X x).attachCells m ⋯).ι = (killingAttachingMaps n (killingStage n X x m).fst (killingStage n X x m).snd m).fst

The cells attached at step m of the relative CW complex are indexed as in TauCeti.killingAttachingMaps.

@[simp]

theorem TauCeti.colimit_ι_killingStage_basepoint (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι (killingTower n X x) m)) (killingStage n X x m).snd = (CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) x

The base point of each stage goes to the image of x in the colimit.

instance TauCeti.instT2SpaceKillingStage (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] (m : ℕ) : T2Space ↑(killingStage n X x m).fst

Every stage of the tower over a Hausdorff space is Hausdorff.

theorem TauCeti.isEmpty_killHomotopyGroupsRelativeCWComplex_attachCells_ι (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) {m : ℕ} (hm : m ≤ n) : IsEmpty ((killHomotopyGroupsRelativeCWComplex n X x).attachCells m ⋯).ι

No cells of dimension at most n are attached in the tower.

instance TauCeti.instT2SpaceKillHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] : T2Space ↑(killHomotopyGroups n X x)

TauCeti.killHomotopyGroups n X x is Hausdorff when X is.

theorem TauCeti.isClosedEmbedding_killHomotopyGroupsIncl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) : Topology.IsClosedEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x))

The inclusion of X into TauCeti.killHomotopyGroups n X x is a closed embedding.

theorem TauCeti.bijective_homotopyGroupMap_killHomotopyGroupsIncl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] {N : Type v} [Finite N] (hN : Nat.card N < n) : Function.Bijective (HomotopyGroup.map (TopCat.Hom.hom (killHomotopyGroupsIncl n X x)) ⋯)

Killing the homotopy groups from dimension n on does not change them below n. For a Hausdorff space X, the inclusion X ⟶ killHomotopyGroups n X x induces a bijection on πₖ at x, where k = Nat.card N < n.

theorem TauCeti.subsingleton_homotopyGroup_killHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] {k : ℕ} (hk : n ≤ k) : Subsingleton (HomotopyGroup.Pi k (↑(killHomotopyGroups n X x)) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) x))

The homotopy groups of killHomotopyGroups n X x vanish from dimension n on, at the image of x, for a Hausdorff space X.

instance TauCeti.instPathConnectedSpaceKillHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [PathConnectedSpace ↑X] : PathConnectedSpace ↑(killHomotopyGroups n X x)

TauCeti.killHomotopyGroups n X x is path-connected when X is Hausdorff and path-connected: attaching cells of positive dimension creates no new path components.

noncomputable def TauCeti.killHomotopyGroupsFundamentalGroupMulEquiv (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] (hn : 1 < n) : FundamentalGroup (↑X) x ≃* FundamentalGroup (↑(killHomotopyGroups n X x)) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) x)

For n ≥ 2, the inclusion of X into TauCeti.killHomotopyGroups n X x induces an isomorphism of fundamental groups at x.

@[simp]

theorem TauCeti.killHomotopyGroupsFundamentalGroupMulEquiv_apply (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] (hn : 1 < n) (g : FundamentalGroup (↑X) x) : (killHomotopyGroupsFundamentalGroupMulEquiv n X x hn) g = (FundamentalGroup.mapOfEq (TopCat.Hom.hom (killHomotopyGroupsIncl n X x)) ⋯) g

The isomorphism of fundamental groups is the map induced by the inclusion of X.

noncomputable def TauCeti.killHomotopyGroupsHomotopyGroupMulEquiv (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] (k : ℕ) [NeZero k] (hk : k < n) : HomotopyGroup.Pi k (↑X) x ≃* HomotopyGroup.Pi k (↑(killHomotopyGroups n X x)) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) x)

For 0 < k < n, the inclusion of X into TauCeti.killHomotopyGroups n X x induces an isomorphism of πₖ at x.

@[simp]

theorem TauCeti.killHomotopyGroupsHomotopyGroupMulEquiv_apply (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] (k : ℕ) [NeZero k] (hk : k < n) (a : HomotopyGroup.Pi k (↑X) x) : (killHomotopyGroupsHomotopyGroupMulEquiv n X x k hk) a = HomotopyGroup.map (TopCat.Hom.hom (killHomotopyGroupsIncl n X x)) ⋯ a

The isomorphism of πₖ is the map induced by the inclusion of X.

theorem TauCeti.isEilenbergMacLaneSpace_killHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [PathConnectedSpace ↑X] (hX : ∀ (k : ℕ), k ≠ 0 → k < n → Subsingleton (HomotopyGroup.Pi k (↑X) x)) : IsEilenbergMacLaneSpace (HomotopyGroup.Pi n (↑X) x) n (↑(killHomotopyGroups (n + 1) X x)) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl (n + 1) X x)) x)

Killing the homotopy groups above dimension n of an (n - 1)-connected space gives a K(πₙ, n). For n ≥ 1 and a Hausdorff, path-connected space X whose homotopy groups πₖ(X, x) vanish for 0 < k < n, the space TauCeti.killHomotopyGroups (n + 1) X x, obtained by attaching cells of dimension at least n + 2, is an Eilenberg--Mac Lane space of type K(πₙ(X, x), n), the isomorphism on πₙ being induced by the inclusion of X (TauCeti.killHomotopyGroupsHomotopyGroupMulEquiv).

theorem TauCeti.isEilenbergMacLaneSpaceOne_killHomotopyGroups (X : TopCat) (x : ↑X) [T2Space ↑X] [PathConnectedSpace ↑X] : IsEilenbergMacLaneSpaceOne (FundamentalGroup (↑X) x) (↑(killHomotopyGroups 2 X x)) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl 2 X x)) x)

Killing the higher homotopy groups of a path-connected space gives a K(π₁, 1). For a Hausdorff, path-connected space X, the space TauCeti.killHomotopyGroups 2 X x obtained by attaching cells of dimension at least 3 is aspherical, and the inclusion of X identifies its fundamental group with π₁(X, x).

theorem TauCeti.isWeakHomotopyEquivalence_killHomotopyGroupsIncl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [PathConnectedSpace ↑X] (hX : ∀ (k : ℕ), n ≤ k → Subsingleton (HomotopyGroup.Pi k (↑X) x)) : (TopCat.Hom.hom (killHomotopyGroupsIncl n X x)).IsWeakHomotopyEquivalence

Killing homotopy groups which already vanish changes nothing up to weak homotopy equivalence. If the homotopy groups πₖ(X, x) of a Hausdorff, path-connected space X vanish for k ≥ n, the inclusion of X into TauCeti.killHomotopyGroups n X x is a weak homotopy equivalence.

The CW structure on the colimit

@[instance_reducible]

noncomputable def TauCeti.killHomotopyGroupsCWComplex (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), n < m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) : Topology.CWComplex Set.univ

The colimit of the tower is a CW complex. If X is a Hausdorff CW complex all of whose cells have dimension at most n, then TauCeti.killHomotopyGroups n X x is a CW complex. Its m-cells are the m-cells of X, included by TauCeti.killHomotopyGroupsIncl n X x, and the cells attached at step m of the tower, which all have dimension greater than n (TauCeti.killHomotopyGroupsCWComplexCellEquiv).

noncomputable def TauCeti.killHomotopyGroupsCWComplexCellEquiv (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), n < m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (m : ℕ) : Topology.RelCWComplex.cell Set.univ m ≃ Topology.RelCWComplex.cell Set.univ m ⊕ ((killHomotopyGroupsRelativeCWComplex n X x).attachCells m ⋯).ι

The m-cells of TauCeti.killHomotopyGroupsCWComplex are the m-cells of X together with the cells attached at step m of the tower.

@[simp]

theorem TauCeti.coe_map_killHomotopyGroupsCWComplexCellEquiv_symm_inl (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), n < m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (m : ℕ) (i : Topology.RelCWComplex.cell Set.univ m) : ↑(Topology.RelCWComplex.map m ((killHomotopyGroupsCWComplexCellEquiv n X x hX m).symm (Sum.inl i))) = ⇑(CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) ∘ ↑(Topology.RelCWComplex.map m i)

The characteristic map of an m-cell of X, as a cell of TauCeti.killHomotopyGroupsCWComplex, is its characteristic map in X followed by the inclusion TauCeti.killHomotopyGroupsIncl n X x.

@[simp]

theorem TauCeti.map_killHomotopyGroupsCWComplexCellEquiv_symm_inr (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), n < m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) (m : ℕ) (i : ((killHomotopyGroupsRelativeCWComplex n X x).attachCells m ⋯).ι) (y : ↑(Metric.closedBall 0 1)) : ↑(Topology.RelCWComplex.map m ((killHomotopyGroupsCWComplexCellEquiv n X x hX m).symm (Sum.inr i))) ↑y = (CategoryTheory.ConcreteCategory.hom { j := m, hj := ⋯, k := i }.ι) ((diskHomeomorphClosedBall m).symm y)

The characteristic map of a cell attached at step m of the tower, as a cell of TauCeti.killHomotopyGroupsCWComplex, is the inclusion of the attached disk, read on the closed unit ball of the sup norm through the radial homeomorphism TauCeti.diskHomeomorphClosedBall.

theorem TauCeti.cwType_killHomotopyGroups (n : ℕ) [NeZero n] (X : TopCat) (x : ↑X) [T2Space ↑X] [Topology.CWComplex Set.univ] (hX : ∀ (m : ℕ), n < m → IsEmpty (Topology.RelCWComplex.cell Set.univ m)) : CWType ↑(killHomotopyGroups n X x)

If X is a Hausdorff CW complex all of whose cells have dimension at most n, then TauCeti.killHomotopyGroups n X x has CW type.

Extending maps over the tower

theorem TopCat.Hom.exists_killingStageIncl_comp_eq {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} {Z : TopCat} {m : ℕ} (g : (TauCeti.killingStage n X x m).fst ⟶ Z) (hZ : ∀ (k : ℕ), m = k + 1 → n ≤ k → Subsingleton (HomotopyGroup.Pi k (↑Z) ((CategoryTheory.ConcreteCategory.hom g) (TauCeti.killingStage n X x m).snd))) : ∃ (g' : (TauCeti.killingStage n X x (m + 1)).fst ⟶ Z), CategoryTheory.CategoryStruct.comp (TauCeti.killingStageIncl n X x m) g' = g

A based map extends over one step of the tower. If the homotopy group of Z vanishes in the dimension of the spheres attached at step m, every map g out of stage m extends over stage m + 1.

theorem TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} {Z : TopCat} (f : X ⟶ Z) (hZ : ∀ (k : ℕ), n ≤ k → Subsingleton (HomotopyGroup.Pi k (↑Z) ((CategoryTheory.ConcreteCategory.hom f) x))) : ∃ (F : TauCeti.killHomotopyGroups n X x ⟶ Z), CategoryTheory.CategoryStruct.comp (TauCeti.killHomotopyGroupsIncl n X x) F = f

Maps into a space without homotopy from dimension n on extend over TauCeti.killHomotopyGroups n X x. If the homotopy groups πₖ(Z, f x) vanish for every k ≥ n, then f : X ⟶ Z extends along the inclusion X ⟶ killHomotopyGroups n X x. Only the homotopy groups at the base point f x enter, because every cell of the tower is attached along a based map.

theorem TauCeti.exists_mapOfEq_comp_killHomotopyGroupsFundamentalGroupMulEquiv {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} {Z : TopCat} [T2Space ↑X] (hn : 1 < n) (f : X ⟶ Z) (hZ : ∀ (k : ℕ), n ≤ k → Subsingleton (HomotopyGroup.Pi k (↑Z) ((CategoryTheory.ConcreteCategory.hom f) x))) : ∃ (F : killHomotopyGroups n X x ⟶ Z) (hF : (CategoryTheory.ConcreteCategory.hom F) ((CategoryTheory.ConcreteCategory.hom (killHomotopyGroupsIncl n X x)) x) = (CategoryTheory.ConcreteCategory.hom f) x), (FundamentalGroup.mapOfEq (TopCat.Hom.hom F) hF).comp (killHomotopyGroupsFundamentalGroupMulEquiv n X x hn).toMonoidHom = FundamentalGroup.mapOfEq (TopCat.Hom.hom f) ⋯

The extension realizes the map on fundamental groups. For n ≥ 2 and a Hausdorff space X, if the homotopy groups πₖ(Z, f x) vanish for every k ≥ n, then f : X ⟶ Z extends to a based map F out of TauCeti.killHomotopyGroups n X x that induces on π₁ the map induced by f, read through the isomorphism TauCeti.killHomotopyGroupsFundamentalGroupMulEquiv.

theorem TopCat.Hom.exists_killHomotopyGroupsIncl_comp_eq_and_isWeakHomotopyEquivalence {n : ℕ} [NeZero n] {X : TopCat} {x : ↑X} {Z : TopCat} [T2Space ↑X] [PathConnectedSpace ↑X] (hX : ∀ (k : ℕ), k ≠ 0 → k < n → Subsingleton (HomotopyGroup.Pi k (↑X) x)) {G : Type u_1} [Group G] (f : X ⟶ Z) (hZ : TauCeti.IsEilenbergMacLaneSpace G n (↑Z) ((CategoryTheory.ConcreteCategory.hom f) x)) (hf : Function.Bijective (HomotopyGroup.map (hom f) ⋯)) : ∃ (F : TauCeti.killHomotopyGroups (n + 1) X x ⟶ Z), CategoryTheory.CategoryStruct.comp (TauCeti.killHomotopyGroupsIncl (n + 1) X x) F = f ∧ (hom F).IsWeakHomotopyEquivalence

The K(πₙ, n) of an (n - 1)-connected space is unique up to weak homotopy equivalence. Let n ≥ 1 and let X be a Hausdorff, path-connected space whose homotopy groups πₖ(X, x) vanish for 0 < k < n. A map f : X ⟶ Z into a K(G, n) space that induces a bijection on πₙ extends along the inclusion of X to a weak homotopy equivalence from the K(πₙ(X, x), n) space TauCeti.killHomotopyGroups (n + 1) X x.