Light condensed objects #
This file defines the category of light condensed objects in a category C
, following the work
of Clausen-Scholze (see https://www.youtube.com/playlist?list=PLx5f8IelFRgGmu6gmL-Kf_Rl_6Mm7juZO).
def
LightCondensed
(C : Type w)
[CategoryTheory.Category.{v, w} C]
:
Type (max (max (max (u + 1) w) u) v)
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.
Instances For
Equations
- instCategoryLightCondensed = let_fun this := inferInstance; this
@[reducible, inline]
Light condensed sets. Because LightProfinite
is an essentially small category, we don't need the
same universe bump as in CondensedSet
.