is_sheafedSpace_iso — Mathlib

English

If f is an isomorphism in LocallyRingedSpace, then its corresponding toShHom is an isomorphism of sheafed spaces.

Русский

Если f является изоморфизмом в LocallyRingedSpace, то соответствующий toShHom является изоморфизмом пространства с Sheaf.

LaTeX

$$$ [IsIso f] \\Rightarrow IsIso f.toShHom $$$

Lean4

instance is_sheafedSpace_iso {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) [IsIso f] : IsIso f.toShHom :=
  LocallyRingedSpace.forgetToSheafedSpace.map_isIso f

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