A subgroup of one homology group is a subgroup of the total homology

Proved

additivelyEmbeds_totalIntegralHomology_of_degree

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

algebraic-topologyhomology

Let $X$ be a topological space, $G$ an abelian group and $q$ a nonnegative integer. If $G$ admits an injective additive homomorphism into $H_q(X;\mathbb Z)$ , then it admits one into the total integral homology

H_*(X;\mathbb Z)=\bigoplus_{n\ge0}H_n(X;\mathbb Z).

The inclusion of the degree- $q$ summand into the direct sum is injective, and composing with it transports any embedding into a single homology group to an embedding into the total homology. This is the bridge between degree-specific computations and statements phrased in terms of total homology.

Formalization Note Homology is integral singular homology and total homology is the direct sum over all nonnegative degrees, as in the ambient definition file; "subgroup" means an explicit injective additive homomorphism.

Preamble

import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle DirectSum

Formal statement

theorem additivelyEmbeds_totalIntegralHomology_of_degree
    (G : Type) [AddCommGroup G] (X : Type) [TopologicalSpace X] (q : ℕ)
    (h : AdditivelyEmbeds G (IntegralHomology q X)) :
    AdditivelyEmbeds G (TotalIntegralHomology X) := by sorry

Source

Elementary property of direct sums of abelian groups, in the total-homology formulation used by this mission.

View graph