Commit 2024-06-10 11:04 5e33eb3b

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

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