Theorems · Theorem · category theory

CondensedMod.isDiscrete_tfae

∀ (R : Type (u + 1)) [inst : Ring R] (M : CondensedMod R),
  [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M),
      CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.obj).mapCocone S.asLimitCone.op))].TFAE

Defined in

Mathlib.Condensed.Discrete.Characterization

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring