Theorems · Definition · category theory

LightCondensed.equivSmallFreeIso

(R : Type u) →
  [inst : CommRing R] →
    (LightCondensed.equivSmall (Type u)).inverse.comp
        ((LightCondensed.free R).comp (LightCondensed.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.

Defined in

Mathlib.Condensed.Light.Small

Cited by

0 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing