functorIsoDiscreteComponents — Mathlib

English

The LocallyConstant functor is part of an equivalence with the forgetful functor to modules.

Русский

Функтор LocallyConstant образует эквивалентность с функтором забывания к модулям.

LaTeX

$$$\\text{adjunction}:(\\text{functor }R) \\dashv \\text{underlying (ModuleCat }R)\\;,$$$

Lean4

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

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