instReflectsIsomorphismsSheafOfModulesFunctorOppositeAddCommGrpCatCompSheafToSheafSheafToPresheaf

English

The functor from sheafified modules to presheaf forgetful functor reflects isomorphisms.

Русский

Функтор из шейифицированных модулей в пресешейф отражает изоморфизмы.

LaTeX

$$$ (\mathrm{SheafOfModules.toSheaf} R).\text{ReflectsIsomorphisms} $$$

Lean4

instance : (SheafOfModules.toSheaf.{v} R ⋙ sheafToPresheaf _ _).ReflectsIsomorphisms :=
  inferInstanceAs (SheafOfModules.forget.{v} R ⋙ toPresheaf _).ReflectsIsomorphisms

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