What is the conjecture
In rational homotopy theory, the Halperin conjecture (formulated by Stephen Halperin in 1976) concerns the Serre spectral sequence of fibrations with certain fiber properties.
Let $F \to E \to B$ be a fibration where the fiber $F$ is an elliptic space with evenly graded cohomology (equivalently, with positive Euler characteristic $\chi(F) > 0$). The conjecture states that this fibration is TNCZ (totally non-homologous to zero), which means the induced map $H^(B) \to H^(F)$ is surjective in rational cohomology. Equivalently, the Serre spectral sequence associated to the fibration degenerates at the $E_2$-page.
An elliptic space is a simply connected space whose rational homotopy algebra (the minimal model) is a finite-dimensional, commutative, differential graded algebra over $\mathbb{Q}$.
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 5/5 (0 is best) (as of 2026-02-06)
Building blocks (1-3; from search results):
- Fibrations and fiber bundles (basic category theory and topology in Mathlib)
- Serre spectral sequences (available in Mathlib's homological algebra)
- Rational cohomology and differential graded algebras (partially in Mathlib)
Missing pieces (exactly 2; unclear/absent from search results):
- Rational homotopy theory infrastructure: formal definitions of elliptic spaces, minimal models, and the correspondence between spaces and commutative differential graded algebras over $\mathbb{Q}$
- Characterization of the TNCZ property in terms of spectral sequence degeneracy and explicit connection to formality and the Euler characteristic condition
Rating justification (1-2 sentences): The foundational concepts (fibrations, spectral sequences) exist in Mathlib, but the theory of rational homotopy, elliptic spaces, and their formal properties requires significant new infrastructure beyond what is currently available. The formalization would require developing a substantial portion of rational homotopy theory, particularly the minimal model machinery and formality conditions.
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link
What is the conjecture
In rational homotopy theory, the Halperin conjecture (formulated by Stephen Halperin in 1976) concerns the Serre spectral sequence of fibrations with certain fiber properties.
Let$F \to E \to B$ be a fibration where the fiber $F$ is an elliptic space with evenly graded cohomology (equivalently, with positive Euler characteristic $\chi(F) > 0$ ). The conjecture states that this fibration is TNCZ (totally non-homologous to zero), which means the induced map $H^(B) \to H^(F)$ is surjective in rational cohomology. Equivalently, the Serre spectral sequence associated to the fibration degenerates at the $E_2$ -page.
An elliptic space is a simply connected space whose rational homotopy algebra (the minimal model) is a finite-dimensional, commutative, differential graded algebra over$\mathbb{Q}$ .
(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)
Sources:
Prerequisites needed
Formalizability Rating: 5/5 (0 is best) (as of 2026-02-06)
Building blocks (1-3; from search results):
Missing pieces (exactly 2; unclear/absent from search results):
Rating justification (1-2 sentences): The foundational concepts (fibrations, spectral sequences) exist in Mathlib, but the theory of rational homotopy, elliptic spaces, and their formal properties requires significant new infrastructure beyond what is currently available. The formalization would require developing a substantial portion of rational homotopy theory, particularly the minimal model machinery and formality conditions.
AMS categories
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link