isDiscrete_iff_isDiscrete_forget — Mathlib

English

For CondensedMod R, discreteness is detected after forgetting to Condensed.forget; i.e., M.IsDiscrete if and only if (Condensed.forget R).obj M is discrete.

Русский

Для CondensedMod R дискретность определяется после забывания: M дискретна тогда и только тогда, когда изображение под забыванием становится дискретным.

LaTeX

$$$\\mathrm{IsDiscrete}(M) \\iff \\mathrm{IsDiscrete}(\\mathrm{Condensed.forget}\\,R\\,\\mathrm{obj}\\,M)$$$

Lean4

theorem isDiscrete_iff_isDiscrete_forget (M : CondensedMod R) :
    M.IsDiscrete ↔ ((Condensed.forget R).obj M).IsDiscrete :=
  Sheaf.isConstant_iff_forget (coherentTopology CompHaus) (forget (ModuleCat R)) M CompHaus.isTerminalPUnit

Похожие утверждения