Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

A full subcomplex makes OmegamathcalZK\\Omega\\mathcal Z_KOmegamathcalZK​ a retract of OmegamathcalZL\\Omega\\mathcal Z_LOmegamathcalZL​: loop-homology embedding in every degree

Proved
momentAngle_fullSubcomplex_loopHomology_retract

by Gabewhigham · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologyhomologyloop-spacesmoment-angle-complexes

Let KKK be a finite abstract simplicial complex on sss vertices, LLL one on mmm vertices, and let e:V(K)↪V(L)e:V(K)\hookrightarrow V(L)e:V(K)↪V(L) identify KKK with the full subcomplex of LLL spanned by e(V(K))e(V(K))e(V(K)), i.e. σ\sigmaσ is a face of KKK if and only if e(σ)e(\sigma)e(σ) is a face of LLL. Then for every degree qqq there is an injective additive homomorphism

Hq(ΩZK;Z)↪Hq(ΩZL;Z).H_q(\Omega\mathcal Z_K;\mathbb Z)\hookrightarrow H_q(\Omega\mathcal Z_L;\mathbb Z).Hq​(ΩZK​;Z)↪Hq​(ΩZL​;Z).

The coordinate inclusion ZK→ZL\mathcal Z_K\to\mathcal Z_LZK​→ZL​ (extend by 111 outside e(V(K))e(V(K))e(V(K))) and the coordinate projection ZL→ZK\mathcal Z_L\to\mathcal Z_KZL​→ZK​ 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 qqq, and the conclusion is an explicit injective additive homomorphism.

Preamble
import Definitions.Def_frame_2026_moment_angle_interfaces

open MomentAngle
Formal statement
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
Source
Standard property of full subcomplexes of polyhedral products, looped: see V. M. Buchstaber and T. E. Panov, Toric Topology, Mathematical Surveys and Monographs 204, AMS 2015, Section 4.2 for the retraction Z_K -> Z_{K_S}; a based retraction induces a retraction of based loop spaces.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me