English
The functor Γ sends morphisms in opposite LocallyRingedSpace to the corresponding maps between their global sections.
Русский
Функтор Γ переводит морфизмы в противоположном LocallyRingedSpace в соответствующие отображения между их глобальными секциями.
LaTeX
$$$ \\Gamma.map f = f.unop.c.app (op ⊤) $$$
Lean4
/-- Given two locally ringed spaces `X` and `Y`, an isomorphism between `X` and `Y` as _sheafed_
spaces can be lifted to an isomorphism `X ⟶ Y` as locally ringed spaces.
This is related to the property that the functor `forgetToSheafedSpace` reflects isomorphisms.
In fact, it is slightly stronger as we do not require `f` to come from a morphism between
_locally_ ringed spaces.
-/
def isoOfSheafedSpaceIso {X Y : LocallyRingedSpace.{u}} (f : X.toSheafedSpace ≅ Y.toSheafedSpace) : X ≅ Y
where
hom := homOfSheafedSpaceHomOfIsIso f.hom
inv := homOfSheafedSpaceHomOfIsIso f.inv
hom_inv_id := Hom.ext' f.hom_inv_id
inv_hom_id := Hom.ext' f.inv_hom_id
