Algebraic and complex geometry · Result 052

Tangent splittings and product decompositions

2 papersLean

A splitting of the tangent bundle of a compact Kähler manifold into two integrable holomorphic subbundles induces a compatible product decomposition of its universal cover, proving the two-summand form of Beauville's splitting conjecture. On smooth rationally connected projective manifolds, both summands are automatically integrable, establishing Höring's conjecture and the corresponding product decomposition.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Universal-cover splitting for compact Kähler manifolds

OpenAI · September 23, 2026

We prove the two-summand form of Beauville's compatible splitting conjecture. If the tangent bundle of a compact connected Kähler manifold decomposes into two integrable holomorphic subbundles of positive rank, then its ordinary universal cover admits a product decomposition whose factor tangent bundles are the lifted specified summands.

Read PDF Download Source

Cite

@misc{OAI:Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026,
  author = {{OpenAI}},
  title = {{Universal-cover splitting for compact K"ahler manifolds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026/paper.pdf}{OAI:Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026}},
  year = {2026}
}

Integrability of split tangent bundles on rationally connected manifolds

OpenAI · September 23, 2026

We prove that both summands of every specified holomorphic splitting of the tangent bundle of a smooth rationally connected projective complex manifold into two positive-rank subbundles are integrable. This proves Höring's conjecture on rationally connected projective manifolds. Höring's product theorem then gives a product decomposition compatible with the specified splitting.

Read PDF Download Source

Cite

@misc{OAI:Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026,
  author = {{OpenAI}},
  title = {{Integrability of split tangent bundles on rationally connected manifolds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026/main.pdf}{OAI:Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The splitting question asks whether a holomorphic decomposition of the tangent bundle comes from a product decomposition of the universal cover. The formalized result gives an affirmative answer for a compact connected Kähler manifold whose tangent bundle splits into two positive-rank, integrable holomorphic subbundles. The universal cover is a product of connected simply connected complex manifolds of the prescribed dimensions, and the differential identifies the two tangent factors with the original summands.

Both integrability assumptions are required. Automatic integrability and the paper's additional corollaries are not included.

The formalization proves integrability of both summands in a holomorphic splitting of the tangent bundle of a rationally connected projective manifold. More precisely, for a compact connected complex manifold of dimension at least two with a projective embedding witnessing rational connectedness, each positive-rank summand of a holomorphic tangent-bundle splitting is integrable. The paper's compatible product decomposition is a separate consequence, outside this selected statement.

Comparator links

Result	Comparator statement
Universal-cover product splitting	KahlerSplitting.lean
Integrability of both holomorphic tangent summands	SplitTangentIntegrability.lean

Scope note on GitHub →