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

[jjaassoonn]

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)$

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]

---

[jjaassoonn]

This is a fun error:

Error: ././././Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean:371:9: error: AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction_homEquiv_apply.{u_1} Left-hand side simplifies from
  (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X R) f
to
  (AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.homEquiv X R) f

They look the same to me.

[erdOne]

Looking at the lemmas used, I think some implicit types involved were dsimped.
This is a mwe. Not sure what to do here. Maybe we shouldn't tag the _obj lemmas as simp, or make them scoped instead.

import Mathlib.Logic.Equiv.Defs

def A := Unit
@[simp] def B := A
def e : B ≃ Unit := Equiv.refl _

@[simp] lemma e_apply (x) : e x = x := rfl

example (x) : e x = x := by simp -- fails because `B` gets rewritten to `A` first.

#lint only simpNF

[erdOne]

Maybe either raise its priority or don't tag it as simp.

[jjaassoonn]

Maybe either raise its priority or don't tag it as simp.

Raising priority to high doesn't seem to be working, so I deleted the simp attribute

[github-actions]

PR summary

Import changes

No significant changes to the import graph

---

Declarations diff

+ Spec.locallyRingedSpaceObj_presheaf'
+ Spec.locallyRingedSpaceObj_presheaf_map
+ Spec.locallyRingedSpaceObj_presheaf_map'
+ Spec.locallyRingedSpaceObj_sheaf
+ Spec.locallyRingedSpaceObj_sheaf'
+ locallyRingedSpaceAdjunction_counit_app
+ locallyRingedSpaceAdjunction_counit_app'
+ locallyRingedSpaceAdjunction_homEquiv_apply
+ locallyRingedSpaceAdjunction_homEquiv_apply'
+ rightOp_map_unop
+ toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style