Derived solidification of free CW complexes (light condensed mathematics)
derived_solidification_free_CW_homology
Submitter: Dagur Asgeirsson.
Notes: Extracted from the LeanCondensed project, which develops Clausen–Scholze light condensed mathematics in Lean. The trusted part of the file defines light solid abelian groups (a light condensed abelian group is solid if 1 - shift acts invertibly on internal homs out of P = ℤ[ℕ∪{∞}]/ℤ[∞]) and shows the category of solid objects is abelian with an exact inclusion into light condensed abelian groups. The holes ask for the solidification functor with its adjunction, the derived solidification functor characterized as the total left derived functor of degreewise solidification, the derived adjunction, the CW-functor package identifying derived solidification of free light condensed abelian groups on CW complexes, and finally the comparison theorem: naturally in a CW complex X, the derived inclusion of the derived solidification of the free light condensed abelian group ℤ[X] is isomorphic in the derived category of light condensed abelian groups to the integral singular chains of X (homological degree n placed in cohomological degree -n), hence its homology is integral singular homology. The adjunctions, derived-functor property, and CW-functor specification pin the data holes down up to natural isomorphism, so the final theorem has its intended content.
Informal solution: Solidification exists by a light-condensed adjoint functor theorem (the solid objects form a reflective subcategory closed under limits and colimits). Derived solidification is the total left derived functor, which exists since the category of solid abelian groups has a compact projective generator. The natural derived comparison is the chain-level form of the same result: for a CW complex X, derived solidification of ℤ[X] identifies with the integral singular chains of X in the derived category of light condensed abelian groups; taking homology gives the pointwise statement. For the comparison: see Example 6.5 in https://arxiv.org/pdf/2605.03658
/-- **Hole 1.** The solidification functor, left adjoint to the inclusion of solid objects. -/
def declaration uses `sorry`solidification : LightCondAb ⥤ Solid := sorry/-- **Hole 2.** The solidification functor is additive. (This follows from the adjunction of the
next hole, but is needed as an instance to state the holes below.) -/
instance declaration uses `sorry`solidification_additive : solidification.Additive := sorry/-- **Hole 3.** The solidification adjunction: solidification is left adjoint to the inclusion of
solid objects in light condensed abelian groups. -/
def declaration uses `sorry`solidificationAdjunction : solidification ⊣ isSolid.ι := sorry/-- **Hole 4.** The derived solidification functor. -/
def declaration uses `sorry`derivedSolidification : DLightCondAb ⥤ DSolid := sorry/-- **Hole 5.** The comparison map from derived solidification to degreewise solidification. -/
def declaration uses `sorry`derivedSolidificationCounit :
DerivedCategory.Q ⋙ derivedSolidification ⟶
solidification.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q := sorry/-- **Hole 6.** Derived solidification, together with the comparison map of the previous hole, is
the total left derived functor of degreewise solidification followed by localization. -/
instance declaration uses `sorry`derivedSolidification_isLeftDerivedFunctor :
derivedSolidification.IsLeftDerivedFunctor derivedSolidificationCounit
(HomologicalComplex.quasiIso LightCondAb (ComplexShape.up ℤ)) := sorry/-- **Hole 7.** The derived solidification adjunction: derived solidification is left adjoint to
the derived inclusion. -/
def declaration uses `sorry`derivedSolidificationAdjunction : derivedSolidification ⊣ derivedInclusion :=
sorry/-- **Hole 8.** The functor sending a CW complex to the derived inclusion of the derived
solidification of the free light condensed abelian group on it. -/
def declaration uses `sorry`derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry/-- **Hole 9.** The specification identifying `derivedSolidificationFreeCWFunctor` with the
expected composite functor. -/
def declaration uses `sorry`derivedSolidificationFreeCWFunctorSpec :
derivedSolidificationFreeCWFunctor ≅
CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙
derivedSolidification ⋙ derivedInclusion := sorry/-- **Hole 10.** The derived comparison theorem, naturally in a CW complex `X`: after applying the
exact derived inclusion from solid light condensed abelian groups to light condensed abelian groups,
the derived solidification of the free light condensed abelian group on `X` is the integral singular
chain complex of `X` as a derived object of light condensed abelian groups. -/
def declaration uses `sorry`derivedSolidification_free_CW_derivedNatIso :
derivedSolidificationFreeCWFunctor ≅ singularChainsLightCondAbCWDerivedFunctor := sorry/-- **Hole 11.** For a CW complex `X`, the homology of the derived solidification of the free
light condensed abelian group on `X` is integral singular homology. Since the derived category
is cohomologically indexed, the `n`-th singular homology group occurs in degree `-n`. -/
def declaration uses `sorry`derivedSolidification_free_CW_homologyIso
(X : TopCat) [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) :
isSolid.ι.obj
((DerivedCategory.homologyFunctor Solid (-(n : ℤ))).obj
(derivedSolidification.obj
((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X)))) ≅
singularHomologyLightCondAb X n := sorry/-- **Hole 12.** The theorem form of `derivedSolidification_free_CW_homologyIso`: the derived
solidification of the free light condensed abelian group on a CW complex computes integral
singular homology. -/
theorem declaration uses `sorry`derivedSolidification_free_CW_homology
(X : TopCat) [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) :
Nonempty
(isSolid.ι.obj
((DerivedCategory.homologyFunctor Solid (-(n : ℤ))).obj
(derivedSolidification.obj
((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X)))) ≅
singularHomologyLightCondAb X n) := sorrySolved by
Not yet solved.