Skip to content

Solid condensed homology of CW complexes

32 fully proved2 statement formalized3 ready to state8 planned

Light Profinite

DefinitionThe shift map on \(\mathbb{N} \cup \{\infty\}\)#✓fully proved

Write \(\mathbb{N} \cup \{\infty\}\) for the one-point compactification of \(\mathbb{N}\), viewed as a light profinite set. The shift map is the continuous map \(\mathbb{N} \cup \{\infty\} \to \mathbb{N} \cup \{\infty\}\) sending \(n\) to \(n + 1\) and \(\infty\) to \(\infty\).

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)⟩ }
Used by 2
Used byOne minus shift on ℤ(ℕ ∪ {∞}) · One minus shift on P

Light Condensed

DefinitionInclusion of the point at infinity#✓fully proved

The morphism of light profinite spaces from the one-point space to the one-point compactification \(\mathbb{N} \cup \{\infty\}\) of \(\mathbb{N}\) that sends the point to \(\infty\).

def ι : LightProfinite.of PUnit.{1} ⟶ ℕ∪{∞} :=
  ConcreteCategory.ofHom ⟨fun _ ↦ ∞, continuous_const⟩
Used by 5
Used byOne minus shift on P · The map ℤ(∞) → ℤ(ℕ ∪ {∞}) · Short exactness of the sequence defining \(P\) · A splitting of the sequence defining \(P\) · Splitting of the inclusion of the point at infinity

DefinitionSplitting of the inclusion of the point at infinity#✓fully proved

The inclusion of the point at infinity into the one-point compactification \(\mathbb{N} \cup \{\infty\}\) of \(\mathbb{N}\) is a split monomorphism of light profinite spaces, with retraction the unique map from \(\mathbb{N} \cup \{\infty\}\) to the one-point space.

def ι_split : SplitMono ι where
  retraction := ConcreteCategory.ofHom ⟨fun _ ↦ PUnit.unit, continuous_const⟩
  id := rfl
Uses 1 · Used by 2
Statement usesInclusion of the point at infinity
Used byShort exactness of the sequence defining \(P\) · A splitting of the sequence defining \(P\)

DefinitionThe map ℤ(∞) → ℤ(ℕ ∪ {∞})#✓fully proved

For a light profinite set \(S\), let \(\mathbb{Z}[S]\) be the free light condensed abelian group on \(S\), and let \(\iota\) be the inclusion of the point \(\infty\) into \(\mathbb{N} \cup \{\infty\}\). This is the morphism \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by \(\iota\), where \(\mathbb{Z}[\infty]\) is the free light condensed abelian group on a point.

def P_map :
    (free ℤ).obj (LightProfinite.of PUnit.{1}).toCondensed ⟶ (free ℤ).obj (ℕ∪{∞}).toCondensed :=
  (lightProfiniteToLightCondSet ⋙ free ℤ).map ι
Uses 1 · Used by 7
Statement usesInclusion of the point at infinity
Used byOne minus shift on P · The light condensed abelian group P · Maps out of P · The projection onto P · The short complex defining \(P\) · Short exactness of the sequence defining \(P\) · A splitting of the sequence defining \(P\)

DefinitionThe light condensed abelian group P#✓fully proved

For a light profinite set \(S\), let \(\mathbb{Z}[S]\) be the free light condensed abelian group on \(S\), and let \(\mathbb{N} \cup \{\infty\}\) be the one-point compactification of \(\mathbb{N}\). Then \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\) is the cokernel of the morphism \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by the inclusion of the point \(\infty\).

def P : LightCondAb := cokernel P_map
Uses 1 · Used by 20
Statement usesThe map ℤ(∞) → ℤ(ℕ ∪ {∞})
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · Derived category of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P · Maps out of P · The projection onto P · P is a retract of ℤ(ℕ ∪ {∞}) · The short complex defining \(P\) · Short exactness of the sequence defining \(P\)

DefinitionThe projection onto P#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), and let \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\). This is the quotient map \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\), the cokernel projection of the map \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by the inclusion of the point \(\infty\).

def P_proj : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ P := cokernel.π _
Uses 2 · Used by 3
Statement usesThe light condensed abelian group P · The map ℤ(∞) → ℤ(ℕ ∪ {∞})
Used byOne minus shift on P · The short complex defining \(P\) · Short exactness of the sequence defining \(P\)

DefinitionThe short complex defining \(P\)#✓fully proved

Write \(\mathbb{N} \cup \{\infty\}\) for the one-point compactification of \(\mathbb{N}\), viewed as a light profinite set, and \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), with \(\mathbb{Z}[\infty]\) the one on a point. This is the short complex of light condensed abelian groups \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\) whose first map is induced by the inclusion of the point \(\infty\) and whose second map is the cokernel projection onto \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\).

def PSequence : ShortComplex LightCondAb :=
  ShortComplex.mk P_map P_proj (cokernel.condition _)
Uses 3 · Used by 3
Statement usesThe light condensed abelian group P · The map ℤ(∞) → ℤ(ℕ ∪ {∞}) · The projection onto P
Used byP is a retract of ℤ(ℕ ∪ {∞}) · Short exactness of the sequence defining \(P\) · A splitting of the sequence defining \(P\)

LemmaShort exactness of the sequence defining \(P\)#✓fully proved

Write \(\mathbb{N} \cup \{\infty\}\) for the one-point compactification of \(\mathbb{N}\), viewed as a light profinite set, and \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), with \(\mathbb{Z}[\infty]\) the one on a point. The short complex of light condensed abelian groups \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\), whose first map is induced by the inclusion of the point \(\infty\) and whose second map is the cokernel projection onto \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\), is short exact: the first map is a monomorphism, the second map is an epimorphism, and the sequence is exact in the middle.

lemma PSequence_exact : PSequence.ShortExact
Uses 6 · Used by 1
Statement usesThe short complex defining \(P\)
Proof usesThe light condensed abelian group P · The map ℤ(∞) → ℤ(ℕ ∪ {∞}) · The projection onto P · Inclusion of the point at infinity · Splitting of the inclusion of the point at infinity
Used byA splitting of the sequence defining \(P\)

DefinitionA splitting of the sequence defining \(P\)#✓fully proved

Write \(\mathbb{N} \cup \{\infty\}\) for the one-point compactification of \(\mathbb{N}\), viewed as a light profinite set, and \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), with \(\mathbb{Z}[\infty]\) the one on a point. Let \(f \colon \mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) be induced by the inclusion of the point \(\infty\), and let \(g \colon \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\) be the cokernel projection onto \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\). This is a chosen splitting of the short exact sequence of light condensed abelian groups \(\mathbb{Z}[\infty] \xrightarrow{f} \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \xrightarrow{g} P\), that is, maps \(r \colon \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to \mathbb{Z}[\infty]\) and \(s \colon P \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) such that \(r \circ f = \mathrm{id}\), \(g \circ s = \mathrm{id}\) and \(f \circ r + s \circ g = \mathrm{id}\), where \(r\) is induced by the map from \(\mathbb{N} \cup \{\infty\}\) to the point.

def PSequence_split : PSequence.Splitting :=
  ShortComplex.Splitting.ofExactOfRetraction _
    PSequence_exact.exact _
    (ι_split.map (lightProfiniteToLightCondSet ⋙ free ℤ)).id
    coequalizer.π_epi
Uses 5 · Used by 1
Statement usesThe short complex defining \(P\) · Short exactness of the sequence defining \(P\) · The map ℤ(∞) → ℤ(ℕ ∪ {∞}) · Inclusion of the point at infinity · Splitting of the inclusion of the point at infinity
Used byP is a retract of ℤ(ℕ ∪ {∞})

DefinitionP is a retract of ℤ(ℕ ∪ {∞})#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\). The quotient \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\) by the image of the map induced by the inclusion of the point \(\infty\) is a retract of \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\): the short exact sequence \(0 \to \mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P \to 0\) splits, and a section of the projection \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\) from this splitting, together with the projection, exhibits the retraction.

def P_retract : Retract P ((free ℤ).obj (ℕ∪{∞}).toCondensed) where
  i := _
  r := _
  retract := PSequence_split.s_g
Uses 3 · Used by 13
Statement usesThe light condensed abelian group P · The short complex defining \(P\) · A splitting of the sequence defining \(P\)
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · Derived category of light solid abelian groups

DefinitionMaps out of P#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), and let \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\) be the cokernel of the map \(\mathbb{Z}[\infty] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by the inclusion of the point \(\infty\). Let \(A\) be a light condensed abelian group and let \(f \colon \mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to A\) be a morphism whose composite with this map is zero. Then \(f\) factors through the projection \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}] \to P\), and this is the induced morphism \(P \to A\).

def P_homMk (A : LightCondAb) (f : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ A)
    (hf : P_map ≫ f = 0) : P ⟶ A := cokernel.desc _ f hf
Uses 2 · Used by 1
Statement usesThe light condensed abelian group P · The map ℤ(∞) → ℤ(ℕ ∪ {∞})
Used byOne minus shift on P

DefinitionOne minus shift on ℤ(ℕ ∪ {∞})#✓fully proved

Let \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) be the free light condensed abelian group on the light profinite set \(\mathbb{N} \cup \{\infty\}\), and let \(\mathrm{shift}\) be its endomorphism induced by the map \(n \mapsto n + 1\), \(\infty \mapsto \infty\). This is the endomorphism \(1 - \mathrm{shift}\) of \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\).

def oneMinusShift' : (free ℤ).obj (ℕ∪{∞}).toCondensed ⟶ (free ℤ).obj (ℕ∪{∞}).toCondensed :=
  𝟙 _ - (lightProfiniteToLightCondSet ⋙ free ℤ).map LightProfinite.shift
Uses 1 · Used by 1
Statement usesThe shift map on \(\mathbb{N} \cup \{\infty\}\)
Used byOne minus shift on P

DefinitionOne minus shift on P#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), let \(\mathbb{N} \cup \{\infty\}\) be the one-point compactification of \(\mathbb{N}\), and let \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\) be the cokernel of the map induced by the inclusion of the point \(\infty\). Let \(\mathrm{shift}\) be the endomorphism of \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by \(n \mapsto n + 1\), \(\infty \mapsto \infty\). The endomorphism \(1 - \mathrm{shift}\) vanishes on \(\mathbb{Z}[\infty]\), so it factors through a morphism \(P \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\). Composing this morphism with the projection onto \(P\) gives the induced endomorphism \(1 - \mathrm{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
Uses 7 · Used by 14
Statement usesThe light condensed abelian group P · Maps out of P · The map ℤ(∞) → ℤ(ℕ ∪ {∞}) · The projection onto P · One minus shift on ℤ(ℕ ∪ {∞}) · Inclusion of the point at infinity · The shift map on \(\mathbb{N} \cup \{\infty\}\)
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · Derived category of light solid abelian groups · Solid light condensed abelian groups

DefinitionSolid light condensed abelian groups#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), let \(\mathbb{N} \cup \{\infty\}\) be the one-point compactification of \(\mathbb{N}\), and let \(P = \mathbb{Z}[\mathbb{N} \cup \{\infty\}]/\mathbb{Z}[\infty]\) be the cokernel of the map induced by the inclusion of the point \(\infty\). The shift \(n \mapsto n + 1\), \(\infty \mapsto \infty\) induces an endomorphism \(1 - \mathrm{shift}\) of \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\), and hence of \(P\). A light condensed abelian group \(A\) is solid if precomposition with this endomorphism of \(P\) is an isomorphism from the internal hom \(\underline{\mathrm{Hom}}(P, A)\) to itself.

def isSolid : ObjectProperty LightCondAb :=
  fun A ↦ IsIso ((MonoidalClosed.pre oneMinusShift).app A)
Uses 2 · Used by 18
Statement usesThe light condensed abelian group P · One minus shift on P
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · Derived category of light solid abelian groups · Degreewise inclusion of complexes of light solid abelian groups · The solidity class · The category of light solid abelian groups · Solidification · Solidification adjunction

AbbreviationThe solidity class#✓fully proved

For a light condensed abelian group \(A\), the class asserting that \(A\) is solid.

abbrev IsSolid (A : LightCondAb) := isSolid.Is A
Uses 1
Statement usesSolid light condensed abelian groups

AbbreviationThe category of light solid abelian groups#✓fully proved

Write \(\mathbb{Z}[S]\) for the free light condensed abelian group on a light profinite set \(S\), let \(\mathbb{N} \cup \{\infty\}\) be the one-point compactification of \(\mathbb{N}\), viewed as a light profinite set, write \(\mathrm{pt}\) for the one-point light profinite set, and let \(P\) be the cokernel of the map \(\mathbb{Z}[\mathrm{pt}] \to \mathbb{Z}[\mathbb{N} \cup \{\infty\}]\) induced by the inclusion of the point \(\infty\). The endomorphism \(1 - \mathrm{shift}\) of \(\mathbb{Z}[\mathbb{N} \cup \{\infty\}]\), where \(\mathrm{shift}\) is induced by \(n \mapsto n + 1\) and \(\infty \mapsto \infty\), descends to an endomorphism of \(P\). A light condensed abelian group \(A\) is solid when this endomorphism of \(P\) induces an isomorphism of internal homs \(\underline{\mathrm{Hom}}(P, A) \to \underline{\mathrm{Hom}}(P, A)\). The category of light solid abelian groups is the full subcategory of light condensed abelian groups on the solid objects.

abbrev Solid : Type _ := isSolid.FullSubcategory
Uses 1 · Used by 16
Statement usesSolid light condensed abelian groups
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · Derived category of light solid abelian groups · Degreewise inclusion of complexes of light solid abelian groups · Solidification · Solidification adjunction

Solid

AbbreviationDerived category of light condensed abelian groups#✓fully proved

The derived category of the abelian category of light condensed abelian groups.

abbrev DLightCondAb := DerivedCategory LightCondAb
Used by 17
Used byDerived inclusion of solid abelian groups · Comparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification of free CW complexes computes singular chains · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Derived solidification on CW complexes · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification · The singular chain functor on CW spaces · The singular chains of a space in the derived category · The singular chain functor into the derived category

AbbreviationDerived category of light solid abelian groups#✓fully proved

The derived category of the abelian category of light solid abelian groups.

abbrev DSolid := DerivedCategory Solid
Uses 5 · Used by 10
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P
Used byDerived inclusion of solid abelian groups · Derived solidification · Derived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification

DefinitionSolidification#●ready to state

The solidification functor from the category of light condensed abelian groups to the category of light solid abelian groups.

This declaration fixes only the functor. Its intended characterization, as left adjoint to the inclusion of light solid abelian groups into light condensed abelian groups, is the separate solidification adjunction.

public def_wanted solidification : LightCondAb ⥤ Solid
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 2 · Used by 3
Statement usesThe category of light solid abelian groups · Solid light condensed abelian groups
Used byComparison map from derived to degreewise solidification · Derived solidification is the left derived functor of solidification · Solidification adjunction

DefinitionSolidification adjunction#●planned

An adjunction exhibiting the solidification functor from light condensed abelian groups to light solid abelian groups as left adjoint to the inclusion of the full subcategory of light solid abelian groups into light condensed abelian groups.

public def_wanted solidificationAdjunction : ❰solidification❱ ⊣ isSolid.ι
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 3
Statement usesThe category of light solid abelian groups · Solidification · Solid light condensed abelian groups

DefinitionDerived solidification#●ready to state

A functor from the derived category of light condensed abelian groups to the derived category of light solid abelian groups.

Separate statements require it to be the left derived functor of degreewise solidification and left adjoint to the derived inclusion; these determine it up to natural isomorphism.

public def_wanted derivedSolidification : DLightCondAb ⥤ DSolid
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 7 · Used by 8
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P
Used byDerived solidification is left adjoint to the derived inclusion · Comparison map from derived to degreewise solidification · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex · Natural isomorphism specifying derived solidification on CW complexes · Derived solidification is the left derived functor of solidification

DefinitionComparison map from derived to degreewise solidification#●planned

Let \(Q\) denote the localization functors from cochain complexes to derived categories. This is a natural transformation from the functor sending a cochain complex \(K\) of light condensed abelian groups to the derived solidification of \(Q(K)\) to the functor sending \(K\) to \(Q(\mathrm{Sol}(K))\), where \(\mathrm{Sol}(K)\) is the complex of light solid abelian groups obtained by applying solidification to \(K\) degreewise.

public def_wanted derivedSolidificationCounit :
    DerivedCategory.Q ⋙ ❰derivedSolidification❱ ⟶
      (❰solidification❱).mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 9 · Used by 1
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived solidification · Solidification · Solid light condensed abelian groups · One minus shift on P
Used byDerived solidification is the left derived functor of solidification

DefinitionDerived solidification is the left derived functor of solidification#●planned

Let \(Q\) denote the localization functors from cochain complexes indexed by \(\mathbb{Z}\) to derived categories. Derived solidification, together with the comparison natural transformation from \(Q\) followed by derived solidification to degreewise solidification followed by \(Q\), is a left derived functor of the functor that applies solidification degreewise to a cochain complex of light condensed abelian groups and then passes to the derived category of light solid abelian groups, with respect to the quasi-isomorphisms of cochain complexes of light condensed abelian groups.

public def_wanted derivedSolidification_isLeftDerivedFunctor :
    (❰derivedSolidification❱).IsLeftDerivedFunctor ❰derivedSolidificationCounit❱
      (HomologicalComplex.quasiIso LightCondAb (ComplexShape.up ℤ))
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 10
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived solidification · Comparison map from derived to degreewise solidification · Solidification · Solid light condensed abelian groups · One minus shift on P

AbbreviationDegreewise inclusion of complexes of light solid abelian groups#✓fully proved

The functor from cochain complexes indexed by \(\mathbb{Z}\) of light solid abelian groups to cochain complexes indexed by \(\mathbb{Z}\) of light condensed abelian groups that applies the inclusion of light solid abelian groups into light condensed abelian groups in each degree.

abbrev inclusionComplexes :
    CochainComplex Solid ℤ ⥤ CochainComplex LightCondAb ℤ :=
  isSolid.ι.mapHomologicalComplex (ComplexShape.up ℤ)
