A full subcomplex makes a retract of : loop-homology embedding in every degree
ProvedmomentAngle_fullSubcomplex_loopHomology_retractLet be a finite abstract simplicial complex on vertices, one on vertices, and let identify with the full subcomplex of spanned by , i.e. is a face of if and only if is a face of . Then for every degree there is an injective additive homomorphism
The coordinate inclusion (extend by outside ) and the coordinate projection are both based maps for the all-ones basepoints, and the projection is a left inverse of the inclusion. Post-composition with a based map is continuous for the compact-open topology on loop spaces, so the based loop spaces inherit the retraction, and any homology functor converts it into a split injection.
Formalization Note The loop space is the space of based paths from the all-ones point to itself with the compact-open topology, homology is integral singular homology in the fixed degree , and the conclusion is an explicit injective additive homomorphism.
import Definitions.Def_frame_2026_moment_angle_interfaces open MomentAngle
theorem momentAngle_fullSubcomplex_loopHomology_retract
{s m : ℕ} (K : AbstractSimplicialComplex (Fin s))
(L : AbstractSimplicialComplex (Fin m)) (e : Fin s ↪ Fin m)
(hfull : ∀ σ : Finset (Fin s), σ ∈ K ↔ σ.map e ∈ L) (q : ℕ) :
AdditivelyEmbeds (IntegralHomology q (BasedLoopSpace K))
(IntegralHomology q (BasedLoopSpace L)) := by sorry