Discrete-underlying adjunction #
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
.
We also give the variant LightCondensed.discreteUnderlyingAdj
for light condensed objects.
The discrete condensed object associated to an object of C
is the constant sheaf at that object.
Equations
Instances For
The underlying object of a condensed object in C
is the condensed object evaluated at a point.
This can be viewed as a sort of forgetful functor from Condensed C
to C
Equations
Instances For
Discreteness is left adjoint to the forgetful functor. When C
is Type*
, this is analogous to
TopCat.adj₁ : TopCat.discrete ⊣ forget TopCat
.
Equations
Instances For
The discrete light condensed object associated to an object of C
is the constant sheaf at that
object.
Equations
Instances For
The underlying object of a condensed object in C
is the light condensed object evaluated at a
point. This can be viewed as a sort of forgetful functor from LightCondensed C
to C
Equations
Instances For
Discreteness is left adjoint to the forgetful functor. When C
is Type*
, this is analogous to
TopCat.adj₁ : TopCat.discrete ⊣ forget TopCat
.
Equations
- LightCondensed.discreteUnderlyingAdj C = CategoryTheory.constantSheafAdj (CategoryTheory.coherentTopology LightProfinite) C CompHausLike.isTerminalPUnit
Instances For
A version of LightCondensed.discrete
in the LightCondSet
namespace
Equations
Instances For
A version of LightCondensed.underlying
in the LightCondSet
namespace
Equations
Instances For
A version of LightCondensed.discrete_underlying_adj
in the LightCondSet
namespace