Uses 2 · Used by 2
Statement usesThe category of light solid abelian groups · Solid light condensed abelian groups
Used byComparison map for the derived inclusion · The derived inclusion is computed degreewise

AbbreviationDerived inclusion of solid abelian groups#✓fully proved

The inclusion \(\iota\) of light solid abelian groups into light condensed abelian groups is exact, so it induces a functor \(D(\iota)\) from the derived category of light solid abelian groups to the derived category of light condensed abelian groups.

abbrev derivedInclusion : DSolid ⥤ DLightCondAb :=
  isSolid.ι.mapDerivedCategory
Uses 7 · Used by 6
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P
Used byComparison map for the derived inclusion · The derived inclusion is computed degreewise · Derived solidification is left adjoint to the derived inclusion · Pointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Natural isomorphism specifying derived solidification on CW complexes

AbbreviationThe derived inclusion is computed degreewise#✓fully proved

Let \(\iota\) be the inclusion of light solid abelian groups into light condensed abelian groups, \(D(\iota)\) the induced derived inclusion, and \(Q\) the localization functors from cochain complexes to derived categories. This is the natural isomorphism \(D(\iota)(Q K) \cong Q(\iota K)\) for cochain complexes \(K\) of light solid abelian groups, where \(\iota K\) is \(K\) with \(\iota\) applied degreewise.

abbrev derivedInclusionFactors :
    DerivedCategory.Q ⋙ derivedInclusion ≅ inclusionComplexes ⋙ DerivedCategory.Q :=
  isSolid.ι.mapDerivedCategoryFactors
Uses 8 · Used by 1
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived inclusion of solid abelian groups · Degreewise inclusion of complexes of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P
Used byComparison map for the derived inclusion

AbbreviationComparison map for the derived inclusion#✓fully proved

Let \(\iota\) be the inclusion of light solid abelian groups into light condensed abelian groups, \(D(\iota)\) the induced derived inclusion, and \(Q\) the localization functors from cochain complexes to derived categories. The comparison map is the natural transformation from \(K \mapsto Q(\iota K)\) to \(K \mapsto D(\iota)(Q K)\), for cochain complexes \(K\) of light solid abelian groups, where \(\iota K\) is \(K\) with \(\iota\) applied degreewise; it is the inverse of the natural isomorphism \(D(\iota)(Q K) \cong Q(\iota K)\).

With this comparison map, \(D(\iota)\) is a right derived functor of the degreewise inclusion with respect to quasi-isomorphisms.

abbrev derivedInclusionComparison :
    inclusionComplexes ⋙ DerivedCategory.Q ⟶ DerivedCategory.Q ⋙ derivedInclusion :=
  derivedInclusionFactors.inv
Uses 9
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived inclusion of solid abelian groups · The derived inclusion is computed degreewise · Degreewise inclusion of complexes of light solid abelian groups · Solid light condensed abelian groups · One minus shift on P

DefinitionDerived solidification is left adjoint to the derived inclusion#●planned

An adjunction in which derived solidification, from the derived category of light condensed abelian groups to the derived category of light solid abelian groups, is left adjoint to the derived inclusion \(D(\iota)\) induced by the inclusion \(\iota\) of light solid abelian groups into light condensed abelian groups.

public def_wanted derivedSolidificationAdjunction : ❰derivedSolidification❱ ⊣ derivedInclusion
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 9
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived inclusion of solid abelian groups · Derived solidification · Solid light condensed abelian groups · One minus shift on P

AbbreviationFree light condensed abelian group on a topological space#✓fully proved

For a topological space \(X\), \(\mathbb{Z}[X]\) is the free light condensed abelian group on the light condensed set associated with \(X\).

abbrev freeLightCondAbOfTop (X : TopCat) : LightCondAb :=
  (free ℤ).obj X.toLightCondSet
Used by 4
Used byPointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one · Derived solidification computes singular homology · Homology of the derived solidification of a free CW complex

AbbreviationFree light condensed abelian group functor on topological spaces#✓fully proved

The functor from topological spaces to light condensed abelian groups sending a space \(X\) to the free light condensed abelian group \(\mathbb{Z}[X]\) on the light condensed set associated with \(X\).

abbrev freeLightCondAbOfTopFunctor : TopCat ⥤ LightCondAb :=
  topCatToLightCondSet ⋙ free ℤ
Used by 2
Used byThe pointwise derived comparison is the component of the natural one · Natural isomorphism specifying derived solidification on CW complexes

AbbreviationSingular homology as a light condensed abelian group#✓fully proved

For a topological space \(X\) and \(n \in \mathbb{N}\), this is the discrete light condensed abelian group on the \(n\)-th integral singular homology group \(H_n(X; \mathbb{Z})\).

