isDiscrete_iff_isDiscrete_forget — Mathlib

English

For LightCondMod R, discreteness is equivalent to discreteness after forgetting along the condensed forgetful functor to modules over R.

Русский

Для LightCondMod R дискретность эквивалентна после забывания через конденсированное забывающее отображение на модули над R.

LaTeX

$$$\\mathrm{IsDiscrete}(\\text{LightCondensed.forget}\\,R\\;\\mathrm{obj}\\ M) \\;\\text{iff}\\; \\mathrm{IsDiscrete}(M)$$$

Lean4

theorem isDiscrete_iff_isDiscrete_forget (M : LightCondMod R) :
    M.IsDiscrete ↔ ((LightCondensed.forget R).obj M).IsDiscrete :=
  Sheaf.isConstant_iff_forget (coherentTopology LightProfinite) (forget (ModuleCat R)) M LightProfinite.isTerminalPUnit

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