From 1a39ff88b2fb3bfafcf7e7fa88dc1e8bd03ab6b9 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Thu, 2 Jul 2026 13:34:20 +0000 Subject: [PATCH 1/7] feat: add derived solidification of free CW complexes challenge Add a multi-hole problem extracted from the LeanCondensed project (light condensed mathematics of Clausen-Scholze). The trusted part of the file defines light solid abelian groups using only Mathlib and shows that they form an abelian category with an exact inclusion into light condensed abelian groups. The nine holes ask for the solidification functor with its adjunction, the derived solidification functor characterized as a total left derived functor, the derived adjunction, and the comparison theorem: for a CW complex X, the homology of the derived solidification of the free light condensed abelian group on X is integral singular homology. Co-Authored-By: Claude Fable 5 --- .../DerivedSolidCWHomology.lean | 388 ++++++++++++++++++ ...rived_solidification_free_CW_homology.toml | 9 + 2 files changed, 397 insertions(+) create mode 100644 LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean create mode 100644 manifests/problems/derived_solidification_free_CW_homology.toml diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean new file mode 100644 index 00000000..9d35deba --- /dev/null +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -0,0 +1,388 @@ +import Mathlib +import EvalTools.Markers + +/-! +# Derived solidification of free CW complexes + +This challenge is extracted from the LeanCondensed project +, 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 +on `X` is integral singular homology. + +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 +on internal homs into `A`. The full subcategory `Solid` of solid objects is closed under limits, +kernels, cokernels and finite products, hence abelian, and the inclusion into light condensed +abelian groups is exact, so it induces a functor on derived categories. + +The `sorry`ed declarations (the holes of this multi-hole problem) are: + +* `solidification` — the solidification functor `LightCondAb ⥤ Solid`; +* `solidification_additive` — additivity of the solidification functor; +* `solidificationAdjunction` — solidification is left adjoint to the inclusion; +* `derivedSolidification` — the derived solidification functor + `DerivedCategory LightCondAb ⥤ DerivedCategory Solid`; +* `derivedSolidificationCounit` — the comparison map exhibiting `derivedSolidification` as a + functor under degreewise solidification; +* `derivedSolidification_isLeftDerivedFunctor` — `derivedSolidification` is the total left + derived functor of degreewise solidification; +* `derivedSolidificationAdjunction` — derived solidification is left adjoint to the derived + inclusion; +* `derivedSolidification_free_CW_homologyIso` — for a CW complex `X`, the homology of the derived + solidification of `ℤ[X]` is integral singular homology (the derived category is cohomologically + indexed, so the `n`-th singular homology group appears in degree `-n`); +* `derivedSolidification_free_CW_homology` — the theorem form of the previous isomorphism. + +All holes must be filled compatibly: the adjunctions and derived functor property pin down +`solidification` and `derivedSolidification` up to natural isomorphism, so the final comparison +theorem has its intended mathematical content. + +Note that the LeanCondensed project contains significant progress towards some of the earlier holes +in this challenge. +-/ + +open CategoryTheory Limits LightProfinite OnePoint LightCondensed MonoidalCategory MonoidalClosed + +noncomputable section + +namespace LightProfinite + +/-- The shift map `ℕ∪{∞} ⟶ ℕ∪{∞}` sending `n` to `n + 1` and `∞` to `∞`. -/ +def shift : ℕ∪{∞} ⟶ ℕ∪{∞} := ConcreteCategory.ofHom { + toFun + | ∞ => ∞ + | OnePoint.some n => (n + 1 : ℕ) + continuous_toFun := by + rw [OnePoint.continuous_iff_from_nat, Filter.tendsto_add_atTop_iff_nat, tendsto_atTop_nhds] + intro U h hU + simp only [isOpen_iff_of_mem h, isClosed_discrete, isCompact_iff_finite, true_and] at hU + refine ⟨sSup (Option.some ⁻¹' U)ᶜ + 1, fun n hn ↦ by + simpa using! notMem_of_csSup_lt (Nat.succ_le_iff.mp hn) (Set.Finite.bddAbove hU)⟩ } + +end LightProfinite + +namespace LightCondensed + +/-- The inclusion of the point at infinity into `ℕ∪{∞}`. -/ +def ι : LightProfinite.of PUnit.{1} ⟶ ℕ∪{∞} := + ConcreteCategory.ofHom ⟨fun _ ↦ ∞, continuous_const⟩ + +/-- The inclusion of the point at infinity into `ℕ∪{∞}` is a split monomorphism. -/ +def ι_split : SplitMono ι where + retraction := ConcreteCategory.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩ + id := rfl + +/-- The map `ℤ[∞] ⟶ ℤ[ℕ∪{∞}]` of free light condensed abelian groups induced by `ι`. -/ +def P_map : + (free ℤ).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free ℤ).obj (ℕ∪{∞}).toCondensed := + (lightProfiniteToLightCondSet ⋙ free ℤ).map ι + +/-- The light condensed abelian group `P = ℤ[ℕ∪{∞}]/ℤ[∞]`. -/ +def P : LightCondAb := cokernel P_map + +/-- The projection `ℤ[ℕ∪{∞}] ⟶ P`. -/ +def P_proj : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ P := cokernel.π _ + +/-- The short complex `ℤ[∞] ⟶ ℤ[ℕ∪{∞}] ⟶ P`. -/ +def PSequence : ShortComplex LightCondAb := + ShortComplex.mk P_map P_proj (cokernel.condition _) + +/-- The short complex `ℤ[∞] ⟶ ℤ[ℕ∪{∞}] ⟶ P` is a short exact sequence. -/ +lemma PSequence_exact : PSequence.ShortExact := by + refine ShortComplex.ShortExact.mk' ?_ + (SplitMono.mono (ι_split.map (lightProfiniteToLightCondSet ⋙ free ℤ))) + coequalizer.π_epi + erw [ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, + ← kernel.condition P_proj] + rfl + +/-- The short exact sequence `ℤ[∞] ⟶ ℤ[ℕ∪{∞}] ⟶ P` splits. -/ +def PSequence_split : PSequence.Splitting := + ShortComplex.Splitting.ofExactOfRetraction _ + PSequence_exact.exact _ + (ι_split.map (lightProfiniteToLightCondSet ⋙ free ℤ)).id + coequalizer.π_epi + +/-- `P` is a retract of `ℤ[ℕ∪{∞}]`. -/ +def P_retract : Retract P ((free ℤ).obj (ℕ∪{∞}).toCondensed) where + i := _ + r := _ + retract := PSequence_split.s_g + +/-- Construct a map out of `P` from a map out of `ℤ[ℕ∪{∞}]` annihilating `ℤ[∞]`. -/ +def P_homMk (A : LightCondAb) (f : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ A) + (hf : P_map ≫ f = 0) : P ⟶ A := cokernel.desc _ f hf + +/-- The endomorphism `1 - shift` of the free light condensed abelian group `ℤ[ℕ∪{∞}]`. -/ +def oneMinusShift' : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ (free ℤ).obj (ℕ∪{∞}).toCondensed := + 𝟙 _ - (lightProfiniteToLightCondSet ⋙ free ℤ).map LightProfinite.shift + +set_option backward.isDefEq.respectTransparency false in +/-- The induced endomorphism `1 - shift` of `P = ℤ[ℕ∪{∞}]/ℤ[∞]`. -/ +def oneMinusShift : P ⟶ P := by + refine P_homMk _ oneMinusShift' ?_ ≫ P_proj + rw [oneMinusShift', Preadditive.comp_sub] + simp only [sub_eq_zero, P_map, ← Functor.map_comp] + rfl + +/-- A light condensed abelian group `A` is *solid* if the map `1 - shift` on `P` induces an +isomorphism on internal homs into `A`. -/ +def isSolid : ObjectProperty LightCondAb := + fun A ↦ IsIso ((MonoidalClosed.pre oneMinusShift).app A) + +/-- The class expressing that a light condensed abelian group is solid. -/ +abbrev IsSolid (A : LightCondAb) := isSolid.Is A + +/-- The category of light solid abelian groups, as the full subcategory of solid objects in light +condensed abelian groups. -/ +abbrev Solid : Type _ := isSolid.FullSubcategory + +namespace Solid + +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +/-- Solid objects are closed under limits, because internal homs out of a fixed object preserve +limits in the second variable. -/ +instance (J : Type) [SmallCategory J] : isSolid.IsClosedUnderLimitsOfShape J := by + have : PreservesLimitsOfSize.{0, 0} (ihom P) := + (ihom.adjunction P).rightAdjoint_preservesLimits + apply ObjectProperty.IsClosedUnderLimitsOfShape.mk + intro A ⟨⟨F, π, hl⟩, h⟩ + let hl' := isLimitOfPreserves (ihom P) hl + let α := F.whiskerLeft <| MonoidalClosed.pre oneMinusShift + have : IsIso α := by + rw [NatTrans.isIso_iff_isIso_app] + intro j + exact h j + let c := (Cone.postcompose α).obj ((ihom P).mapCone ⟨A, π⟩) + have : hl'.lift c = (MonoidalClosed.pre oneMinusShift).app A := by + apply hl'.hom_ext + intro j + change _ ≫ ((ihom P).mapCone ⟨A, π⟩).π.app _ = _ + simp only [Functor.comp_obj, Functor.const_obj_obj, IsLimit.fac] + simp only [Functor.mapCone_pt, Functor.mapCone_π_app] + simp only [MonoidalClosed.pre, Cone.postcompose_obj_pt, Functor.mapCone_pt, + Cone.postcompose_obj_π, NatTrans.comp_app, Functor.const_obj_obj, Functor.comp_obj, + Functor.mapCone_π_app, Functor.whiskerLeft_app, conjugateEquiv_apply_app, + curriedTensor_obj_obj, ihom.ihom_adjunction_unit, curriedTensor_map_app, + ihom.ihom_adjunction_counit, ← Functor.map_comp, ihom.coev_naturality_assoc, Category.assoc, + ← ihom.ev_naturality, Functor.id_obj, c, α] + rw [← whisker_exchange_assoc] + rw [isSolid, ← this, ← IsLimit.nonempty_isLimit_iff_isIso_lift] + exact ⟨(IsLimit.postcomposeHomEquiv (asIso α) _).symm hl'⟩ + +set_option backward.defeqAttrib.useBackward true in +set_option backward.isDefEq.respectTransparency false in +/-- Solid objects are closed under colimits of any shape for which internal homs out of `P` +preserve colimits. -/ +instance (J : Type) [SmallCategory J] [PreservesColimitsOfShape J (ihom P)] : + isSolid.IsClosedUnderColimitsOfShape J := by + apply ObjectProperty.IsClosedUnderColimitsOfShape.mk + intro A ⟨⟨F, ι, hc⟩, h⟩ + let hc' := isColimitOfPreserves (ihom P) hc + let α := F.whiskerLeft <| MonoidalClosed.pre oneMinusShift + have : IsIso α := by + rw [NatTrans.isIso_iff_isIso_app] + intro j + exact h j + let c := (Cocone.precompose α).obj ((ihom P).mapCocone ⟨A, ι⟩) + have hdesc : hc'.desc c = (MonoidalClosed.pre oneMinusShift).app A := by + apply hc'.hom_ext + intro j + simp only [IsColimit.fac] + simp only [Functor.mapCocone_pt, Functor.mapCocone_ι_app] + simp only [MonoidalClosed.pre, Cocone.precompose_obj_pt, Functor.mapCocone_pt, + Cocone.precompose_obj_ι, NatTrans.comp_app, Functor.const_obj_obj, Functor.comp_obj, + Functor.mapCocone_ι_app, Functor.whiskerLeft_app, conjugateEquiv_apply_app, + curriedTensor_obj_obj, ihom.ihom_adjunction_unit, curriedTensor_map_app, + ihom.ihom_adjunction_counit, ← Functor.map_comp, ihom.coev_naturality_assoc, Category.assoc, + ← ihom.ev_naturality, Functor.id_obj, c, α] + rw [← whisker_exchange_assoc] + rw [isSolid, ← hdesc, ← IsColimit.nonempty_isColimit_iff_isIso_desc hc'] + exact ⟨(IsColimit.precomposeHomEquiv (asIso α) _).symm hc'⟩ + +/-- The free light condensed abelian group `ℤ[ℕ∪{∞}]` is internally projective. -/ +instance : InternallyProjective ((free ℤ).obj (ℕ∪{∞}).toCondensed) := + internallyProjective_free_natUnionInfty ℤ + +/-- `P` is internally projective, being a retract of `ℤ[ℕ∪{∞}]`. -/ +instance : InternallyProjective P := .ofRetract P_retract + +/-- Internal homs out of `P` form an additive functor. -/ +instance : (ihom P).Additive := by + have h : PreservesColimitsOfSize.{0, 0} (tensorLeft P) := + (ihom.adjunction P).leftAdjoint_preservesColimits + have : PreservesColimitsOfShape (Discrete WalkingPair) (tensorLeft P) := + h.preservesColimitsOfShape + have : PreservesBinaryBiproducts (tensorLeft P) := + preservesBinaryBiproducts_of_preservesBinaryCoproducts _ + have : (tensorLeft P).Additive := Functor.additive_of_preservesBinaryBiproducts _ + exact (ihom.adjunction P).right_adjoint_additive + +/-- Internal homs out of the internally projective object `P` preserve finite colimits. -/ +instance : PreservesFiniteColimits (ihom P) := by + have : PreservesLimitsOfSize.{0, 0} (ihom P) := + (ihom.adjunction P).rightAdjoint_preservesLimits + rw [Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi] + intro S hS + haveI : Epi S.g := hS.epi_g + exact ⟨((Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono (ihom P)).1 + inferInstance S hS).1, inferInstance⟩ + +/-- Solid objects are closed under kernels. -/ +instance : isSolid.IsClosedUnderKernels where + kernels_le := by + rintro _ ⟨_, k, hk, hf⟩ + exact isSolid.prop_of_isLimit hk (by rintro (_ | _) <;> first | exact hf.1 | exact hf.2) + +/-- Solid objects are closed under cokernels. -/ +instance : isSolid.IsClosedUnderCokernels where + cokernels_le := by + rintro _ ⟨_, k, hk, hf⟩ + exact isSolid.prop_of_isColimit hk (by rintro (_ | _) <;> first | exact hf.1 | exact hf.2) + +/-- Solid objects are closed under finite products. -/ +instance : isSolid.IsClosedUnderFiniteProducts where + isClosedUnderLimitsOfShape _ _ := inferInstance + +/-- The zero object is solid. -/ +instance : isSolid.ContainsZero where + exists_zero := by + obtain ⟨Z, hZ⟩ := HasZeroObject.zero (C := LightCondAb) + refine ⟨Z, hZ, ?_⟩ + have hz : IsZero ((ihom P).obj Z) := (ihom P).map_isZero hZ + have h : (MonoidalClosed.pre oneMinusShift).app Z = (hz.iso hz).hom := hz.eq_of_src _ _ + show IsIso ((MonoidalClosed.pre oneMinusShift).app Z) + rw [h] + infer_instance + +/-- The category of light solid abelian groups is abelian. -/ +instance : Abelian Solid := inferInstanceAs (Abelian isSolid.FullSubcategory) + +/-- The inclusion of solid objects preserves finite limits. -/ +instance : PreservesFiniteLimits isSolid.ι where + preservesFiniteLimits _ := inferInstance + +/-- The inclusion of solid objects preserves finite colimits. -/ +instance : PreservesFiniteColimits isSolid.ι where + preservesFiniteColimits _ := inferInstance + +/-- A choice of derived category of light condensed abelian groups. -/ +instance instHasDerivedCategoryLightCondAb : HasDerivedCategory LightCondAb := + HasDerivedCategory.standard _ + +/-- A choice of derived category of light solid abelian groups. -/ +instance instHasDerivedCategorySolid : HasDerivedCategory Solid := + HasDerivedCategory.standard _ + +/-- The derived category of light condensed abelian groups. -/ +abbrev DLightCondAb := DerivedCategory LightCondAb + +/-- The derived category of light solid abelian groups. -/ +abbrev DSolid := DerivedCategory Solid + +/-- **Hole 1.** The solidification functor, left adjoint to the inclusion of solid objects. -/ +@[eval_problem] +noncomputable def 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.) -/ +@[eval_problem] +instance 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. -/ +@[eval_problem] +noncomputable def solidificationAdjunction : solidification ⊣ isSolid.ι := sorry + +/-- **Hole 4.** The derived solidification functor. -/ +@[eval_problem] +noncomputable def derivedSolidification : DLightCondAb ⥤ DSolid := sorry + +/-- **Hole 5.** The comparison map from derived solidification to degreewise solidification. -/ +@[eval_problem] +noncomputable def 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. -/ +@[eval_problem] +instance derivedSolidification_isLeftDerivedFunctor : + derivedSolidification.IsLeftDerivedFunctor derivedSolidificationCounit + (HomologicalComplex.quasiIso LightCondAb (ComplexShape.up ℤ)) := sorry + +/-- The inclusion of solid abelian groups, applied degreewise to cochain complexes. -/ +noncomputable abbrev inclusionComplexes : + CochainComplex Solid ℤ ⥤ CochainComplex LightCondAb ℤ := + isSolid.ι.mapHomologicalComplex (ComplexShape.up ℤ) + +/-- The exact functor on derived categories induced by the inclusion `Solid ⥤ LightCondAb`. -/ +noncomputable abbrev derivedInclusion : DSolid ⥤ DLightCondAb := + isSolid.ι.mapDerivedCategory + +/-- The derived inclusion is induced by applying the inclusion degreewise to complexes. -/ +noncomputable abbrev derivedInclusionFactors : + DerivedCategory.Q ⋙ derivedInclusion ≅ inclusionComplexes ⋙ DerivedCategory.Q := + isSolid.ι.mapDerivedCategoryFactors + +/-- The comparison map exhibiting `derivedInclusion` as a right derived functor of the degreewise +inclusion. -/ +noncomputable abbrev derivedInclusionComparison : + inclusionComplexes ⋙ DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ derivedInclusion := + derivedInclusionFactors.inv + +/-- The exact derived inclusion is the right derived functor of the degreewise inclusion. -/ +instance derivedInclusion_isRightDerivedFunctor : + derivedInclusion.IsRightDerivedFunctor derivedInclusionComparison + (HomologicalComplex.quasiIso Solid (ComplexShape.up ℤ)) := + Functor.isRightDerivedFunctor_of_inverts + (HomologicalComplex.quasiIso Solid (ComplexShape.up ℤ)) derivedInclusion + derivedInclusionFactors + +/-- **Hole 7.** The derived solidification adjunction: derived solidification is left adjoint to +the derived inclusion. -/ +@[eval_problem] +noncomputable def derivedSolidificationAdjunction : derivedSolidification ⊣ derivedInclusion := + sorry + +/-- The free light condensed abelian group on a topological space. -/ +noncomputable abbrev freeLightCondAbOfTop (X : TopCat) : LightCondAb := + (free ℤ).obj X.toLightCondSet + +/-- Integral singular homology of a topological space, viewed as a discrete light condensed +abelian group. -/ +noncomputable abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := + (LightCondensed.discrete (ModuleCat ℤ)).obj + (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) + +/-- **Hole 8.** 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`. -/ +@[eval_problem] +noncomputable def 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 9.** 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. -/ +@[eval_problem] +theorem 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) := sorry + +end Solid + +end LightCondensed diff --git a/manifests/problems/derived_solidification_free_CW_homology.toml b/manifests/problems/derived_solidification_free_CW_homology.toml new file mode 100644 index 00000000..8d5d4e40 --- /dev/null +++ b/manifests/problems/derived_solidification_free_CW_homology.toml @@ -0,0 +1,9 @@ +id = "derived_solidification_free_CW_homology" +title = "Derived solidification of free CW complexes (light condensed mathematics)" +test = false +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.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, and finally the comparison theorem: 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). The adjunctions and derived-functor property 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." +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 light condensed abelian groups have enough objects adapted to solidification (e.g. complexes of direct sums of ℤ[S] for light profinite S). For the comparison: ℤ[X] for a CW complex X is (locally on the CW structure) a complex of discrete objects; discrete light condensed abelian groups are already solid and adapted to solidification, so the derived solidification of the single complex ℤ[X] is computed by the cellular/singular chain complex of X, whose homology is singular homology, placed in cohomological degree -n." From ce7c8e8bc982497223df5f1851e5a9259db05c3f Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Thu, 2 Jul 2026 13:47:43 +0000 Subject: [PATCH 2/7] fix informal solution --- manifests/problems/derived_solidification_free_CW_homology.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manifests/problems/derived_solidification_free_CW_homology.toml b/manifests/problems/derived_solidification_free_CW_homology.toml index 8d5d4e40..caca0b16 100644 --- a/manifests/problems/derived_solidification_free_CW_homology.toml +++ b/manifests/problems/derived_solidification_free_CW_homology.toml @@ -6,4 +6,4 @@ holes = ["LightCondensed.Solid.solidification", "LightCondensed.Solid.solidifica 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, and finally the comparison theorem: 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). The adjunctions and derived-functor property 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." -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 light condensed abelian groups have enough objects adapted to solidification (e.g. complexes of direct sums of ℤ[S] for light profinite S). For the comparison: ℤ[X] for a CW complex X is (locally on the CW structure) a complex of discrete objects; discrete light condensed abelian groups are already solid and adapted to solidification, so the derived solidification of the single complex ℤ[X] is computed by the cellular/singular chain complex of X, whose homology is singular homology, placed in cohomological degree -n." +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. For the comparison: see Example 6.5 in https://arxiv.org/pdf/2605.03658" From f6b39517b70a08142c47b57d240ea2eadafc90b3 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Thu, 2 Jul 2026 13:48:32 +0000 Subject: [PATCH 3/7] fix reference --- manifests/problems/derived_solidification_free_CW_homology.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manifests/problems/derived_solidification_free_CW_homology.toml b/manifests/problems/derived_solidification_free_CW_homology.toml index caca0b16..6ce5f33b 100644 --- a/manifests/problems/derived_solidification_free_CW_homology.toml +++ b/manifests/problems/derived_solidification_free_CW_homology.toml @@ -5,5 +5,5 @@ 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.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, and finally the comparison theorem: 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). The adjunctions and derived-functor property 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." +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. For the comparison: see Example 6.5 in https://arxiv.org/pdf/2605.03658" From 8e797efa4d28a9420ec13eafb699b09e6d654d37 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Thu, 2 Jul 2026 15:46:06 +0000 Subject: [PATCH 4/7] add actual iso of derived objects --- .../DerivedSolidCWHomology.lean | 80 ++++++++++++++++++- ...rived_solidification_free_CW_homology.toml | 6 +- 2 files changed, 79 insertions(+), 7 deletions(-) diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index 9d35deba..81f10282 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -30,14 +30,19 @@ The `sorry`ed declarations (the holes of this multi-hole problem) are: derived functor of degreewise solidification; * `derivedSolidificationAdjunction` — derived solidification is left adjoint to 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 `ℤ[X]` is integral singular homology (the derived category is cohomologically indexed, so the `n`-th singular homology group appears in degree `-n`); * `derivedSolidification_free_CW_homology` — the theorem form of the previous isomorphism. All holes must be filled compatibly: the adjunctions and derived functor property pin down -`solidification` and `derivedSolidification` up to natural isomorphism, so the final comparison -theorem has its intended mathematical content. +`solidification` and `derivedSolidification` up to natural isomorphism, so the final derived +comparison theorem and its pointwise homology form have their intended mathematical content. Note that the LeanCondensed project contains significant progress towards some of the earlier holes in this challenge. @@ -352,13 +357,80 @@ noncomputable def derivedSolidificationAdjunction : derivedSolidification ⊣ de noncomputable abbrev freeLightCondAbOfTop (X : TopCat) : LightCondAb := (free ℤ).obj X.toLightCondSet +/-- The free light condensed abelian group on a topological space, functorially in the space. -/ +noncomputable abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb := + topCatToLightCondSet ⋙ free ℤ + /-- Integral singular homology of a topological space, viewed as a discrete light condensed abelian group. -/ noncomputable abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := (LightCondensed.discrete (ModuleCat ℤ)).obj (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) -/-- **Hole 8.** For a CW complex `X`, the homology of the derived solidification of the free +/-- The integral singular chain complex of a topological space, viewed as a cochain complex of +light condensed abelian groups by applying the discrete functor degreewise and placing homological +chain degree `n` in cohomological degree `-n`. -/ +noncomputable abbrev singularChainsLightCondAbComplexFunctor : + TopCat ⥤ CochainComplex LightCondAb ℤ := + ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ + (LightCondensed.discrete (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.down ℕ) ⋙ + ComplexShape.embeddingDownNat.extendFunctor LightCondAb + +/-- The integral singular chain complex of a topological space as an object of the derived category +of light condensed abelian groups. -/ +noncomputable abbrev singularChainsLightCondAbDerivedFunctor : TopCat ⥤ DLightCondAb := + singularChainsLightCondAbComplexFunctor ⋙ DerivedCategory.Q + +/-- The integral singular chain complex of a topological space as a derived object. -/ +noncomputable abbrev singularChainsLightCondAbDerived (X : TopCat) : DLightCondAb := + singularChainsLightCondAbDerivedFunctor.obj X + +/-- The property of topological spaces admitting a classical CW complex structure. -/ +abbrev isCWTopCat : ObjectProperty TopCat := + fun X ↦ Nonempty (Topology.CWComplex (Set.univ : Set X)) + +/-- The full subcategory of topological spaces admitting a classical CW complex structure. -/ +abbrev CWTopCat : Type _ := isCWTopCat.FullSubcategory + +namespace CWTopCat + +noncomputable instance (X : CWTopCat) : Topology.CWComplex (Set.univ : Set X.obj) := + Classical.choice X.property + +/-- The inclusion of CW spaces into topological spaces. -/ +abbrev toTopCat : CWTopCat ⥤ TopCat := isCWTopCat.ι + +end CWTopCat + +/-- The functor sending a CW complex to the derived inclusion of the derived solidification of the +free light condensed abelian group on it. -/ +noncomputable abbrev derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := + CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙ + derivedSolidification ⋙ derivedInclusion + +/-- The integral singular chains functor on CW complexes, viewed in the derived category of light +condensed abelian groups. -/ +noncomputable abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb := + CWTopCat.toTopCat ⋙ singularChainsLightCondAbDerivedFunctor + +/-- **Hole 8.** 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. -/ +@[eval_problem] +noncomputable def derivedSolidification_free_CW_derivedNatIso : + derivedSolidificationFreeCWFunctor ≅ singularChainsLightCondAbCWDerivedFunctor := sorry + +/-- The pointwise component of `derivedSolidification_free_CW_derivedNatIso`. -/ +noncomputable def derivedSolidification_free_CW_derivedIso + (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] : + derivedInclusion.obj + (derivedSolidification.obj + ((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X))) ≅ + singularChainsLightCondAbDerived X := + derivedSolidification_free_CW_derivedNatIso.app ⟨X, ⟨inferInstance⟩⟩ + +/-- **Hole 9.** 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`. -/ @[eval_problem] @@ -370,7 +442,7 @@ noncomputable def derivedSolidification_free_CW_homologyIso ((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X)))) ≅ singularHomologyLightCondAb X n := sorry -/-- **Hole 9.** The theorem form of `derivedSolidification_free_CW_homologyIso`: the derived +/-- **Hole 10.** 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. -/ @[eval_problem] diff --git a/manifests/problems/derived_solidification_free_CW_homology.toml b/manifests/problems/derived_solidification_free_CW_homology.toml index 6ce5f33b..f9b67980 100644 --- a/manifests/problems/derived_solidification_free_CW_homology.toml +++ b/manifests/problems/derived_solidification_free_CW_homology.toml @@ -2,8 +2,8 @@ id = "derived_solidification_free_CW_homology" title = "Derived solidification of free CW complexes (light condensed mathematics)" test = false 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.derivedSolidification_free_CW_homologyIso", "LightCondensed.Solid.derivedSolidification_free_CW_homology"] +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.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, and finally the comparison theorem: 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). The adjunctions and derived-functor property 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, 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 and derived-functor property 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. 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 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" From 1634ceb12687f98a071d2bc521c4e5d5f49c4485 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Fri, 3 Jul 2026 08:46:04 +0000 Subject: [PATCH 5/7] fix derived solidification challenge holes --- .../DerivedSolidCWHomology.lean | 30 +++++++++++++------ ...rived_solidification_free_CW_homology.toml | 4 +-- 2 files changed, 23 insertions(+), 11 deletions(-) diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index 81f10282..418235ca 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -30,6 +30,10 @@ The `sorry`ed declarations (the holes of this multi-hole problem) are: derived functor of degreewise solidification; * `derivedSolidificationAdjunction` — derived solidification is left adjoint to the derived inclusion; +* `derivedSolidificationFreeCWFunctor` — the functor on CW complexes whose values are the derived + inclusion of the derived solidification of the free light condensed abelian group; +* `derivedSolidificationFreeCWFunctorSpec` — an isomorphism identifying + `derivedSolidificationFreeCWFunctor` with the expected composite functor; * `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 @@ -402,18 +406,25 @@ abbrev toTopCat : CWTopCat ⥤ TopCat := isCWTopCat.ι end CWTopCat -/-- The functor sending a CW complex to the derived inclusion of the derived solidification of the -free light condensed abelian group on it. -/ -noncomputable abbrev derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := - CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙ - derivedSolidification ⋙ derivedInclusion +/-- **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. -/ +@[eval_problem] +noncomputable abbrev derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry + +/-- **Hole 9.** The specification identifying `derivedSolidificationFreeCWFunctor` with the +expected composite functor. -/ +@[eval_problem] +noncomputable abbrev derivedSolidificationFreeCWFunctorSpec : + derivedSolidificationFreeCWFunctor ≅ + CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙ + derivedSolidification ⋙ derivedInclusion := sorry /-- The integral singular chains functor on CW complexes, viewed in the derived category of light condensed abelian groups. -/ noncomputable abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb := CWTopCat.toTopCat ⋙ singularChainsLightCondAbDerivedFunctor -/-- **Hole 8.** The derived comparison theorem, naturally in a CW complex `X`: after applying the +/-- **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. -/ @@ -428,9 +439,10 @@ noncomputable def derivedSolidification_free_CW_derivedIso (derivedSolidification.obj ((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X))) ≅ singularChainsLightCondAbDerived X := - derivedSolidification_free_CW_derivedNatIso.app ⟨X, ⟨inferInstance⟩⟩ + (derivedSolidificationFreeCWFunctorSpec.app ⟨X, ⟨inferInstance⟩⟩).symm.trans + (derivedSolidification_free_CW_derivedNatIso.app ⟨X, ⟨inferInstance⟩⟩) -/-- **Hole 9.** For a CW complex `X`, the homology of the derived solidification of the free +/-- **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`. -/ @[eval_problem] @@ -442,7 +454,7 @@ noncomputable def derivedSolidification_free_CW_homologyIso ((DerivedCategory.singleFunctor LightCondAb 0).obj (freeLightCondAbOfTop X)))) ≅ singularHomologyLightCondAb X n := sorry -/-- **Hole 10.** The theorem form of `derivedSolidification_free_CW_homologyIso`: the derived +/-- **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. -/ @[eval_problem] diff --git a/manifests/problems/derived_solidification_free_CW_homology.toml b/manifests/problems/derived_solidification_free_CW_homology.toml index f9b67980..7020eb0d 100644 --- a/manifests/problems/derived_solidification_free_CW_homology.toml +++ b/manifests/problems/derived_solidification_free_CW_homology.toml @@ -2,8 +2,8 @@ id = "derived_solidification_free_CW_homology" title = "Derived solidification of free CW complexes (light condensed mathematics)" test = false 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.derivedSolidification_free_CW_derivedNatIso", "LightCondensed.Solid.derivedSolidification_free_CW_homologyIso", "LightCondensed.Solid.derivedSolidification_free_CW_homology"] +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, 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 and derived-functor property 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 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" From a1d3943c235a1c630c9b36386bab13a9e9c2a8cb Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Sat, 4 Jul 2026 22:08:00 +0000 Subject: [PATCH 6/7] fix --- LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index 418235ca..eaefbfbc 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -409,12 +409,12 @@ end CWTopCat /-- **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. -/ @[eval_problem] -noncomputable abbrev derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry +noncomputable def derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry /-- **Hole 9.** The specification identifying `derivedSolidificationFreeCWFunctor` with the expected composite functor. -/ @[eval_problem] -noncomputable abbrev derivedSolidificationFreeCWFunctorSpec : +noncomputable def derivedSolidificationFreeCWFunctorSpec : derivedSolidificationFreeCWFunctor ≅ CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙ derivedSolidification ⋙ derivedInclusion := sorry From 87894fa1cad4d6ad89eece4c8eb669658ebfd2c3 Mon Sep 17 00:00:00 2001 From: Dagur Asgeirsson Date: Sun, 12 Jul 2026 12:13:53 +0000 Subject: [PATCH 7/7] fix? --- .../DerivedSolidCWHomology.lean | 46 ++++++++++--------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean index eaefbfbc..1eea3978 100644 --- a/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean +++ b/LeanEval/CondensedMathematics/DerivedSolidCWHomology.lean @@ -294,7 +294,7 @@ abbrev DSolid := DerivedCategory Solid /-- **Hole 1.** The solidification functor, left adjoint to the inclusion of solid objects. -/ @[eval_problem] -noncomputable def solidification : LightCondAb ⥤ Solid := sorry +def 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.) -/ @@ -304,15 +304,15 @@ instance 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. -/ @[eval_problem] -noncomputable def solidificationAdjunction : solidification ⊣ isSolid.ι := sorry +def solidificationAdjunction : solidification ⊣ isSolid.ι := sorry /-- **Hole 4.** The derived solidification functor. -/ @[eval_problem] -noncomputable def derivedSolidification : DLightCondAb ⥤ DSolid := sorry +def derivedSolidification : DLightCondAb ⥤ DSolid := sorry /-- **Hole 5.** The comparison map from derived solidification to degreewise solidification. -/ @[eval_problem] -noncomputable def derivedSolidificationCounit : +def derivedSolidificationCounit : DerivedCategory.Q ⋙ derivedSolidification ⟶ solidification.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q := sorry @@ -324,22 +324,22 @@ instance derivedSolidification_isLeftDerivedFunctor : (HomologicalComplex.quasiIso LightCondAb (ComplexShape.up ℤ)) := sorry /-- The inclusion of solid abelian groups, applied degreewise to cochain complexes. -/ -noncomputable abbrev inclusionComplexes : +abbrev inclusionComplexes : CochainComplex Solid ℤ ⥤ CochainComplex LightCondAb ℤ := isSolid.ι.mapHomologicalComplex (ComplexShape.up ℤ) /-- The exact functor on derived categories induced by the inclusion `Solid ⥤ LightCondAb`. -/ -noncomputable abbrev derivedInclusion : DSolid ⥤ DLightCondAb := +abbrev derivedInclusion : DSolid ⥤ DLightCondAb := isSolid.ι.mapDerivedCategory /-- The derived inclusion is induced by applying the inclusion degreewise to complexes. -/ -noncomputable abbrev derivedInclusionFactors : +abbrev derivedInclusionFactors : DerivedCategory.Q ⋙ derivedInclusion ≅ inclusionComplexes ⋙ DerivedCategory.Q := isSolid.ι.mapDerivedCategoryFactors /-- The comparison map exhibiting `derivedInclusion` as a right derived functor of the degreewise inclusion. -/ -noncomputable abbrev derivedInclusionComparison : +abbrev derivedInclusionComparison : inclusionComplexes ⋙ DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ derivedInclusion := derivedInclusionFactors.inv @@ -354,27 +354,27 @@ instance derivedInclusion_isRightDerivedFunctor : /-- **Hole 7.** The derived solidification adjunction: derived solidification is left adjoint to the derived inclusion. -/ @[eval_problem] -noncomputable def derivedSolidificationAdjunction : derivedSolidification ⊣ derivedInclusion := +def derivedSolidificationAdjunction : derivedSolidification ⊣ derivedInclusion := sorry /-- The free light condensed abelian group on a topological space. -/ -noncomputable abbrev freeLightCondAbOfTop (X : TopCat) : LightCondAb := +abbrev freeLightCondAbOfTop (X : TopCat) : LightCondAb := (free ℤ).obj X.toLightCondSet /-- The free light condensed abelian group on a topological space, functorially in the space. -/ -noncomputable abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb := +abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb := topCatToLightCondSet ⋙ free ℤ /-- Integral singular homology of a topological space, viewed as a discrete light condensed abelian group. -/ -noncomputable abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := +abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb := (LightCondensed.discrete (ModuleCat ℤ)).obj (((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X) /-- The integral singular chain complex of a topological space, viewed as a cochain complex of light condensed abelian groups by applying the discrete functor degreewise and placing homological chain degree `n` in cohomological degree `-n`. -/ -noncomputable abbrev singularChainsLightCondAbComplexFunctor : +abbrev singularChainsLightCondAbComplexFunctor : TopCat ⥤ CochainComplex LightCondAb ℤ := ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙ (LightCondensed.discrete (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.down ℕ) ⋙ @@ -382,11 +382,11 @@ noncomputable abbrev singularChainsLightCondAbComplexFunctor : /-- The integral singular chain complex of a topological space as an object of the derived category of light condensed abelian groups. -/ -noncomputable abbrev singularChainsLightCondAbDerivedFunctor : TopCat ⥤ DLightCondAb := +abbrev singularChainsLightCondAbDerivedFunctor : TopCat ⥤ DLightCondAb := singularChainsLightCondAbComplexFunctor ⋙ DerivedCategory.Q /-- The integral singular chain complex of a topological space as a derived object. -/ -noncomputable abbrev singularChainsLightCondAbDerived (X : TopCat) : DLightCondAb := +abbrev singularChainsLightCondAbDerived (X : TopCat) : DLightCondAb := singularChainsLightCondAbDerivedFunctor.obj X /-- The property of topological spaces admitting a classical CW complex structure. -/ @@ -398,7 +398,7 @@ abbrev CWTopCat : Type _ := isCWTopCat.FullSubcategory namespace CWTopCat -noncomputable instance (X : CWTopCat) : Topology.CWComplex (Set.univ : Set X.obj) := +instance (X : CWTopCat) : Topology.CWComplex (Set.univ : Set X.obj) := Classical.choice X.property /-- The inclusion of CW spaces into topological spaces. -/ @@ -409,19 +409,19 @@ end CWTopCat /-- **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. -/ @[eval_problem] -noncomputable def derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry +def derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb := sorry /-- **Hole 9.** The specification identifying `derivedSolidificationFreeCWFunctor` with the expected composite functor. -/ @[eval_problem] -noncomputable def derivedSolidificationFreeCWFunctorSpec : +def derivedSolidificationFreeCWFunctorSpec : derivedSolidificationFreeCWFunctor ≅ CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙ derivedSolidification ⋙ derivedInclusion := sorry /-- The integral singular chains functor on CW complexes, viewed in the derived category of light condensed abelian groups. -/ -noncomputable abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb := +abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb := CWTopCat.toTopCat ⋙ singularChainsLightCondAbDerivedFunctor /-- **Hole 10.** The derived comparison theorem, naturally in a CW complex `X`: after applying the @@ -429,11 +429,11 @@ exact derived inclusion from solid light condensed abelian groups to light conde 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] -noncomputable def derivedSolidification_free_CW_derivedNatIso : +def derivedSolidification_free_CW_derivedNatIso : derivedSolidificationFreeCWFunctor ≅ singularChainsLightCondAbCWDerivedFunctor := sorry /-- The pointwise component of `derivedSolidification_free_CW_derivedNatIso`. -/ -noncomputable def derivedSolidification_free_CW_derivedIso +def derivedSolidification_free_CW_derivedIso (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] : derivedInclusion.obj (derivedSolidification.obj @@ -446,7 +446,7 @@ noncomputable def derivedSolidification_free_CW_derivedIso 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] -noncomputable def derivedSolidification_free_CW_homologyIso +def derivedSolidification_free_CW_homologyIso (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] (n : ℕ) : isSolid.ι.obj ((DerivedCategory.homologyFunctor Solid (-(n : ℤ))).obj @@ -470,3 +470,5 @@ theorem derivedSolidification_free_CW_homology end Solid end LightCondensed + +end