feat(Condensed): discrete-underlying adjunction (#8270)

We define a functor, associating to an object of a concrete category with nice properties, a "discrete" condensed object, and prove that this functor is left adjoint to the forgetful functor from `Condensed C` to `C`.

Mathlib.lean

@@ -1208,6 +1208,7 @@ import Mathlib.CategoryTheory.Sites.Closed
 import Mathlib.CategoryTheory.Sites.Coherent
 import Mathlib.CategoryTheory.Sites.CompatiblePlus
 import Mathlib.CategoryTheory.Sites.CompatibleSheafification
+import Mathlib.CategoryTheory.Sites.ConstantSheaf
 import Mathlib.CategoryTheory.Sites.CoverLifting
 import Mathlib.CategoryTheory.Sites.CoverPreserving
 import Mathlib.CategoryTheory.Sites.Coverage
@@ -1347,6 +1348,7 @@ import Mathlib.Computability.TMToPartrec
 import Mathlib.Computability.TuringMachine
 import Mathlib.Condensed.Abelian
 import Mathlib.Condensed.Basic
+import Mathlib.Condensed.Discrete
 import Mathlib.Condensed.Equivalence
 import Mathlib.Control.Applicative
 import Mathlib.Control.Basic

Mathlib/CategoryTheory/Sites/ConstantSheaf.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.CategoryTheory.Sites.Sheafification
+
+/-!
+
+# The constant sheaf
+
+We define the constant sheaf functor (the sheafification of the constant presheaf)
+`constantSheaf : D ⥤ Sheaf J D` and prove that it is left adjoint to evaluation at a terminal
+object (see `constantSheafAdj`).
+-/
+
+namespace CategoryTheory
+
+open Limits Opposite
+
+variable {C : Type*} [Category C] (J : GrothendieckTopology C)
+
+variable (D : Type*) [Category D]
+
+/-- The constant presheaf functor is left adjoint to evaluation at a terminal object. -/
+noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) :
+    Functor.const Cᵒᵖ ⊣ (evaluation Cᵒᵖ D).obj (op T) :=
+  Adjunction.mkOfUnitCounit {
+    unit := (Functor.constCompEvaluationObj D (op T)).hom
+    counit := {
+      app := fun F => {
+        app := fun ⟨X⟩ => F.map (IsTerminal.from hT X).op
+        naturality := fun _ _ _ => by
+          simp only [Functor.comp_obj, Functor.const_obj_obj, Functor.id_obj, Functor.const_obj_map,
+            Category.id_comp, ← Functor.map_comp]
+          congr
+          simp }
+      naturality := by intros; ext; simp /- Note: `aesop` works but is kind of slow -/ } }
+
+variable [ConcreteCategory D] [PreservesLimits (forget D)]
+  [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)]
+  [∀ X : C, HasColimitsOfShape (J.Cover X)ᵒᵖ D]
+  [∀ X : C, PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)] [ReflectsIsomorphisms (forget D)]
+
+/--
+The functor which maps an object of `D` to the constant sheaf at that object, i.e. the
+sheafification of the constant presheaf.
+-/
+noncomputable def constantSheaf : D ⥤ Sheaf J D := Functor.const Cᵒᵖ ⋙ (presheafToSheaf J D)
+
+/-- The constant sheaf functor is left adjoint to evaluation at a terminal object. -/
+noncomputable def constantSheafAdj {T : C} (hT : IsTerminal T) :
+    constantSheaf J D ⊣ (sheafSections J D).obj (op T) :=
+  (constantPresheafAdj D hT).comp (sheafificationAdjunction J D)
+
+end CategoryTheory

Mathlib/CategoryTheory/Sites/Sheaf.lean

@@ -328,6 +328,9 @@ def sheafToPresheaf : Sheaf J A ⥤ Cᵒᵖ ⥤ A where
 set_option linter.uppercaseLean3 false in
 #align category_theory.Sheaf_to_presheaf CategoryTheory.sheafToPresheaf
 
+/-- The sections of a sheaf (i.e. evaluation as a presheaf on `C`). -/
+abbrev sheafSections : Cᵒᵖ ⥤ Sheaf J A ⥤ A := (sheafToPresheaf J A).flip
+
 instance : Full (sheafToPresheaf J A) where preimage f := ⟨f⟩
 
 instance : Faithful (sheafToPresheaf J A) where

Mathlib/Condensed/Discrete.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dagur Asgeirsson
+-/
+import Mathlib.CategoryTheory.Sites.ConstantSheaf
+import Mathlib.Condensed.Basic
+
+/-!
+
+# 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`.
+-/
+
+universe u v w
+
+open CategoryTheory Limits Opposite GrothendieckTopology
+
+variable (C : Type w) [Category.{u+1} C] [ConcreteCategory C]
+  [PreservesLimits (forget C)] [ReflectsIsomorphisms (forget C)]
+  [∀ (P : CompHausᵒᵖ ⥤ C) X (S : Cover (coherentTopology CompHaus) X),
+    HasMultiequalizer (Cover.index S P)]
+  [∀ X, HasColimitsOfShape (Cover (coherentTopology CompHaus) X)ᵒᵖ C]
+  [∀ X, PreservesColimitsOfShape (Cover (coherentTopology CompHaus) X)ᵒᵖ (forget C)]
+-- These conditions are satisfied by the category of abelian groups, and other "algebraic"
+-- categories.
+
+/--
+The discrete condensed object associated to an object of `C` is the constant sheaf at that object.
+-/
+@[simps!]
+noncomputable def Condensed.discrete : C ⥤ Condensed.{u} C := constantSheaf _ 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`
+-/
+@[simps!]
+noncomputable def Condensed.underlying : Condensed.{u} C ⥤ C := (sheafSections _ _).obj (op (⊤_ _))
+
+/--
+Discreteness is left adjoint to the forgetful functor. When `C` is `Type*`, this is analogous to
+`TopCat.adj₁ : TopCat.discrete ⊣ forget TopCat`.  
+-/
+noncomputable def Condensed.discrete_underlying_adj : discrete C ⊣ underlying C :=
+  constantSheafAdj _ _ terminalIsTerminal