Documentation

Mathlib.Condensed.Discrete

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.

source
@[simp]
theorem Condensed.discrete_map (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] :
∀ {X Y : C} (f : X ⟶ Y), (Condensed.discrete C).toPrefunctor.map f = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).toPrefunctor.map ((CategoryTheory.Functor.const CompHausᵒᵖ).toPrefunctor.map f)
source
@[simp]
theorem Condensed.discrete_obj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] (X : C) :
(Condensed.discrete C).toPrefunctor.obj X = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).toPrefunctor.obj ((CategoryTheory.Functor.const CompHausᵒᵖ).toPrefunctor.obj X)
source
noncomputable def Condensed.discrete (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] :
CategoryTheory.Functor C (Condensed C)

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

Equations
Instances For
    source
    @[simp]
    theorem Condensed.underlying_obj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C) :
    (Condensed.underlying C).toPrefunctor.obj j = j.val.toPrefunctor.obj (Opposite.op (⊤_ CompHaus))
    source
    @[simp]
    theorem Condensed.underlying_map (C : Type w) [CategoryTheory.Category.{u + 1, w} C] :
    ∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C} (f : X ⟶ Y), (Condensed.underlying C).toPrefunctor.map f = f.val.app (Opposite.op (⊤_ CompHaus))
    source
    noncomputable def Condensed.underlying (C : Type w) [CategoryTheory.Category.{u + 1, w} C] :
    CategoryTheory.Functor (Condensed C) 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

    Equations
    Instances For
      source
      noncomputable def Condensed.discrete_underlying_adj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] :
      Condensed.discrete C ⊣ Condensed.underlying C

      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