[Merged by Bors] - refactor(AlgebraicGeometry): stalk maps

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -552,7 +552,7 @@ theorem isLocalization_stalk' (y : PrimeSpectrum Γ(X, U)) (hy : hU.fromSpec.1.b
     (@IsLocalization.isLocalization_iff_of_ringEquiv (R := Γ(X, U))
       (S := X.presheaf.stalk (hU.fromSpec.1.base y)) _ y.asIdeal.primeCompl _
       (TopCat.Presheaf.algebra_section_stalk X.presheaf ⟨hU.fromSpec.1.base y, hy⟩) _ _
-      (asIso <| PresheafedSpace.stalkMap hU.fromSpec.1 y).commRingCatIsoToRingEquiv).mpr
+      (asIso <| hU.fromSpec.stalkMap y).commRingCatIsoToRingEquiv).mpr
   -- Porting note: need to know what the ring is and after convert, instead of equality
   -- we get an `iff`.
   convert StructureSheaf.IsLocalization.to_stalk Γ(X, U) y using 1
@@ -690,6 +690,20 @@ lemma Scheme.eq_zeroLocus_of_isClosed_of_isAffine (X : Scheme.{u}) [IsAffine X]
 
 end ZeroLocus
 
+section Stalks
+
+/-- Variant of `AlgebraicGeometry.localRingHom_comp_stalkIso` for `Spec.map`. -/
+@[elementwise]
+lemma Scheme.localRingHom_comp_stalkIso {R S : CommRingCat} (f : R ⟶ S) (p : PrimeSpectrum S) :
+    (StructureSheaf.stalkIso R (PrimeSpectrum.comap f p)).hom ≫
+      CategoryStruct.comp (Y := CommRingCat.of (Localization.AtPrime p.asIdeal))
+        (Localization.localRingHom (PrimeSpectrum.comap f p).asIdeal p.asIdeal f rfl)
+        (StructureSheaf.stalkIso S p).inv =
+    (Spec.map f).stalkMap p :=
+  AlgebraicGeometry.localRingHom_comp_stalkIso f p
+
+end Stalks
+
 @[deprecated (since := "2024-06-21"), nolint defLemma]
 alias isAffineAffineScheme := isAffine_affineScheme
 @[deprecated (since := "2024-06-21"), nolint defLemma]

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -61,28 +61,12 @@ namespace LocallyRingedSpace
 
 variable (X : LocallyRingedSpace.{u})
 
