is_presheafedSpace_iso — Mathlib

English

If a morphism f between sheafed spaces is an isomorphism, then its image under the forgetful functor to presheafed spaces is an isomorphism as well.

Русский

Если морфизм между расслоенными пространствами является изоморфизмом, то его образ в PresheafedSpace также является изоморфизмом.

LaTeX

$$$\forall f:\, X\to Y\text{ in }\mathrm{SheafedSpace}(C),\; IsIso(f) \Rightarrow IsIso(\mathrm{forgetToPresheafedSpace}(f))$$$

Lean4

instance is_presheafedSpace_iso {X Y : SheafedSpace C} (f : X ⟶ Y) [IsIso f] : @IsIso (PresheafedSpace C) _ _ _ f :=
  SheafedSpace.forgetToPresheafedSpace.map_isIso f

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