Maps from a CW complex into a space without higher homotopy

Let Y be a space whose homotopy groups πₙ(Y, y) vanish for n ≥ 2 at every point y, such as a K(H, 1). A map from a CW complex into Y is determined up to homotopy by what it does on the 1-skeleton up to homotopy: two maps f g : C → Y out of a relative CW complex (C, D) that, on every path in C between points of the 0-skeleton, agree up to homotopy relative to the endpoints, are homotopic relative to the 0-skeleton (TauCeti.homotopicRel_skeletonLT_one_of_forall_homotopicRel). For a complex whose only 0-cell is its base point, this says that pointed maps inducing the same homomorphism of fundamental groups are homotopic relative to the base point (TauCeti.homotopicRel_singleton_of_mapOfEq_eq). This is the uniqueness half of Hatcher's Proposition 1B.9 for complexes with a single 0-cell, the case to which Hatcher reduces by collapsing a maximal tree; for the cellular classifying space, the existence half is TauCeti.exists_mapOfEq_cellularClassifyingSpace.

The proof reads a homotopy from f to g relative to a set A as a deformation, relative to A, of the map (f, g) : C → Y × Y into the diagonal. Since the diagonal Δ ⊆ Y × Y is a retract of Y × Y and πₙ(Y × Y) vanishes for n ≥ 2, the exact sequence of the pair shows that the relative homotopy sets πₙ(Y × Y, Δ) vanish for n ≥ 2 (TauCeti.subsingleton_relHomotopyGroup_diagonal). So the compression lemma deforms (f, g) into Δ relative to D as soon as (C, D) has no cells of dimension 0 or 1 and f = g on D (TauCeti.homotopicRel_base_of_isEmpty_cell). In general the hypothesis on paths first lets one homotope f, relative to the 0-skeleton, to agree with g on every 1-cell, and the compression lemma then applies to C relative to its 1-skeleton (Topology.RelCWComplex.Subcomplex.relCWComplex), which has no cells of dimension below 2.

Only the vanishing of the higher homotopy groups of Y is used: neither space needs to be path connected, and Y need not have the homotopy type of a CW complex.

Main results

• TauCeti.subsingleton_relHomotopyGroup_diagonal: the relative homotopy sets of the diagonal in Y × Y vanish from degree 2 on.
• TauCeti.homotopicRel_base_of_isEmpty_cell: maps agreeing on the base of a relative CW complex without cells of dimension 0 and 1 are homotopic relative to the base.
• TauCeti.homotopicRel_skeletonLT_one_of_forall_homotopicRel: maps agreeing up to homotopy on paths between points of the 0-skeleton are homotopic relative to the 0-skeleton.
• TauCeti.homotopicRel_singleton_of_mapOfEq_eq: pointed maps from a CW complex with a single 0-cell into a space without higher homotopy are determined, up to homotopy relative to the base point, by the homomorphism they induce on fundamental groups.
• TauCeti.homotopicRel_singleton_of_mapOfEq_eq_of_cwComplex: the same for a CW structure on the whole space.

References

• A. Hatcher, Algebraic Topology, Section 1.B, Proposition 1B.9, and Section 4.1, Lemma 4.6 (the compression lemma).

theorem TauCeti.subsingleton_relHomotopyGroup_diagonal {Y : Type v} [TopologicalSpace Y] (hY : ∀ (y : Y) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Y y)) (n : ℕ) (b : ↑(Set.diagonal Y)) : Subsingleton (RelHomotopyGroup (Fin (n + 1)) { pair := TopPair.ofSubset (Set.diagonal Y), basepoint := b })

If the homotopy groups of Y vanish from degree 2 on, at every point, then so do the relative homotopy sets π_{n+2}(Y × Y, Δ, b) of the diagonal Δ ⊆ Y × Y, at every point b of the diagonal.

