feat(AlgebraicGeometry/GammaSpecAdjunction): a missing lemma (#13412)

Added the following lemma:

Let $X$ be a locally ringed space, $R$ a ring and $U \subseteq \mathrm{Spec} R$ an open set.
Then for any $f : R \to \Gamma(\mathcal O_X, X)$, if we denote $F$ as the corresponding morphism $X \to \mathrm{Spec} R$ under the gamma spec adjunction  we have that 
the composition $res^{\mathrm{X}}\_{F^{-1}U} \circ f$ is equal to the composition $(R \to \mathcal{O}_{\mathrm{Spec} R}(U)\circ F(U)$
 
```lean
lemma toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app
    {X : LocallyRingedSpace} {R : Type u} [CommRing R]
    (f : LocallyRingedSpace.Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) (U) :
    StructureSheaf.toOpen R U.unop ≫
      (locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) f).1.c.app U =
    f.unop ≫ X.presheaf.map (homOfLE le_top).op := by
```

found usefuly by Andrew during #12371

Co-authored-by: Andrew Yang <[email protected]>

Author: 2 people

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -368,6 +368,43 @@ lemma locallyRingedSpaceAdjunction_counit :
     locallyRingedSpaceAdjunction.counit = (NatIso.op SpecΓIdentity.{u}).inv := rfl
 #align algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction_counit AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit
 
+@[simp]
+lemma locallyRingedSpaceAdjunction_counit_app (R : CommRingCatᵒᵖ) :
+    locallyRingedSpaceAdjunction.counit.app R =
+      (toOpen R.unop ⊤).op := rfl
+
+@[simp]
+lemma locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] :
+    locallyRingedSpaceAdjunction.counit.app (op <| CommRingCat.of R) =
+      (toOpen R ⊤).op := rfl
+
+lemma locallyRingedSpaceAdjunction_homEquiv_apply
+    {X : LocallyRingedSpace} {R : CommRingCatᵒᵖ}
+    (f : Γ.rightOp.obj X ⟶ R) :
+    locallyRingedSpaceAdjunction.homEquiv X R f =
+      identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f.unop := rfl
+
+lemma locallyRingedSpaceAdjunction_homEquiv_apply'
+    {X : LocallyRingedSpace} {R : Type u} [CommRing R]
+    (f : CommRingCat.of R ⟶ Γ.obj <| op X) :
+    locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) (op f) =
+      identityToΓSpec.app X ≫ Spec.locallyRingedSpaceMap f := rfl
+
+lemma toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app
+    {X : LocallyRingedSpace} {R : Type u} [CommRing R]
+    (f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) (U) :
+    StructureSheaf.toOpen R U.unop ≫
+      (locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) f).1.c.app U =
+    f.unop ≫ X.presheaf.map (homOfLE le_top).op := by
+  rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
+    NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,
+    show (toOpen R ⊤) = (toOpen R ⊤).op.unop from rfl,
+    ← locallyRingedSpaceAdjunction_counit_app']
+  simp_rw [← Γ_map_op]
+  rw [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp, ← Adjunction.homEquiv_counit,
+    Equiv.symm_apply_apply]
+  rfl
+
 -- Porting Note: Commented
 --attribute [local semireducible] Spec.toLocallyRingedSpace
 

Mathlib/AlgebraicGeometry/Spec.lean

@@ -202,7 +202,7 @@ set_option linter.uppercaseLean3 false in
 -- if more is needed, add them here
 /-- The spectrum of a commutative ring, as a `LocallyRingedSpace`.
 -/
-@[simps! toSheafedSpace]
+@[simps! toSheafedSpace presheaf]
 def Spec.locallyRingedSpaceObj (R : CommRingCat.{u}) : LocallyRingedSpace :=
   { Spec.sheafedSpaceObj R with
     localRing := fun x =>
@@ -211,6 +211,23 @@ def Spec.locallyRingedSpaceObj (R : CommRingCat.{u}) : LocallyRingedSpace :=
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.Spec.LocallyRingedSpace_obj AlgebraicGeometry.Spec.locallyRingedSpaceObj
 
+lemma Spec.locallyRingedSpaceObj_sheaf (R : CommRingCat.{u}) :
+    (Spec.locallyRingedSpaceObj R).sheaf = structureSheaf R := rfl
+
+lemma Spec.locallyRingedSpaceObj_sheaf' (R : Type u) [CommRing R] :
+    (Spec.locallyRingedSpaceObj <| CommRingCat.of R).sheaf = structureSheaf R := rfl
+
+lemma Spec.locallyRingedSpaceObj_presheaf_map (R : CommRingCat.{u}) {U V} (i : U ⟶ V) :
+    (Spec.locallyRingedSpaceObj R).presheaf.map i =
+    (structureSheaf R).1.map i := rfl
+
+lemma Spec.locallyRingedSpaceObj_presheaf' (R : Type u) [CommRing R] :
+    (Spec.locallyRingedSpaceObj <| CommRingCat.of R).presheaf = (structureSheaf R).1 := rfl
+
+lemma Spec.locallyRingedSpaceObj_presheaf_map' (R : Type u) [CommRing R] {U V} (i : U ⟶ V) :
+    (Spec.locallyRingedSpaceObj <| CommRingCat.of R).presheaf.map i =
+    (structureSheaf R).1.map i := rfl
+
 @[elementwise]
 theorem stalkMap_toStalk {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
     toStalk R (PrimeSpectrum.comap f p) ≫ PresheafedSpace.stalkMap (Spec.sheafedSpaceMap f) p =

Mathlib/CategoryTheory/Opposites.lean

@@ -250,6 +250,9 @@ protected def rightOp (F : Cᵒᵖ ⥤ D) : C ⥤ Dᵒᵖ where
   map f := (F.map f.op).op
 #align category_theory.functor.right_op CategoryTheory.Functor.rightOp
 
+lemma rightOp_map_unop {F : Cᵒᵖ ⥤ D} {X Y} (f : X ⟶ Y) :
+    (F.rightOp.map f).unop = F.map f.op := rfl
+
 instance {F : C ⥤ D} [Full F] : Full F.op where
   map_surjective f := ⟨(F.preimage f.unop).op, by simp⟩