feat(Condensed): light condensed objects (#11586)

New foundations for analytic geometry based on light condensed sets are being developed by Clausen-Scholze (see [this youtube playlist](https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO)). 

This PR defines light condensed objects.

- [x] depends on: #8613
- [x] depends on: #8643 
- [x] depends on: #8674
- [x] depends on: #8676
- [x] depends on: #8678 
- [x] depends on: #9513  
- [x] depends on: #11585

Mathlib.lean

@@ -1714,6 +1714,7 @@ import Mathlib.Condensed.Discrete
 import Mathlib.Condensed.Equivalence
 import Mathlib.Condensed.Explicit
 import Mathlib.Condensed.Functors
+import Mathlib.Condensed.Light.Basic
 import Mathlib.Condensed.Limits
 import Mathlib.Condensed.Module
 import Mathlib.Condensed.Solid

Mathlib/Condensed/Light/Basic.lean

@@ -0,0 +1,35 @@
+/-
+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.Sheaf
+import Mathlib.Topology.Category.LightProfinite.EffectiveEpi
+/-!
+
+# Light condensed objects
+
+This file defines the category of light condensed objects in a category `C`, following the work
+of Clausen-Scholze.
+
+-/
+
+universe u v w
+
+open CategoryTheory Limits
+
+/--
+`LightCondensed.{u} C` is the category of light condensed objects in a category `C`, which are
+defined as sheaves on `LightProfinite.{u}` with respect to the coherent Grothendieck topology.
+-/
+def LightCondensed (C : Type w) [Category.{v} C] :=
+  Sheaf (coherentTopology LightProfinite.{u}) C
+
+instance {C : Type w} [Category.{v} C] : Category (LightCondensed.{u} C) :=
+  show Category (Sheaf _ _) from inferInstance
+
+/--
+Light condensed sets. Because `LightProfinite` is an essentially small category, we don't need the
+same universe bump as in `CondensedSet`.
+-/
+abbrev LightCondSet := LightCondensed.{u} (Type u)