[Merged by Bors] - feat(AlgebraicGeometry/GammaSpecAdjunction): a missing lemma

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -368,6 +368,72 @@ lemma locallyRingedSpaceAdjunction_counit :
     locallyRingedSpaceAdjunction.counit = (NatIso.op SpecΓIdentity.{u}).inv := rfl
 #align algebraic_geometry.Γ_Spec.LocallyRingedSpace_adjunction_counit AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_counit
 
+lemma locallyRingedSpaceAdjunction_counit_app (R : CommRingCatᵒᵖ) :
+    (locallyRingedSpaceAdjunction.counit.app R).unop =
+    toOpen R.unop ⊤ := rfl
+
+lemma locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] :
+    (locallyRingedSpaceAdjunction.counit.app <| op <| .of R).unop =
+    toOpen R ⊤ := 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
+
+@[reassoc]
+lemma locallyRingedSpaceAdjunction_homEquiv_apply_naturality
+    {X : LocallyRingedSpace} {R : CommRingCatᵒᵖ}
+    (f : Γ.rightOp.obj X ⟶ R) {U V} (i : U ⟶ V) :
+    (structureSheaf R.unop).val.map i ≫
+      (locallyRingedSpaceAdjunction.homEquiv X R f).1.c.app V =
+    (locallyRingedSpaceAdjunction.homEquiv X R f).1.c.app U ≫
+      ((locallyRingedSpaceAdjunction.homEquiv X R f).val.base _* X.presheaf).map i :=
+  NatTrans.naturality _ _
+
+@[reassoc]
+lemma locallyRingedSpaceAdjunction_homEquiv_apply_naturality'
+    {X : LocallyRingedSpace} {R : Type u} [CommRing R]
+    (f : CommRingCat.of R ⟶ Γ.obj <| op X) {U V} (i : U ⟶ V) :
+    (structureSheaf R).val.map i ≫
+      (locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) (op f)).1.c.app V =
+    (locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) (op f)).1.c.app U ≫
+      ((locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) (op f)).val.base _*
+        X.presheaf).map i :=
+  NatTrans.naturality _ _
+
+@[reassoc]
+lemma locallyRingedSpaceAdjunction_homEquiv_apply_naturality''
+    {X : LocallyRingedSpace} {R : Type u} [CommRing R]
+    (f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) {U V} (i : U ⟶ V) :
+    (structureSheaf R).val.map i ≫
+      (locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) f).1.c.app V =
+    (locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) f).1.c.app U ≫
+      ((locallyRingedSpaceAdjunction.homEquiv X (op <| .of R) f).val.base _*
+        X.presheaf).map i :=
+  NatTrans.naturality _ _
+
+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,
+    locallyRingedSpaceAdjunction_homEquiv_apply_naturality'' f (homOfLE (le_top (a := U.unop))).op,
+    ← 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

@@ -211,6 +211,26 @@ 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 (R : CommRingCat.{u}) :
+    (Spec.locallyRingedSpaceObj R).presheaf = (structureSheaf R).1 := 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

@@ -246,9 +246,12 @@
   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⟩
 
 instance {F : C ⥤ D} [Faithful F] : Faithful F.op where
   map_injective h := Quiver.Hom.unop_inj <| by simpa using map_injective F (Quiver.Hom.op_inj h)