get rid of erw

Author: chrisflav

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -61,24 +61,6 @@ 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.presheaf.Γgerm x) (LocalRing.closedPoint (X.presheaf.stalk x))

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -615,9 +615,8 @@ lemma awayToΓ_ΓToStalk (f) (x) :
       (Proj.stalkIso' 𝒜 x.1).toCommRingCatIso.inv ≫
       ((Proj.toLocallyRingedSpace 𝒜).restrictStalkIso (Opens.openEmbedding _) x).inv := by
   rw [awayToΓ, Category.assoc, ← Category.assoc _ (Iso.inv _),
-    Iso.eq_comp_inv, Category.assoc, Category.assoc]
-  simp only [LocallyRingedSpace.restrict, Presheaf.Γgerm]
-  erw [PresheafedSpace.restrictStalkIso_hom_eq_germ]
+    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

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -631,6 +631,25 @@ lemma stalkMap_germ' {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Opens Y) (x : X) (hx
       f.app U ≫ X.presheaf.germ (U := f⁻¹ᵁ U) ⟨x, hx⟩ :=
   PresheafedSpace.stalkMap_germ' f.val U x hx
 
+variable {U : TopCat} (X : Scheme.{u}) {f : U ⟶ X.toTopCat} (h : OpenEmbedding f)
+  (V : Opens U) (x : U) (hx : x ∈ V)
+
+@[elementwise, reassoc]
+lemma restrictStalkIso_hom_eq_germ :
+    (X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrictStalkIso h x).hom =
+      X.presheaf.germ ⟨f x, show f x ∈ h.isOpenMap.functor.obj V from ⟨x, hx, rfl⟩⟩ :=
+  PresheafedSpace.restrictStalkIso_hom_eq_germ X.toPresheafedSpace h V x hx
+
+@[simp, elementwise, reassoc]
+lemma restrictStalkIso_inv_eq_germ :
+    X.presheaf.germ ⟨f x, show f x ∈ h.isOpenMap.functor.obj V from ⟨x, hx, rfl⟩⟩ ≫
+      (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩ :=
+  PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace h V x hx
+
+lemma restrictStalkIso_inv_eq_ofRestrict :
+    (X.restrictStalkIso h x).inv = (X.ofRestrict h).stalkMap x :=
+  PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict X.toPresheafedSpace h x
+
 end Scheme
 
 end Stalks

Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean

@@ -371,6 +371,42 @@ lemma stalkMap_inv_hom {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) (x : X) :
   rw [← stalkMap_comp, LocallyRingedSpace.stalkMap_congr_hom (e.hom ≫ e.inv) (𝟙 _) (by simp)]
   simp
 
+@[reassoc, elementwise]
+lemma stalkMap_germ {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) (U : Opens Y)
+    (x : (Opens.map f.val.base).obj U) :
+    Y.presheaf.germ ⟨f.val.base x.val, x.property⟩ ≫ f.stalkMap x.val =
+      f.val.c.app (op U) ≫ X.presheaf.germ x :=
+  PresheafedSpace.stalkMap_germ f.val U x
+
+@[reassoc (attr := simp), elementwise (attr := simp)]
+lemma stalkMap_germ' {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) (U : Opens Y) (x : X)
+    (hx : f.val.base x ∈ U) :
+    Y.presheaf.germ ⟨f.val.base x, hx⟩ ≫ f.stalkMap x =
+      f.val.c.app (op U) ≫ X.presheaf.germ (U := (Opens.map f.val.base).obj U) ⟨x, hx⟩ :=
+  PresheafedSpace.stalkMap_germ' f.val U x hx
+
+variable {U : TopCat} (X : LocallyRingedSpace.{u}) {f : U ⟶ X.toTopCat} (h : OpenEmbedding f)
+  (V : Opens U) (x : U) (hx : x ∈ V)
+
+@[elementwise, reassoc]
+lemma restrictStalkIso_hom_eq_germ :
+    (X.restrict h).presheaf.germ ⟨x, hx⟩ ≫ (X.restrictStalkIso h x).hom =
+      X.presheaf.germ ⟨f x, show f x ∈ h.isOpenMap.functor.obj V from ⟨x, hx, rfl⟩⟩ :=
+  PresheafedSpace.restrictStalkIso_hom_eq_germ X.toPresheafedSpace h V x hx
+
+@[simp, elementwise, reassoc]
+lemma restrictStalkIso_inv_eq_germ :
+    X.presheaf.germ ⟨f x, show f x ∈ h.isOpenMap.functor.obj V from ⟨x, hx, rfl⟩⟩ ≫
+      (X.restrictStalkIso h x).inv = (X.restrict h).presheaf.germ ⟨x, hx⟩ :=
+  PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace h V x hx
+
+lemma restrictStalkIso_inv_eq_ofRestrict :
+    (X.restrictStalkIso h x).inv = (X.ofRestrict h).stalkMap x :=
+  PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict X.toPresheafedSpace h x
+
+instance ofRestrict_stalkMap_isIso : IsIso ((X.ofRestrict h).stalkMap x) :=
+  PresheafedSpace.ofRestrict_stalkMap_isIso X.toPresheafedSpace h x
+
 end Stalks
 
 end LocallyRingedSpace