Discrete-underlying adjunction #

Given a well-behaved concrete category C, we define a functor C ⥤ Condensed C which associates to an object of C the corresponding "discrete" condensed object (see Condensed.discrete).

In Condensed.discrete_underlying_adj we prove that this functor is left adjoint to the forgetful functor from Condensed C to C.

theorem Condensed.discrete_obj_val_map (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget C)] [∀ (P : CategoryTheory.Functor CompHausᵒᵖ C) (X : CompHaus) (S : CategoryTheory.GrothendieckTopology.Cover (CategoryTheory.coherentTopology CompHaus) X), CategoryTheory.Limits.HasMultiequalizer (CategoryTheory.GrothendieckTopology.Cover.index S P)] [∀ (X : CompHaus), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover (CategoryTheory.coherentTopology CompHaus) X)ᵒᵖ C] [(X : CompHaus) → CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.GrothendieckTopology.Cover (CategoryTheory.coherentTopology CompHaus) X)ᵒᵖ (CategoryTheory.forget C)] (X : C) :

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

Instances For