Documentation

Mathlib.Condensed.Discrete

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.

@[simp]
theorem Condensed.discrete_obj_val_map (C : Type w) [] (X : C) :
@[simp]
theorem Condensed.discrete_obj_val_obj (C : Type w) [] (X : C) (X : ) :
(.obj X✝).val.obj X =
@[simp]
theorem Condensed.discrete_map_val_app (C : Type w) [] :
∀ {X Y : C} (f : X Y) (X_1 : ), (.map f).val.app X_1 = CategoryTheory.Limits.colimMap ()

The discrete condensed object associated to an object of C is the constant sheaf at that object.

Equations
Instances For
@[simp]
theorem Condensed.underlying_obj (C : Type w) [] :
.obj j = j.val.obj ()
@[simp]
theorem Condensed.underlying_map (C : Type w) [] :
∀ {X Y : } (f : X Y), .map f = f.val.app ()
noncomputable def Condensed.underlying (C : Type w) [] :

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