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 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

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

          A version of LightCondensed.discrete in the LightCondSet namespace

          Equations
          Instances For
            @[reducible, inline]

            A version of LightCondensed.underlying in the LightCondSet namespace

            Equations
            Instances For
              @[reducible, inline]

              A version of LightCondensed.discrete_underlying_adj in the LightCondSet namespace

              Equations
              Instances For