homOfSheafedSpaceHomOfIsIso — Mathlib

Lean4

/-- Given two locally ringed spaces `X` and `Y`, an isomorphism between `X` and `Y` as _sheafed_
spaces can be lifted to a morphism `X ⟶ Y` as locally ringed spaces.

See also `isoOfSheafedSpaceIso`.
-/
@[simps! toShHom]
def homOfSheafedSpaceHomOfIsIso {X Y : LocallyRingedSpace.{u}} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace) [IsIso f] :
    X ⟶ Y :=
  Hom.mk f
    fun _ =>
      -- Here we need to see that the stalk maps are really local ring homomorphisms.
          -- This can be solved by type class inference, because stalk maps of isomorphisms
          -- are isomorphisms and isomorphisms are local ring homomorphisms.

    inferInstance

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