abbrev singularHomologyLightCondAb (X : TopCat) (n : ℕ) : LightCondAb :=
  (LightCondensed.discrete (ModuleCat ℤ)).obj
    (((AlgebraicTopology.singularHomologyFunctor (ModuleCat.{0} ℤ) n).obj (ModuleCat.of ℤ ℤ)).obj X)
Used by 2
Used byDerived solidification computes singular homology · Homology of the derived solidification of a free CW complex

AbbreviationThe singular chain complex as a complex of light condensed abelian groups#✓fully proved

This is the functor from topological spaces to cochain complexes of light condensed abelian groups sending a space \(X\) to the complex whose term in degree \(-n\), for \(n \ge 0\), is the discrete light condensed abelian group on the integral singular \(n\)-chains \(C_n(X; \mathbb{Z})\), with the singular boundary maps as differentials and zero in positive degrees.

abbrev singularChainsLightCondAbComplexFunctor :
    TopCat ⥤ CochainComplex LightCondAb ℤ :=
  ((AlgebraicTopology.singularChainComplexFunctor (ModuleCat.{0} ℤ)).obj (ModuleCat.of ℤ ℤ)) ⋙
    (LightCondensed.discrete (ModuleCat ℤ)).mapHomologicalComplex (ComplexShape.down ℕ) ⋙
    ComplexShape.embeddingDownNat.extendFunctor LightCondAb
Used by 1
Used byThe singular chain functor into the derived category

AbbreviationThe singular chain functor into the derived category#✓fully proved

This is the functor from topological spaces to the derived category of light condensed abelian groups sending a space \(X\) to its integral singular chain complex, regarded as a cochain complex of discrete light condensed abelian groups with the \(n\)-chains in degree \(-n\).

abbrev singularChainsLightCondAbDerivedFunctor : TopCat ⥤ DLightCondAb :=
  singularChainsLightCondAbComplexFunctor ⋙ DerivedCategory.Q
Uses 2 · Used by 2
Statement usesDerived category of light condensed abelian groups · The singular chain complex as a complex of light condensed abelian groups
Used byThe singular chain functor on CW spaces · The singular chains of a space in the derived category

AbbreviationThe singular chains of a space in the derived category#✓fully proved

For a topological space \(X\), this is the integral singular chain complex of \(X\), regarded as a cochain complex of discrete light condensed abelian groups with the \(n\)-chains in degree \(-n\), as an object of the derived category of light condensed abelian groups.

abbrev singularChainsLightCondAbDerived (X : TopCat) : DLightCondAb :=
  singularChainsLightCondAbDerivedFunctor.obj X
Uses 2 · Used by 2
Statement usesDerived category of light condensed abelian groups · The singular chain functor into the derived category
Used byPointwise derived comparison for CW complexes · The pointwise derived comparison is the component of the natural one

AbbreviationSpaces admitting a CW complex structure#✓fully proved

A topological space \(X\) has this property when it admits a classical CW complex structure whose underlying set is all of \(X\).

abbrev isCWTopCat : ObjectProperty TopCat :=
  fun X ↦ Nonempty (Topology.CWComplex (Set.univ : Set X))
Used by 7
Used byThe category of spaces admitting a CW structure · The pointwise derived comparison is the component of the natural one · Derived solidification of free CW complexes computes singular chains · Derived solidification on CW complexes · Natural isomorphism specifying derived solidification on CW complexes · The singular chain functor on CW spaces · Inclusion of CW spaces into topological spaces

AbbreviationThe category of spaces admitting a CW structure#✓fully proved

The full subcategory of the category of topological spaces whose objects are the spaces \(X\) admitting a classical CW complex structure with underlying set all of \(X\); its morphisms are all continuous maps between such spaces.

abbrev CWTopCat : Type _ := isCWTopCat.FullSubcategory
Uses 1 · Used by 6
Statement usesSpaces admitting a CW complex structure
Used byThe pointwise derived comparison is the component of the natural one · Derived solidification of free CW complexes computes singular chains · Derived solidification on CW complexes · Natural isomorphism specifying derived solidification on CW complexes · The singular chain functor on CW spaces · Inclusion of CW spaces into topological spaces

CW complexes as topological spaces

AbbreviationInclusion of CW spaces into topological spaces#✓fully proved

The inclusion functor from the full subcategory of topological spaces admitting a classical CW complex structure into the category of topological spaces.

abbrev toTopCat : CWTopCat ⥤ TopCat := isCWTopCat.ι
Uses 2 · Used by 3
Statement usesThe category of spaces admitting a CW structure · Spaces admitting a CW complex structure
Used byThe pointwise derived comparison is the component of the natural one · Natural isomorphism specifying derived solidification on CW complexes · The singular chain functor on CW spaces

Solid

DefinitionDerived solidification on CW complexes#●ready to state

A functor from the category of topological spaces admitting a CW complex structure, with all continuous maps as morphisms, to the derived category of light condensed abelian groups.

A separate specification identifies it, up to natural isomorphism, with the functor sending \(X\) to the derived inclusion of the derived solidification of the free light condensed abelian group \(\mathbb{Z}[X]\), viewed as a complex concentrated in degree \(0\).

public def_wanted derivedSolidificationFreeCWFunctor : CWTopCat ⥤ DLightCondAb
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 3 · Used by 3
Statement usesThe category of spaces admitting a CW structure · Derived category of light condensed abelian groups · Spaces admitting a CW complex structure
Used byThe pointwise derived comparison is the component of the natural one · Derived solidification of free CW complexes computes singular chains · Natural isomorphism specifying derived solidification on CW complexes

DefinitionNatural isomorphism specifying derived solidification on CW complexes#●planned

A natural isomorphism between the derived solidification functor on CW complexes and the composite functor that sends a topological space \(X\) admitting a CW complex structure to the free light condensed abelian group \(\mathbb{Z}[X]\), views it as a complex concentrated in degree \(0\) in the derived category of light condensed abelian groups, applies derived solidification, and then applies the derived inclusion of light solid abelian groups into light condensed abelian groups. Both are functors from the category of topological spaces admitting a CW complex structure, with all continuous maps as morphisms, to the derived category of light condensed abelian groups.

public def_wanted derivedSolidificationFreeCWFunctorSpec :
    ❰derivedSolidificationFreeCWFunctor❱ ≅
      CWTopCat.toTopCat ⋙ freeLightCondAbOfTopFunctor ⋙ DerivedCategory.singleFunctor LightCondAb 0 ⋙
        ❰derivedSolidification❱ ⋙ derivedInclusion
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 14 · Used by 1
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · The category of spaces admitting a CW structure · Inclusion of CW spaces into topological spaces · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived inclusion of solid abelian groups · Derived solidification · Derived solidification on CW complexes · Free light condensed abelian group functor on topological spaces · Spaces admitting a CW complex structure · Solid light condensed abelian groups · One minus shift on P
Used byThe pointwise derived comparison is the component of the natural one

AbbreviationThe singular chain functor on CW spaces#✓fully proved

This is the functor from the category of topological spaces admitting a CW complex structure, with all continuous maps as morphisms, to the derived category of light condensed abelian groups sending \(X\) to its integral singular chain complex, regarded as a cochain complex of discrete light condensed abelian groups with the \(n\)-chains in degree \(-n\).

abbrev singularChainsLightCondAbCWDerivedFunctor : CWTopCat ⥤ DLightCondAb :=
  CWTopCat.toTopCat ⋙ singularChainsLightCondAbDerivedFunctor
Uses 5 · Used by 2
Statement usesThe category of spaces admitting a CW structure · Inclusion of CW spaces into topological spaces · Derived category of light condensed abelian groups · Spaces admitting a CW complex structure · The singular chain functor into the derived category
Used byThe pointwise derived comparison is the component of the natural one · Derived solidification of free CW complexes computes singular chains

DefinitionDerived solidification of free CW complexes computes singular chains#●planned

A natural isomorphism of functors from the category of spaces admitting a CW structure to the derived category of light condensed abelian groups, from the derived solidification functor \(F\) to the integral singular chain complex functor. Here \(F(X)\) is the derived inclusion of the derived solidification of the free light condensed abelian group \(\mathbb{Z}[X]\) placed in degree \(0\) (up to a specified natural isomorphism), and the singular chain complex of \(X\) is viewed as a complex of discrete light condensed abelian groups with chains of degree \(n\) in cohomological degree \(-n\).

public def_wanted derivedSolidification_free_CW_derivedNatIso :
    ❰derivedSolidificationFreeCWFunctor❱ ≅ singularChainsLightCondAbCWDerivedFunctor
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 5 · Used by 1
Statement usesThe category of spaces admitting a CW structure · Derived category of light condensed abelian groups · Derived solidification on CW complexes · Spaces admitting a CW complex structure · The singular chain functor on CW spaces
Used byThe pointwise derived comparison is the component of the natural one

DefinitionPointwise derived comparison for CW complexes#●planned

For a topological space \(X\) with a CW complex structure on all of \(X\), an isomorphism in the derived category of light condensed abelian groups from the derived inclusion of the derived solidification of the free light condensed abelian group \(\mathbb{Z}[X]\), placed in degree \(0\), to the integral singular chain complex of \(X\), viewed as a complex of discrete light condensed abelian groups with chains of degree \(n\) placed in cohomological degree \(-n\).

