Checking isomorphism of sheafed spaces on stalks

Stream: Is there code for X?

[Junyan Xu]

Does anyone has anything like this?

import Mathlib.Geometry.RingedSpace.LocallyRingedSpace
open AlgebraicGeometry
variable (X Y : LocallyRingedSpace) (f : X ⟶ Y)
-- true for SheafedSpace as well
def toIso (homeo : IsHomeomorph f.base) (bij : ∀ x : X, Function.Bijective (f.stalkMap x)) :
    X ≅ Y :=
  sorry

[Andrew Yang]

Should be relatively easy via docs#AlgebraicGeometry.SheafedSpace.IsOpenImmersion.to_iso and docs#AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso

[Junyan Xu]

Thanks!

import Mathlib.Geometry.RingedSpace.OpenImmersion
open AlgebraicGeometry CategoryTheory
noncomputable def toIso (X Y : RingedSpace) (f : X ⟶ Y) (homeo : IsHomeomorph f.base)
    (bij : ∀ x : X, Function.Bijective (f.stalkMap x)) :
    X ≅ Y :=
  have : Epi f.base := (TopCat.epi_iff_surjective _).mpr homeo.bijective.2
  have (x : X) : IsIso (f.stalkMap x) :=
    (ConcreteCategory.isIso_iff_bijective (PresheafedSpace.Hom.stalkMap f x)).mpr (bij x)
  have := (SheafedSpace.IsOpenImmersion.of_stalk_iso f homeo.isOpenEmbedding).to_iso
  asIso f