Documentation

Mathlib.Condensed.Light.Small

Equivalence of light condensed objects with sheaves on a small site #

source
@[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.
Instances For
    source
    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)
    source
    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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      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.

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