Integral homology of a homotopy retract embeds

Proved

homotopyRetract_additivelyEmbeds_integralHomology

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

algebraic-topologyhomologyhomotopy-theory

Let $X$ and $Y$ be topological spaces. Suppose that $X$ is a homotopy retract of $Y$ : there are continuous maps

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

such that the composite $r \circ i$ is homotopic to $\mathrm{id}_X$ (no compatibility with basepoints is required, and $i \circ r$ is unconstrained).

Then for every degree $q$ the induced map $i_* : H_q(X;\mathbb Z) \to H_q(Y;\mathbb Z)$ on integral singular homology is an injective homomorphism of abelian groups; in particular $H_q(X;\mathbb Z)$ occurs as an additive subgroup of $H_q(Y;\mathbb Z)$ .

The proof is functoriality together with homotopy invariance: homotopic maps induce the same map on singular homology, so

r_* \circ i_* = (r \circ i)_* = (\mathrm{id}_X)_* = \mathrm{id},

which exhibits $r_*$ as a left inverse of $i_*$ ; a map with a left inverse is injective.

This is the homotopy-theoretic form of the strict-retract statement: it is what one needs when a splitting is only available up to homotopy, as happens for wedge summands and desuspension arguments.

Formalization Note Homology is Mathlib's integral singular homology functor in a fixed degree, and the conclusion is the existence of an injective additive homomorphism.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle

Formal statement

theorem homotopyRetract_additivelyEmbeds_integralHomology
    {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
    (i : C(X, Y)) (r : C(Y, X)) (hri : (r.comp i).Homotopic (ContinuousMap.id X)) (q : ℕ) :
    AdditivelyEmbeds (IntegralHomology q X) (IntegralHomology q Y) := by sorry

Source

Standard consequence of the homotopy invariance of singular homology: A. Hatcher, Algebraic Topology, Cambridge University Press 2002, Theorem 2.10 (homotopic maps induce the same homomorphism on singular homology) and the functoriality of H_*; the retract argument is the standard one used, e.g., in Hatcher Section 2.1, p. 111 (a retract induces a split injection on homology).

View graph