Theorems · Theorem · category theory

LightCondMod.isDiscrete_tfae

∀ (R : Type u) [inst : Ring R] (M : LightCondMod R),
  [LightCondensed.IsDiscrete M,
      CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit
            (M.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE

Defined in

Mathlib.Condensed.Discrete.Characterization

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring