docs(Condensed): update the docstrings in condensed files (leanprover-community#13775)

Author: dagurtomas

Mathlib/Condensed/Basic.lean

@@ -19,10 +19,6 @@ of Clausen-Scholze and Barwick-Haine.
 We use the coherent Grothendieck topology on `CompHaus`, and define condensed objects in `C` to
 be `C`-valued sheaves, with respect to this Grothendieck topology.
 
-In future work, we will define similar Grothendieck topologies on the category of profinite sets
-and extremally disconnected sets, and show that the three categories are equivalent (under
-suitable assumptions on `C`).
-
 Note: Our definition more closely resembles "Pyknotic objects" in the sense of Barwick-Haine,
 as we do not impose cardinality bounds, and manage universes carefully instead.
 

Mathlib/Condensed/Discrete.lean

@@ -10,8 +10,9 @@ import Mathlib.Condensed.Basic
 
 # Discrete-underlying adjunction
 
-Given a well-behaved category `C`, we define a functor `C ⥤ Condensed C` which associates
-to an object of `C` the corresponding "discrete" condensed object (see `Condensed.discrete`).
+Given a category `C` with sheafification with respect to the coherent topology on compact Hausdorff
+spaces, we define a functor `C ⥤ Condensed C` which associates to an object of `C` the
+corresponding "discrete" condensed object (see `Condensed.discrete`).
 
 In `Condensed.discreteUnderlyingAdj` we prove that this functor is left adjoint to the forgetful
 functor from `Condensed C` to `C`.

Mathlib/Condensed/Light/Discrete.lean

@@ -12,9 +12,9 @@ import Mathlib.Condensed.Light.Basic
 
 # Discrete-underlying adjunction
 
-Given a well-behaved concrete category `C`, we define a functor `C ⥤ LightCondensed C` which
-associates to an object of `C` the corresponding "discrete" condensed object
-(see `LightCondensed.discrete`).
+Given a category `C` with sheafification with respect to the coherent topology on light profinite
+sets, we define a functor `C ⥤ LightCondensed C` which associates to an object of `C` the
+corresponding "discrete" light condensed object (see `LightCondensed.discrete`).
 
 In `LightCondensed.discreteUnderlyingAdj` we prove that this functor is left adjoint to the
 forgetful functor from `Condensed C` to `C`.

Mathlib/Condensed/Light/Explicit.lean

@@ -18,6 +18,10 @@ The property `EqualizerCondition` is defined in `Mathlib/CategoryTheory/Sites/R
 and it says that for any effective epi `X ⟶ B` (in this case that is equivalent to being a
 continuous surjection), the presheaf `F` exhibits `F(B)` as the equalizer of the two maps
 `F(X) ⇉ F(X ×_B X)`
+
+We also give variants for light condensed objects in concrete categories whose forgetful functor
+reflects finite limits (resp. products), where it is enough to check the sheaf condition after
+postcomposing with the forgetful functor.
 -/
 
 universe v u w

Mathlib/Condensed/Limits.lean

@@ -9,7 +9,7 @@ import Mathlib.Condensed.Module
 
 # Limits in categories of condensed objects
 
-This file adds some instances for limits in condensed sets and condensed abelian groups.
+This file adds some instances for limits in condensed sets and condensed modules.
 -/
 
 universe u

Mathlib/Condensed/Solid.lean

@@ -16,7 +16,7 @@ groups were introduced in [scholze2019condensed], Definition 5.1.
 
 ## Main definition
 
-* `CondensedMod.IsSolid R`: the predicate on condensed abelian groups describing the property of
+* `CondensedMod.IsSolid R`: the predicate on condensed `R`-modules describing the property of
   being solid.
 
 TODO (hard): prove that `((profiniteSolid ℤ).obj S).IsSolid` for `S : Profinite`.