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_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) :

∀ {X_1 Y : CompHaus ᵒᵖ} (f : X_1 ⟶ Y), ((Condensed.discrete C).obj X).val.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.GrothendieckTopology.diagramPullback (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.GrothendieckTopology.plusObj (CategoryTheory.coherentTopology CompHaus) ((CategoryTheory.Functor.const CompHaus ᵒᵖ).obj X)) f.unop)) (CategoryTheory.Limits.colimit.pre (CategoryTheory.GrothendieckTopology.diagram (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.GrothendieckTopology.plusObj (CategoryTheory.coherentTopology CompHaus) ((CategoryTheory.Functor.const CompHaus ᵒᵖ).obj X)) Y.unop) (CategoryTheory.GrothendieckTopology.pullback (CategoryTheory.coherentTopology CompHaus) f.unop).op)

source

@[simp]

theorem Condensed.discrete_obj_val_obj (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) (X : CompHaus ᵒᵖ) :

((Condensed.discrete C).obj X✝).val.obj X = CategoryTheory.Limits.colimit (CategoryTheory.GrothendieckTopology.diagram (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.GrothendieckTopology.plusObj (CategoryTheory.coherentTopology CompHaus) ((CategoryTheory.Functor.const CompHaus ᵒᵖ).obj X✝)) X.unop)

source

@[simp]

theorem Condensed.discrete_map_val_app (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 Y : C} (f : X ⟶ Y) (X_1 : CompHaus ᵒᵖ), ((Condensed.discrete C).map f).val.app X_1 = CategoryTheory.Limits.colimMap (CategoryTheory.GrothendieckTopology.diagramNatTrans (CategoryTheory.coherentTopology CompHaus) (CategoryTheory.GrothendieckTopology.plusMap (CategoryTheory.coherentTopology CompHaus) ((CategoryTheory.Functor.const CompHaus ᵒᵖ).map f)) X_1.unop)

source

noncomputable def Condensed.discrete (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)] :

CategoryTheory.Functor C (Condensed C)

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

Equations

Condensed.discrete C = CategoryTheory.constantSheaf (CategoryTheory.coherentTopology CompHaus) C

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).obj j = j.val.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).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

Condensed.underlying C = (CategoryTheory.sheafSections (CategoryTheory.coherentTopology CompHaus) C).obj (Opposite.op (⊤_ CompHaus))

Instances For

source

noncomputable def Condensed.discrete_underlying_adj (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)] :

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

Condensed.discrete_underlying_adj C = CategoryTheory.constantSheafAdj (CategoryTheory.coherentTopology CompHaus) C CategoryTheory.Limits.terminalIsTerminal

Instances For