instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf

English

The forgetful functor composed with sheafify or related constructions reflects isomorphisms.

Русский

После композиции забывания и шейификации соответствующий функтор отражает изоморфизмы.

LaTeX

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

Lean4

instance : (SheafOfModules.toSheaf.{v} R).ReflectsIsomorphisms :=
  reflectsIsomorphisms_of_comp (SheafOfModules.toSheaf.{v} R) (sheafToPresheaf J _)

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