Documentation

Mathlib.Condensed.Light.Discrete

Discrete-underlying adjunction #

Given a category C with sheafification with respect to the coherent topology on light profinite sets, we define a functor C ⥤ LightCondensed C which associates to an object of C the corresponding "discrete" light condensed object (see LightCondensed.discrete).

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

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

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

Equations
Instances For
    source
    @[simp]
    theorem LightCondensed.underlying_obj (C : Type w) [CategoryTheory.Category.{u, w} C] (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C) :
    (LightCondensed.underlying C).obj j = j.val.obj { unop := LightProfinite.of PUnit.{u + 1} }
    source
    @[simp]
    theorem LightCondensed.underlying_map (C : Type w) [CategoryTheory.Category.{u, w} C] :
    ∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C} (f : X ⟶ Y), (LightCondensed.underlying C).map f = f.val.app { unop := LightProfinite.of PUnit.{u + 1} }
    source
    noncomputable def LightCondensed.underlying (C : Type w) [CategoryTheory.Category.{u, w} C] :
    CategoryTheory.Functor (LightCondensed 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 LightCondensed.discreteUnderlyingAdj (C : Type w) [CategoryTheory.Category.{u, w} C] [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] :
      LightCondensed.discrete C ⊣ LightCondensed.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
        source
        @[reducible, inline]
        noncomputable abbrev LightCondSet.discrete :
        CategoryTheory.Functor (Type u) (LightCondensed (Type u))

        A version of LightCondensed.discrete in the LightCondSet namespace

        Equations
        Instances For
          source
          @[reducible, inline]
          noncomputable abbrev LightCondSet.underlying :
          CategoryTheory.Functor (LightCondensed (Type u)) (Type u)

          A version of LightCondensed.underlying in the LightCondSet namespace

          Equations
          Instances For
            source
            @[reducible, inline]
            noncomputable abbrev LightCondSet.discreteUnderlyingAdj :
            LightCondSet.discrete ⊣ LightCondSet.underlying

            A version of LightCondensed.discrete_underlying_adj in the LightCondSet namespace

            Equations
            Instances For