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.

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)

noncomputable def LightCondensed.equivSmallSheafificationIso {C : Type w} [CategoryTheory.Category.{v, w} C] [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology LightProfinite) C] [CategoryTheory.HasWeakSheafify ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology (CategoryTheory.coherentTopology LightProfinite)) C] : (CategoryTheory.equivSmallModel LightProfinite).op.congrLeft.inverse.comp ((CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).comp (equivSmall C).functor) ≅ CategoryTheory.presheafToSheaf ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology (CategoryTheory.coherentTopology LightProfinite)) C

Sheafifying is preserved under conjugating with the equivalence between light condensed objects and sheaves on a small site.

noncomputable def LightCondensed.equivSmallFreeIso (R : Type u) [CommRing R] : (equivSmall (Type u)).inverse.comp ((free R).comp (equivSmall (ModuleCat R)).functor) ≅ CategoryTheory.Sheaf.composeAndSheafify ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology (CategoryTheory.coherentTopology LightProfinite)) (ModuleCat.free R)

Taking the free condensed module is preserved under conjugating with the equivalence between light condensed objects and sheaves on a small site.