fix: require Hausdorff CW spaces for derived solidification

LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean

@@ -6,10 +6,13 @@ import EvalTools.Markers
 
 This challenge is extracted from the LeanCondensed project
 <https://github.com/dagurtomas/LeanCondensed>, which develops the theory of light condensed
-mathematics of Clausen–Scholze in Lean.  The target statement is the comparison theorem for a CW
-complex `X`: the homology of the derived solidification of the free light condensed abelian group
+mathematics of Clausen–Scholze in Lean.  The target statement is the comparison theorem for a Hausdorff
+CW complex `X`: the homology of the derived solidification of the free light condensed abelian group
 on `X` is integral singular homology.
 
+Mathlib's `Topology.CWComplex` does not include a Hausdorff assumption. We require it separately:
+without it, the CW predicate admits non-Hausdorff spaces for which the comparison fails.
+
 The non-`sorry` part of this file develops, using only Mathlib, the definition of
 *light solid abelian groups*: a light condensed abelian group `A` is solid if the map
 `1 - shift` on the free light condensed abelian group `P = ℤ[ℕ∪{∞}]/ℤ[∞]` induces an isomorphism
@@ -389,24 +392,26 @@ abbrev singularChainsLightCondAbDerivedFunctor : TopCat ⥤ DLightCondAb :=
 abbrev singularChainsLightCondAbDerived (X : TopCat) : DLightCondAb :=
   singularChainsLightCondAbDerivedFunctor.obj X
 
-/-- The property of topological spaces admitting a classical CW complex structure. -/
+/-- The property of Hausdorff spaces admitting a classical CW complex structure. -/
 abbrev isCWTopCat : ObjectProperty TopCat :=
-  fun X ↦ Nonempty (Topology.CWComplex (Set.univ : Set X))
+  fun X ↦ T2Space X ∧ Nonempty (Topology.CWComplex (Set.univ : Set X))
 
-/-- The full subcategory of topological spaces admitting a classical CW complex structure. -/
+/-- The full subcategory of Hausdorff spaces admitting a classical CW complex structure. -/
 abbrev CWTopCat : Type _ := isCWTopCat.FullSubcategory
 
 namespace CWTopCat
 
+instance (X : CWTopCat) : T2Space X.obj := X.property.1
+
 instance (X : CWTopCat) : Topology.CWComplex (Set.univ : Set X.obj) :=
-  Classical.choice X.property
+  Classical.choice X.property.2
 
 /-- The inclusion of CW spaces into topological spaces. -/
 abbrev toTopCat : CWTopCat ⥤ TopCat := isCWTopCat.ι
 
 end CWTopCat
 
-/-- **Hole 8.** The functor sending a CW complex to the derived inclusion of the derived
+/-- **Hole 8.** The functor sending a Hausdorff CW complex to the derived inclusion of the derived
 solidification of the free light condensed abelian group on it. -/
 @[eval_problem]
 def derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry
@@ -424,8 +429,8 @@ condensed abelian groups. -/
 abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb :=
   CWTopCat.toTopCat ⋙ singularChainsLightCondAbDerivedFunctor
 
-/-- **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,
+/-- **Hole 10.** The derived comparison theorem, naturally in a Hausdorff 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. -/
 @[eval_problem]
@@ -434,32 +439,32 @@ def derivedSolidification_free_CW_derivedNatIso :
 
 /-- The pointwise component of `derivedSolidification_free_CW_derivedNatIso`. -/
 def derivedSolidification_free_CW_derivedIso
-    (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] :
+    (X : TopCat) [T2Space X] [Topology.CWComplex (Set.univ : Set X)] :
     derivedInclusion.obj
       (derivedSolidification.obj
         ((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X))) ≅
       singularChainsLightCondAbDerived X :=
-  (derivedSolidificationFreeCWFunctorSpec.app ⟨X, ⟨inferInstance⟩⟩).symm.trans
-    (derivedSolidification_free_CW_derivedNatIso.app ⟨X, ⟨inferInstance⟩⟩)
+  (derivedSolidificationFreeCWFunctorSpec.app ⟨X, inferInstance, ⟨inferInstance⟩⟩).symm.trans
+    (derivedSolidification_free_CW_derivedNatIso.app ⟨X, inferInstance, ⟨inferInstance⟩⟩)
 
-/-- **Hole 11.** For a CW complex `X`, the homology of the derived solidification of the free
+/-- **Hole 11.** For a Hausdorff 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`. -/
 @[eval_problem]
 def derivedSolidification_free_CW_homologyIso
-    (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) :
+    (X : TopCat) [T2Space X] [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
+solidification of the free light condensed abelian group on a Hausdorff CW complex computes integral
 singular homology. -/
 @[eval_problem]
 theorem derivedSolidification_free_CW_homology
-    (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) :
+    (X : TopCat) [T2Space X] [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) :
     Nonempty
       (isSolid.ι.obj
         ((DerivedCategory.homologyFunctor Solid (-(n : ℤ))).obj

manifests/problems/derived_solidification_free_CW_homology.toml

@@ -3,16 +3,31 @@ title = "Derived solidification of free CW complexes (light condensed mathematic
 group = "formalization-evaluation"
 status = "active"
 visible = true
-statement_revision = 1
+statement_revision = 2
 tags = []
 module = "LeanEval.CondensedMathematics.DerivedSolidCWHomology"
 holes = ["LightCondensed.Solid.solidification", "LightCondensed.Solid.solidification_additive", "LightCondensed.Solid.solidificationAdjunction", "LightCondensed.Solid.derivedSolidification", "LightCondensed.Solid.derivedSolidificationCounit", "LightCondensed.Solid.derivedSolidification_isLeftDerivedFunctor", "LightCondensed.Solid.derivedSolidificationAdjunction", "LightCondensed.Solid.derivedSolidificationFreeCWFunctor", "LightCondensed.Solid.derivedSolidificationFreeCWFunctorSpec", "LightCondensed.Solid.derivedSolidification_free_CW_derivedNatIso", "LightCondensed.Solid.derivedSolidification_free_CW_homologyIso", "LightCondensed.Solid.derivedSolidification_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."
+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 Hausdorff 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."
 source = "https://github.com/dagurtomas/LeanCondensed (LeanCondensed/Projects/DerivedSolidCWHomology.lean); D. Clausen and P. Scholze, lectures on analytic stacks and light condensed mathematics.; P. Scholze, Lectures on Condensed Mathematics, https://arxiv.org/pdf/2605.03658"
-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"
+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 Hausdorff 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"
 
 [[status_history]]
 status = "active"
 effective_date = "2026-08-20"
 reason = "policy"
+
+# Preserve the original revision referenced by the frozen v1 set.
+[[revision_history]]
+revision = 1
+effective_date = "2026-08-20"
+reason = "initial"
+statement_digest = "sha256:f2b11dc906cbcc86cc15861c3cd8a301c48a8636701db73b5c8ea74a3f79e453"
+
+[[revision_history]]
+revision = 2
+effective_date = "2026-09-29"
+reason = "correction"
+# SHA-256 of the isCWTopCat declaration followed by the 12 marked hole signatures
+# (before :=), stripped and joined by two LF characters, with one final LF.
+statement_digest = "sha256:0aa3b25469e760068cd16fa4bd459270ad2397129e465d5817edac24f46ef34b"