Equivalence of light condensed objects with sheaves on a small site

@[reducible, inline]

noncomputable abbrev LightCondensed.equivSmall (C : Type w) [CategoryTheory.Category.{v, w} C] : LightCondensed C ≌ CategoryTheory.Sheaf ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology (CategoryTheory.coherentTopology LightProfinite)) C

The equivalence of categories from light condensed objects to sheaves on a small site equivalent to light profinite sets.

Equations

• One or more equations did not get rendered due to their size.

instance LightCondensed.instSmallHom {C : Type w} [CategoryTheory.Category.{v, w} C] (X Y : LightCondensed C) : Small.{max u v, max (u + 1) v} (X ⟶ Y)