# Tangent splittings and product decompositions

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

- [Universal-cover splitting for compact Kähler manifolds](../../preprints/Universal-cover-splitting-for-compact-Kahler-manifolds-September-23-2026/paper.pdf)
- [Integrability of split tangent bundles on rationally connected manifolds](../../preprints/Integrability-of-split-tangent-bundles-on-rationally-connected-manifolds-September-23-2026/main.pdf)

## 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](../ComparatorChallenges/KahlerSplitting.lean) |
| Integrability of both holomorphic tangent summands | [SplitTangentIntegrability.lean](../ComparatorChallenges/SplitTangentIntegrability.lean) |