Discrete-underlying adjunction

Given a category C with sheafification with respect to the coherent topology on compact Hausdorff spaces, we define a functor C ⥤ Condensed C which associates to an object of C the corresponding "discrete" condensed object (see Condensed.discrete).

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

We also give the variant LightCondensed.discreteUnderlyingAdj for light condensed objects.

The file Mathlib/Condensed/Discrete/Characterization.lean defines a predicate IsDiscrete on condensed and and light condensed objects, and provides several conditions on a (light) condensed set or module that characterize it as discrete.

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

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

@[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✝) : (discrete C).map f = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).map ((CategoryTheory.Functor.const CompHausᵒᵖ).map f)

@[simp]

theorem Condensed.discrete_obj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] (X : C) : (discrete C).obj X = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology CompHaus) C).obj ((CategoryTheory.Functor.const CompHausᵒᵖ).obj X)

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.of PUnit.{?u.16 + 1}))

@[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✝) : (underlying C).map f = f.val.app (Opposite.op (CompHaus.of PUnit.{u + 1}))

@[simp]

theorem Condensed.underlying_obj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C) : (underlying C).obj j = j.val.obj (Opposite.op (CompHaus.of PUnit.{u + 1}))

noncomputable def Condensed.discreteUnderlyingAdj (C : Type w) [CategoryTheory.Category.{u + 1, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) C] : discrete C ⊣ 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.discreteUnderlyingAdj C = CategoryTheory.constantSheafAdj (CategoryTheory.coherentTopology CompHaus) C CompHaus.isTerminalPUnit

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 light condensed object associated to an object of C is the constant sheaf at that object.

Equations

• LightCondensed.discrete C = CategoryTheory.constantSheaf (CategoryTheory.coherentTopology LightProfinite) C

@[simp]

theorem LightCondensed.discrete_obj (C : Type w) [CategoryTheory.Category.{u, w} C] [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] (X : C) : (discrete C).obj X = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).obj ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).obj X)

@[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✝) : (discrete C).map f = (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).map ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).map f)

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 light condensed object evaluated at a point. This can be viewed as a sort of forgetful functor from LightCondensed C to C

Equations

• LightCondensed.underlying C = (CategoryTheory.sheafSections (CategoryTheory.coherentTopology LightProfinite) C).obj (Opposite.op (LightProfinite.of PUnit.{?u.16 + 1}))

@[simp]

theorem LightCondensed.underlying_map (C : Type w) [CategoryTheory.Category.{u, w} C] {X✝ Y✝ : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C} (f : X✝ ⟶ Y✝) : (underlying C).map f = f.val.app (Opposite.op (LightProfinite.of PUnit.{u + 1}))

@[simp]

theorem LightCondensed.underlying_obj (C : Type w) [CategoryTheory.Category.{u, w} C] (j : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C) : (underlying C).obj j = j.val.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))

noncomputable def LightCondensed.discreteUnderlyingAdj (C : Type w) [CategoryTheory.Category.{u, w} C] [CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] : discrete C ⊣ 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

• LightCondensed.discreteUnderlyingAdj C = CategoryTheory.constantSheafAdj (CategoryTheory.coherentTopology LightProfinite) C CompHausLike.isTerminalPUnit

@[reducible, inline]

noncomputable abbrev LightCondSet.discrete : CategoryTheory.Functor (Type u) (LightCondensed (Type u))

A version of LightCondensed.discrete in the LightCondSet namespace

Equations

• LightCondSet.discrete = LightCondensed.discrete (Type ?u.6)

@[reducible, inline]

noncomputable abbrev LightCondSet.underlying : CategoryTheory.Functor (LightCondensed (Type u)) (Type u)

A version of LightCondensed.underlying in the LightCondSet namespace

Equations

• LightCondSet.underlying = LightCondensed.underlying (Type ?u.6)

@[reducible, inline]

noncomputable abbrev LightCondSet.discreteUnderlyingAdj : discrete ⊣ underlying

A version of LightCondensed.discrete_underlying_adj in the LightCondSet namespace

Equations

• LightCondSet.discreteUnderlyingAdj = LightCondensed.discreteUnderlyingAdj Type