-/-- The map from the global sections to a stalk. -/
-def ΓToStalk (x : X) : Γ.obj (op X) ⟶ X.presheaf.stalk x :=
-  X.presheaf.germ (⟨x, trivial⟩ : (⊤ : Opens X))
-
-lemma ΓToStalk_stalkMap {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : X) :
-    Y.ΓToStalk (f.val.base x) ≫ PresheafedSpace.stalkMap f.val x =
-      f.val.c.app (op ⊤) ≫ X.ΓToStalk x := by
-  dsimp only [LocallyRingedSpace.ΓToStalk]
-  rw [PresheafedSpace.stalkMap_germ']
-
-lemma ΓToStalk_stalkMap_apply {X Y : LocallyRingedSpace} (f : X ⟶ Y) (x : X)
-    (a : Y.presheaf.obj (op ⊤)) :
-    PresheafedSpace.stalkMap f.val x (Y.ΓToStalk (f.val.base x) a) =
-      X.ΓToStalk x (f.val.c.app (op ⊤) a) := by
-  simpa using congrFun (congrArg DFunLike.coe <| ΓToStalk_stalkMap f x) a
-
 /-- The canonical map from the underlying set to the prime spectrum of `Γ(X)`. -/
 def toΓSpecFun : X → PrimeSpectrum (Γ.obj (op X)) := fun x =>
-  comap (X.ΓToStalk x) (LocalRing.closedPoint (X.presheaf.stalk x))
+  comap (X.presheaf.Γgerm x) (LocalRing.closedPoint (X.presheaf.stalk x))
 
 theorem not_mem_prime_iff_unit_in_stalk (r : Γ.obj (op X)) (x : X) :
-    r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit (X.ΓToStalk x r) := by
+    r ∉ (X.toΓSpecFun x).asIdeal ↔ IsUnit (X.presheaf.Γgerm x r) := by
   erw [LocalRing.mem_maximalIdeal, Classical.not_not]
 
 /-- The preimage of a basic open in `Spec Γ(X)` under the unit is the basic
@@ -196,14 +180,13 @@ theorem toΓSpecSheafedSpace_app_eq :
 /-- The map on stalks induced by the unit commutes with maps from `Γ(X)` to
     stalks (in `Spec Γ(X)` and in `X`). -/
 theorem toStalk_stalkMap_toΓSpec (x : X) :
-    toStalk _ _ ≫ PresheafedSpace.stalkMap X.toΓSpecSheafedSpace x = X.ΓToStalk x := by
-  rw [PresheafedSpace.stalkMap]
+    toStalk _ _ ≫ X.toΓSpecSheafedSpace.stalkMap x = X.presheaf.Γgerm x := by
+  rw [PresheafedSpace.Hom.stalkMap]
   erw [← toOpen_germ _ (basicOpen (1 : Γ.obj (op X)))
       ⟨X.toΓSpecFun x, by rw [basicOpen_one]; trivial⟩]
   rw [← Category.assoc, Category.assoc (toOpen _ _)]
   erw [stalkFunctor_map_germ]
-  rw [← Category.assoc, toΓSpecSheafedSpace_app_spec]
-  unfold ΓToStalk
+  rw [← Category.assoc, toΓSpecSheafedSpace_app_spec, Γgerm]
   rw [← stalkPushforward_germ _ X.toΓSpecBase X.presheaf ⊤]
   congr 1
   change (X.toΓSpecBase _* X.presheaf).map le_top.hom.op ≫ _ = _
@@ -300,7 +283,7 @@ def identityToΓSpec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.rightOp ⋙ Spec.toLoc
       erw [this]
       dsimp [toΓSpecFun]
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-      erw [← LocalRing.comap_closedPoint (PresheafedSpace.stalkMap f.val x), ←
+      erw [← LocalRing.comap_closedPoint (f.stalkMap x), ←
         PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply]
       congr 2
       exact (PresheafedSpace.stalkMap_germ f.1 ⊤ ⟨x, trivial⟩).symm

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -358,13 +358,10 @@ theorem fromGlued_injective : Function.Injective 𝒰.fromGlued.1.base := by
     rfl
 
 instance fromGlued_stalk_iso (x : 𝒰.gluedCover.glued.carrier) :
-    IsIso (PresheafedSpace.stalkMap 𝒰.fromGlued.val x) := by
+    IsIso (𝒰.fromGlued.stalkMap x) := by
   obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x
-  have :=
-    PresheafedSpace.stalkMap.congr_hom _ _
-      (congr_arg LocallyRingedSpace.Hom.val <| 𝒰.ι_fromGlued i) x
-  erw [PresheafedSpace.stalkMap.comp] at this
-  rw [← IsIso.eq_comp_inv] at this
+  have := stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x
+  rw [stalkMap_comp, ← IsIso.eq_comp_inv] at this
   rw [this]
   infer_instance
 
@@ -398,7 +395,7 @@ instance : Epi 𝒰.fromGlued.val.base := by
   exact h
 
 instance fromGlued_open_immersion : IsOpenImmersion 𝒰.fromGlued :=
-  SheafedSpace.IsOpenImmersion.of_stalk_iso _ 𝒰.fromGlued_openEmbedding
+  IsOpenImmersion.of_stalk_iso _ 𝒰.fromGlued_openEmbedding
 
 instance : IsIso 𝒰.fromGlued :=
   let F := Scheme.forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -40,7 +40,7 @@ topological map is a closed embedding and the induced stalk maps are surjective.
 @[mk_iff]
 class IsClosedImmersion {X Y : Scheme} (f : X ⟶ Y) : Prop where
   base_closed : ClosedEmbedding f.1.base
-  surj_on_stalks : ∀ x, Function.Surjective (PresheafedSpace.stalkMap f.1 x)
+  surj_on_stalks : ∀ x, Function.Surjective (f.stalkMap x)
 
 namespace IsClosedImmersion
 
@@ -49,7 +49,7 @@ lemma closedEmbedding {X Y : Scheme} (f : X ⟶ Y)
   IsClosedImmersion.base_closed
 
 lemma surjective_stalkMap {X Y : Scheme} (f : X ⟶ Y)
-    [IsClosedImmersion f] (x : X) : Function.Surjective (PresheafedSpace.stalkMap f.1 x) :=
+    [IsClosedImmersion f] (x : X) : Function.Surjective (f.stalkMap x) :=
   IsClosedImmersion.surj_on_stalks x
 
 lemma eq_inf : @IsClosedImmersion = (topologically ClosedEmbedding) ⊓
@@ -67,7 +67,7 @@ instance : MorphismProperty.IsMultiplicative @IsClosedImmersion where
   id_mem _ := inferInstance
   comp_mem {X Y Z} f g hf hg := by
     refine ⟨hg.base_closed.comp hf.base_closed, fun x ↦ ?_⟩
-    erw [PresheafedSpace.stalkMap.comp]
+    rw [Scheme.stalkMap_comp]
     exact (hf.surj_on_stalks x).comp (hg.surj_on_stalks (f.1.1 x))
 
 /-- Composition of closed immersions is a closed immersion. -/
@@ -86,7 +86,8 @@ theorem spec_of_surjective {R S : CommRingCat} (f : R ⟶ S) (h : Function.Surje
     IsClosedImmersion (Spec.map f) where
   base_closed := PrimeSpectrum.closedEmbedding_comap_of_surjective _ _ h
   surj_on_stalks x := by
-    erw [← localRingHom_comp_stalkIso, CommRingCat.coe_comp, CommRingCat.coe_comp]
+    rw [← Scheme.localRingHom_comp_stalkIso]
+    erw [CommRingCat.coe_comp, CommRingCat.coe_comp]
     apply Function.Surjective.comp (Function.Surjective.comp _ _) _
     · exact (ConcreteCategory.bijective_of_isIso (StructureSheaf.stalkIso S x).inv).2
     · exact surjective_localRingHom_of_surjective f h x.asIdeal
@@ -122,7 +123,7 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion
       exact ClosedEmbedding.isClosedMap h _ hZ
   surj_on_stalks x := by
     have h := surjective_stalkMap (f ≫ g) x
-    erw [Scheme.comp_val, PresheafedSpace.stalkMap.comp] at h
+    simp_rw [Scheme.comp_val, Scheme.stalkMap_comp] at h
     exact Function.Surjective.of_comp h
 
 instance {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : QuasiCompact f where

Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

@@ -242,7 +242,7 @@ end Topologically
 /-- `stalkwise P` holds for a morphism if all stalks satisfy `P`. -/
 def stalkwise (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop) :
     MorphismProperty Scheme.{u} :=
-  fun _ _ f => ∀ x, P (PresheafedSpace.stalkMap f.val x)
+  fun _ _ f => ∀ x, P (f.stalkMap x)
 
 section Stalkwise
 
@@ -254,12 +254,12 @@ lemma stalkwise_respectsIso (hP : RingHom.RespectsIso P) :
   precomp {X Y Z} e f hf := by
     simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]
     intro x
-    erw [PresheafedSpace.stalkMap.comp]
+    rw [Scheme.stalkMap_comp]
     exact (RingHom.RespectsIso.cancel_right_isIso hP _ _).mpr <| hf (e.hom.val.base x)
   postcomp {X Y Z} e f hf := by
     simp only [stalkwise, Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply]
     intro x
-    erw [PresheafedSpace.stalkMap.comp]
+    rw [Scheme.stalkMap_comp]
     exact (RingHom.RespectsIso.cancel_left_isIso hP _ _).mpr <| hf x
 
 /-- If `P` respects isos, then `stalkwise P` is local at the target. -/

Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean

@@ -29,7 +29,7 @@ namespace AlgebraicGeometry
 variable {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
 
 theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} : IsOpenImmersion f ↔
-    OpenEmbedding f.1.base ∧ ∀ x, IsIso (PresheafedSpace.stalkMap f.1 x) := by
+    OpenEmbedding f.1.base ∧ ∀ x, IsIso (f.stalkMap x) := by
   constructor
   · intro h; exact ⟨h.1, inferInstance⟩
   · rintro ⟨h₁, h₂⟩; exact IsOpenImmersion.of_stalk_iso f h₁

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -334,19 +334,25 @@ theorem to_iso {X Y : Scheme.{u}} (f : X ⟶ Y) [h : IsOpenImmersion f] [Epi f.1
     (@PresheafedSpace.IsOpenImmersion.to_iso _ _ _ _ f.1 h _) _
 
 theorem of_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) (hf : OpenEmbedding f.1.base)
-    [∀ x, IsIso (PresheafedSpace.stalkMap f.1 x)] : IsOpenImmersion f :=
+    [∀ x, IsIso (f.stalkMap x)] : IsOpenImmersion f :=
+  haveI (x : X) : IsIso (f.val.stalkMap x) := inferInstanceAs <| IsIso (f.stalkMap x)
   SheafedSpace.IsOpenImmersion.of_stalk_iso f.1 hf
 
+instance stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (x : X) :
+    IsIso (f.stalkMap x) :=
+  inferInstanceAs <| IsIso (f.val.stalkMap x)
+
 theorem iff_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) :
-    IsOpenImmersion f ↔ OpenEmbedding f.1.base ∧ ∀ x, IsIso (PresheafedSpace.stalkMap f.1 x) :=
-  ⟨fun H => ⟨H.1, inferInstance⟩, fun ⟨h₁, h₂⟩ => @IsOpenImmersion.of_stalk_iso _ _ f h₁ h₂⟩
+    IsOpenImmersion f ↔ OpenEmbedding f.1.base ∧ ∀ x, IsIso (f.stalkMap x) :=
+  ⟨fun H => ⟨H.1, fun x ↦ inferInstanceAs <| IsIso (f.val.stalkMap x)⟩,
+   fun ⟨h₁, h₂⟩ => @IsOpenImmersion.of_stalk_iso _ _ f h₁ h₂⟩
 
 theorem _root_.AlgebraicGeometry.isIso_iff_isOpenImmersion {X Y : Scheme.{u}} (f : X ⟶ Y) :
     IsIso f ↔ IsOpenImmersion f ∧ Epi f.1.base :=
   ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨h₁, h₂⟩ => @IsOpenImmersion.to_iso _ _ f h₁ h₂⟩
 
 theorem _root_.AlgebraicGeometry.isIso_iff_stalk_iso {X Y : Scheme.{u}} (f : X ⟶ Y) :
-    IsIso f ↔ IsIso f.1.base ∧ ∀ x, IsIso (PresheafedSpace.stalkMap f.1 x) := by
+    IsIso f ↔ IsIso f.1.base ∧ ∀ x, IsIso (f.stalkMap x) := by
   rw [isIso_iff_isOpenImmersion, IsOpenImmersion.iff_stalk_iso, and_comm, ← and_assoc]
   refine and_congr ⟨?_, ?_⟩ Iff.rfl
   · rintro ⟨h₁, h₂⟩

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -598,6 +598,7 @@ lemma awayToSection_germ (f x) :
   ext z
   apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr
   apply Proj.stalkIso'_germ
+
 /--
 The ring map from `A⁰_ f` to the global sections of the structure sheaf of the projective spectrum
 of `A` restricted to the basic open set `D(f)`.
@@ -609,14 +610,13 @@ def awayToΓ (f) : CommRingCat.of (A⁰_ f) ⟶ LocallyRingedSpace.Γ.obj (op <|
     (homOfLE (Opens.openEmbedding_obj_top _).le).op
 
 lemma awayToΓ_ΓToStalk (f) (x) :
-    awayToΓ 𝒜 f ≫ LocallyRingedSpace.ΓToStalk (Proj| pbo f) x =
+    awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x =
       HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr x.2) ≫
       (Proj.stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
       ((Proj.toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.openEmbedding _) x).inv := by
-  rw [awayToΓ, Category.assoc, LocallyRingedSpace.ΓToStalk, ← Category.assoc _ (Iso.inv _),
-    Iso.eq_comp_inv, Category.assoc, Category.assoc]
-  simp only [LocallyRingedSpace.restrict, SheafedSpace.restrict]
-  rw [PresheafedSpace.restrictStalkIso_hom_eq_germ]
+  rw [awayToΓ, Category.assoc, ← Category.assoc _ (Iso.inv _),
+    Iso.eq_comp_inv, Category.assoc, Category.assoc, Presheaf.Γgerm]
+  rw [LocallyRingedSpace.restrictStalkIso_hom_eq_germ]
   simp only [Proj.toLocallyRingedSpace, Proj.toSheafedSpace]
   rw [Presheaf.germ_res, awayToSection_germ]
   rfl
@@ -634,7 +634,7 @@ open HomogeneousLocalization LocalRing
 lemma toSpec_base_apply_eq_comap {f} (x : Proj| pbo f) :
     (toSpec 𝒜 f).1.base x = PrimeSpectrum.comap (mapId 𝒜 (Submonoid.powers_le.mpr x.2))
       (closedPoint (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)) := by
-  show PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ LocallyRingedSpace.ΓToStalk (Proj| pbo f) x)
+  show PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x)
         (LocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _
   rw [awayToΓ_ΓToStalk, CommRingCat.comp_eq_ring_hom_comp, PrimeSpectrum.comap_comp]
   exact congr(PrimeSpectrum.comap _ $(@LocalRing.comap_closedPoint
@@ -678,8 +678,8 @@ lemma toOpen_toSpec_val_c_app (f) (U) :
 
 @[reassoc]
 lemma toStalk_stalkMap_toSpec (f) (x) :
-    StructureSheaf.toStalk _ _ ≫ PresheafedSpace.stalkMap (toSpec 𝒜 f).1 x =
-      awayToΓ 𝒜 f ≫ (Proj| pbo f).ΓToStalk x := by
+    StructureSheaf.toStalk _ _ ≫ (toSpec 𝒜 f).stalkMap x =
+      awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x := by
   rw [StructureSheaf.toStalk, Category.assoc]
   simp_rw [CommRingCat.coe_of]
   erw [PresheafedSpace.stalkMap_germ']
@@ -775,7 +775,7 @@ lemma toStalk_specStalkEquiv (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0
     (Q := AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toAlgHom.comp_algebraMap
 
 lemma stalkMap_toSpec (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
-    LocallyRingedSpace.stalkMap (toSpec 𝒜 f) x =
+    (toSpec 𝒜 f).stalkMap x =
       (specStalkEquiv 𝒜 f x f_deg hm).hom ≫ (Proj.stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
       ((Proj.toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.openEmbedding _) x).inv :=
   IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).1.base x).asIdeal.primeCompl
@@ -786,7 +786,7 @@ lemma stalkMap_toSpec (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
 lemma isIso_toSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
     IsIso (toSpec 𝒜 f) := by
   haveI : IsIso (toSpec 𝒜 f).1.base := toSpec_base_isIso 𝒜 f_deg hm
-  haveI (x) : IsIso (LocallyRingedSpace.stalkMap (toSpec 𝒜 f) x) := by
+  haveI (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
     rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
   haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
     LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)

Mathlib/AlgebraicGeometry/Properties.lean

@@ -164,7 +164,7 @@ theorem eq_zero_of_basicOpen_eq_bot {X : Scheme} [hX : IsReduced X] {U : Opens X
     specialize H (f.app _ s) _ ⟨x, by rw [Opens.mem_mk, e]; trivial⟩
     · rw [← Scheme.preimage_basicOpen, hs]; ext1; simp [Opens.map]
     · erw [← PresheafedSpace.stalkMap_germ_apply f.1 ⟨_, _⟩ ⟨x, _⟩] at H
-      apply_fun inv <| PresheafedSpace.stalkMap f.val x at H
+      apply_fun inv <| f.stalkMap x at H
       erw [CategoryTheory.IsIso.hom_inv_id_apply, map_zero] at H
       exact H
   | h₃ R =>

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -430,24 +430,19 @@ def morphismRestrictRestrictBasicOpen {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Open
 /-- The stalk map of a restriction of a morphism is isomorphic to the stalk map of the original map.
 -/
 def morphismRestrictStalkMap {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens Y) (x) :
-    Arrow.mk (PresheafedSpace.stalkMap (f ∣_ U).1 x) ≅
-      Arrow.mk (PresheafedSpace.stalkMap f.1 x.1) := by
-  fapply Arrow.isoMk'
-  · refine Y.restrictStalkIso U.openEmbedding ((f ∣_ U).1.1 x) ≪≫ TopCat.Presheaf.stalkCongr _ ?_
-    apply Inseparable.of_eq
-    exact morphismRestrict_base_coe f U x
-  · exact X.restrictStalkIso (Opens.openEmbedding _) _
-  · apply TopCat.Presheaf.stalk_hom_ext
+    Arrow.mk ((f ∣_ U).stalkMap x) ≅ Arrow.mk (f.stalkMap x.1) := Arrow.isoMk' _ _
+  (Y.restrictStalkIso U.openEmbedding ((f ∣_ U).1.1 x) ≪≫
+    (TopCat.Presheaf.stalkCongr _ <| Inseparable.of_eq <| morphismRestrict_base_coe f U x))
+  (X.restrictStalkIso (Opens.openEmbedding _) _) <| by
+    apply TopCat.Presheaf.stalk_hom_ext
     intro V hxV
     change ↑(f ⁻¹ᵁ U) at x
-    simp only [Scheme.restrict_presheaf_obj, unop_op, Opens.coe_inclusion, Iso.trans_hom,
-      TopCat.Presheaf.stalkCongr_hom, Category.assoc, Scheme.restrict_toPresheafedSpace]
-    rw [PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc,
-      TopCat.Presheaf.germ_stalkSpecializes'_assoc,
-      PresheafedSpace.stalkMap_germ'_assoc, PresheafedSpace.stalkMap_germ',
-      ← Scheme.Hom.app, ← Scheme.Hom.app, morphismRestrict_app,
-      PresheafedSpace.restrictStalkIso_hom_eq_germ, Category.assoc, TopCat.Presheaf.germ_res]
-    rfl
+    simp only [Scheme.restrict_presheaf_obj, Iso.trans_hom, Category.assoc,
+      Scheme.stalkMap_germ'_assoc, morphismRestrict_app']
+    simp only [Scheme.restrict_toPresheafedSpace, PresheafedSpace.restrictStalkIso_hom_eq_germ_assoc]
+    simp only [Scheme.Hom.appLE, Scheme.Hom.app, Scheme.restrict,
+      PresheafedSpace.restrictStalkIso_hom_eq_germ]
+    simp [TopCat.Presheaf.germ_res]
 
 instance {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens Y) [IsOpenImmersion f] :
     IsOpenImmersion (f ∣_ U) := by