theorem TauCeti.homotopicRel_base_of_isEmpty_cell {Y : Type v} [TopologicalSpace Y] {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (h₀ : IsEmpty (Topology.RelCWComplex.cell C 0)) (h₁ : IsEmpty (Topology.RelCWComplex.cell C 1)) (hY : ∀ (y : Y) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Y y)) {f g : C(↑C, Y)} (hfg : ∀ (x : ↑C), ↑x ∈ D → f x = g x) : f.HomotopicRel g {x : ↑C | ↑x ∈ D}

Let (C, D) be a relative CW complex without cells of dimension 0 and 1, and let Y be a space whose homotopy groups vanish from degree 2 on, at every point. Then two maps C → Y that agree on D are homotopic relative to D.

theorem TauCeti.homotopicRel_skeletonLT_one_of_forall_homotopicRel {Y : Type v} [TopologicalSpace Y] {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (hY : ∀ (y : Y) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Y y)) {f g : C(↑C, Y)} (hfg : ∀ (γ : C(↑unitInterval, ↑C)), ↑(γ 0) ∈ Topology.RelCWComplex.skeletonLT C 1 → ↑(γ 1) ∈ Topology.RelCWComplex.skeletonLT C 1 → (f.comp γ).HomotopicRel (g.comp γ) {0, 1}) : f.HomotopicRel g {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C 1}

Let (C, D) be a relative CW complex, and let Y be a space whose homotopy groups vanish from degree 2 on, at every point. Let f g : C → Y be such that, for every path γ in C between points of the 0-skeleton skeletonLT C 1, the paths f ∘ γ and g ∘ γ are homotopic relative to their endpoints. Then f and g are homotopic relative to the 0-skeleton.

theorem TauCeti.homotopicRel_singleton_of_mapOfEq_eq {Y : Type v} [TopologicalSpace Y] {X : Type u} [TopologicalSpace X] [T2Space X] {C D : Set X} [Topology.RelCWComplex C D] (hY : ∀ (y : Y) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Y y)) {x₀ : ↑C} (hx₀ : {x : ↑C | ↑x ∈ Topology.RelCWComplex.skeletonLT C 1} = {x₀}) {f g : C(↑C, Y)} {y₀ : Y} (hf : f x₀ = y₀) (hg : g x₀ = y₀) (hfg : FundamentalGroup.mapOfEq f hf = FundamentalGroup.mapOfEq g hg) : f.HomotopicRel g {x₀}

Maps into a space without higher homotopy are determined by their effect on π₁. Let C be a relative CW complex whose 0-skeleton is a single point x₀, such as a CW complex with a single 0-cell, and let Y be a space whose homotopy groups vanish from degree 2 on, at every point, such as a K(H, 1). Two maps C → Y sending x₀ to y₀ and inducing the same homomorphism π₁(C, x₀) → π₁(Y, y₀) are homotopic relative to x₀.

theorem TauCeti.homotopicRel_singleton_of_mapOfEq_eq_of_cwComplex {Y : Type v} [TopologicalSpace Y] {X : Type u} [TopologicalSpace X] [T2Space X] [Topology.CWComplex Set.univ] (hY : ∀ (y : Y) (n : ℕ), Subsingleton (HomotopyGroup.Pi (n + 2) Y y)) {x₀ : X} (hx₀ : ↑(Topology.RelCWComplex.skeletonLT Set.univ 1) = {x₀}) {f g : C(X, Y)} {y₀ : Y} (hf : f x₀ = y₀) (hg : g x₀ = y₀) (hfg : FundamentalGroup.mapOfEq f hf = FundamentalGroup.mapOfEq g hg) : f.HomotopicRel g {x₀}

Maps into a space without higher homotopy are determined by their effect on π₁, for a CW structure on the whole space. Let X be a CW complex whose 0-skeleton is a single point x₀, such as a CW complex with a single 0-cell, and let Y be a space whose homotopy groups vanish from degree 2 on, at every point. Two maps X → Y sending x₀ to y₀ and inducing the same homomorphism π₁(X, x₀) → π₁(Y, y₀) are homotopic relative to x₀.