functorIsoDiscreteComponents — Mathlib

English

There is a Condensed.discrete isomorphism between a module and its LocallyConstant realization.

Русский

Существует сокращение между дискретной конденсированной структурой и локально-константной реализацией модуля.

LaTeX

$$$\operatorname{Isomorphism}(((\mathrm{Condensed.discrete}).obj M))$$$

Lean4

/-- Auxiliary definition for `functorIsoDiscrete`. -/
noncomputable def functorIsoDiscreteComponents (M : ModuleCat R) : (discrete _).obj M ≅ (functor R).obj M :=
  have : (Condensed.forget R).ReflectsIsomorphisms := inferInstanceAs (sheafCompose _ _).ReflectsIsomorphisms
  have : IsIso ((discreteUnderlyingAdj (ModuleCat R)).counit.app ((functor R).obj M)) :=
    isIso_of_reflects_iso _ (Condensed.forget R)
  functorIsoDiscreteAux₂ R M ≪≫ asIso ((discreteUnderlyingAdj _).counit.app ((functor R).obj M))

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