Loop-space homology of a based homotopy retract embeds

Proved

basedHomotopyRetract_additivelyEmbeds_loopHomology

by Gabewhigham · Sep 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebraic-topologyhomologyhomotopy-theoryloop-spaces

Let $(X,x_0)$ and $(Y,y_0)$ be based topological spaces and suppose $X$ is a based homotopy retract of $Y$ : there are continuous maps

i : X \to Y, \qquad r : Y \to X,

with $i(x_0)=y_0$ , and a homotopy from $r \circ i$ to $\mathrm{id}_X$ that fixes the basepoint $x_0$ at all times. (The identity $r(y_0)=x_0$ is not assumed; it follows, since the basepoint-fixing homotopy forces $r(i(x_0))=x_0$ .)

Then for every degree $q$ the integral singular homology of the based loop space $\Omega X$ embeds as an additive subgroup of that of $\Omega Y$ :

H_q(\Omega X;\mathbb Z) \hookrightarrow H_q(\Omega Y;\mathbb Z).

The argument is that $\Omega$ is functorial for based maps and takes basepoint-fixing homotopies to homotopies: if $H_t$ is a homotopy from $r\circ i$ to $\mathrm{id}_X$ with $H_t(x_0)=x_0$ for all $t$ , then $\gamma \mapsto H_t \circ \gamma$ is a homotopy of self-maps of $\Omega X$ from $\Omega(r)\circ \Omega(i)$ to the identity. Hence $\Omega X$ is a homotopy retract of $\Omega Y$ , and the induced map $\Omega(i)_*$ on singular homology has a left inverse, so it is injective.

Formalization Note The based loop space is Mathlib's space of paths from the basepoint to itself, with the topology induced from the compact-open topology; the homotopy hypothesis is HomotopicRel relative to the singleton containing the basepoint; homology is integral singular homology, and the conclusion is an injective additive homomorphism.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem basedHomotopyRetract_additivelyEmbeds_loopHomology
    {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] {x₀ : X} {y₀ : Y}
    (i : C(X, Y)) (r : C(Y, X)) (hi : i x₀ = y₀)
    (hri : (r.comp i).HomotopicRel (ContinuousMap.id X) {x₀}) (q : ℕ) :
    AdditivelyEmbeds (IntegralHomology q (Path x₀ x₀)) (IntegralHomology q (Path y₀ y₀)) := by
  sorry

Source

Standard consequence of the functoriality of the based loop space and the homotopy invariance of singular homology: A. Hatcher, Algebraic Topology, Cambridge University Press 2002, Theorem 2.10, together with the fact that a based homotopy induces a homotopy of induced maps of based loop spaces (Hatcher, Section 4.3, discussion of the loop space functor).

View graph