Documentation

Mathlib.Condensed.Discrete.Basic

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 file Mathlib.Condensed.Discrete.Characterization defines a predicate IsDiscrete on condensed and and light condensed objects, and provides several conditions on a (light) condensed set or module that characterize it as discrete.

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

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
@[reducible, inline]

A version of LightCondensed.discrete_underlying_adj in the LightCondSet namespace

Equations