public def_wanted 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
Uses 11 · Used by 1
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived inclusion of solid abelian groups · Derived solidification · Free light condensed abelian group on a topological space · The singular chains of a space in the derived category · Solid light condensed abelian groups · One minus shift on P
Used byThe pointwise derived comparison is the component of the natural one

TheoremThe pointwise derived comparison is the component of the natural one#●statement formalized

Let \(X\) be a topological space with a CW complex structure on all of \(X\), regarded as an object of the category of spaces admitting a CW structure, and let \(\mathbb{Z}[X]\) be the free light condensed abelian group on \(X\). Let \(F\) be the derived solidification functor on spaces admitting a CW structure, let \(\sigma\) be the natural isomorphism from \(F\) to the functor sending \(X\) to the derived inclusion of the derived solidification of \(\mathbb{Z}[X]\) placed in degree \(0\), and let \(\nu\) be the natural isomorphism from \(F\) to the integral singular chain complex functor with values in the derived category of light condensed abelian groups. Then the pointwise isomorphism \(\phi_X\) from the derived inclusion of the derived solidification of \(\mathbb{Z}[X]\) (placed in degree \(0\)) to the singular chain complex of \(X\) equals \(\nu_X \circ \sigma_X^{-1}\).

public theorem_wanted derivedSolidification_free_CW_derivedIso_eq
    (X : TopCat) [Topology.CWComplex (Set.univ : Set X)] :
    ❰derivedSolidification_free_CW_derivedIso❱ X =
      (❰derivedSolidificationFreeCWFunctorSpec❱.app ⟨X, ⟨inferInstance⟩⟩).symm.trans
        (❰derivedSolidification_free_CW_derivedNatIso❱.app ⟨X, ⟨inferInstance⟩⟩)
Uses 20
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · The category of spaces admitting a CW structure · Inclusion of CW spaces into topological spaces · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived inclusion of solid abelian groups · Derived solidification · Derived solidification on CW complexes · Natural isomorphism specifying derived solidification on CW complexes · Pointwise derived comparison for CW complexes · Derived solidification of free CW complexes computes singular chains · Free light condensed abelian group on a topological space · Free light condensed abelian group functor on topological spaces · Spaces admitting a CW complex structure · The singular chain functor on CW spaces · The singular chains of a space in the derived category · Solid light condensed abelian groups · One minus shift on P

DefinitionDerived solidification computes singular homology#●planned

Let \(X\) be a topological space equipped with a CW complex structure, let \(n\) be a natural number, and let \(\mathbb{Z}[X]\) be the free light condensed abelian group on \(X\), viewed as a complex concentrated in degree \(0\) in the derived category of light condensed abelian groups. Apply derived solidification to \(\mathbb{Z}[X]\), take the homology in cohomological degree \(-n\), which is a light solid abelian group, and regard it as a light condensed abelian group. This is an isomorphism between the resulting light condensed abelian group and the \(n\)-th singular homology group \(H_n(X; \mathbb{Z})\) of \(X\) with integer coefficients, regarded as a discrete light condensed abelian group.

The derived category is cohomologically indexed, so the \(n\)-th homology group sits in degree \(-n\).

public def_wanted 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
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 10
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived solidification · Free light condensed abelian group on a topological space · Singular homology as a light condensed abelian group · Solid light condensed abelian groups · One minus shift on P

TheoremHomology of the derived solidification of a free CW complex#●statement formalized

Let \(X\) be a topological space with a CW complex structure on all of \(X\), let \(\mathbb{Z}[X]\) be the free light condensed abelian group on \(X\), and let \(n\) be a natural number. Then the cohomology in degree \(-n\) of the derived solidification of \(\mathbb{Z}[X]\) placed in degree \(0\), a light solid abelian group regarded as a light condensed abelian group, is isomorphic to the integral singular homology group \(H_n(X; \mathbb{Z})\) viewed as a discrete light condensed abelian group.

public theorem_wanted 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)
Sources
  • https://github.com/dagurtomas/LeanCondensed; 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. Problem derived_solidification_free_CW_homology of the lean-eval benchmark.
Uses 10
Statement usesThe light condensed abelian group P · P is a retract of ℤ(ℕ ∪ {∞}) · The category of light solid abelian groups · Derived category of light condensed abelian groups · Derived category of light solid abelian groups · Derived solidification · Free light condensed abelian group on a topological space · Singular homology as a light condensed abelian group · Solid light condensed abelian groups · One minus shift on P

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.