Add derived solidification of free CW complexes challenge (light condensed mathematics)

[dagurtomas]

This adds a new multi-hole problem, derived_solidification_free_CW_homology, extracted from the LeanCondensed project, which develops the light condensed mathematics of Clausen–Scholze in Lean.

The problem file develops, using only Mathlib imports, the definition of light solid abelian groups: a light condensed abelian group A is solid if 1 - shift acts invertibly on internal homs out of P = ℤ[ℕ∪{∞}]/ℤ[∞]. It then shows that the full subcategory Solid of solid objects is closed under limits, kernels, cokernels and finite products — hence abelian — and that the inclusion into light condensed abelian groups is exact, so it induces a functor on derived categories.

The challenge has nine holes:

• solidification — the solidification functor LightCondAb ⥤ Solid;
• solidification_additive — additivity of the solidification functor;
• solidificationAdjunction — solidification is left adjoint to the inclusion of solid objects;
• derivedSolidification — the derived solidification functor DerivedCategory LightCondAb ⥤ DerivedCategory Solid;
• derivedSolidificationCounit — the comparison map from derived solidification to degreewise solidification;
• derivedSolidification_isLeftDerivedFunctor — derived solidification is the total left derived functor of degreewise solidification;
• derivedSolidificationAdjunction — the derived adjunction with the derived inclusion;
• derivedSolidification_free_CW_derivedNatIso — naturally in a CW complex X, the derived
  inclusion of the derived solidification of ℤ[X] is isomorphic in the derived category of light
  condensed abelian groups to the integral singular chain complex of X, viewed as a complex of
  discrete light condensed abelian groups with homological degree n placed in cohomological
  degree -n, this is the main challenge;
• derivedSolidification_free_CW_homologyIso — for a CW complex X, the homology of the derived solidification of the free light condensed abelian group ℤ[X] is integral singular homology (in cohomological degree -n);
• derivedSolidification_free_CW_homology — the theorem form of the isomorphism.

The adjunctions and the derived-functor characterization pin the data holes down up to natural isomorphism, so the final comparison theorem has its intended mathematical content and cannot be satisfied by junk functors.

🤖 Generated with Claude Code