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.

Equations

• LightCondensed C = CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C

instance instCategoryLightCondensed {C : Type w} [CategoryTheory.Category.{v, w} C] : CategoryTheory.Category.{max (u + 1) v, max (max (u + 1) w) v} (LightCondensed C)

Equations

• instCategoryLightCondensed = let_fun this := inferInstance; this

@[reducible, inline]

abbrev LightCondSet : Type (u + 1)

Light condensed sets. Because LightProfinite is an essentially small category, we don't need the same universe bump as in CondensedSet.

Equations

• LightCondSet = LightCondensed (Type u)